logo

Show the Proof

In [1]:
import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof
Out[1]:
 step typerequirementsstatement
0instantiation1, 2, 3, , , , , , , ,  ⊢  
  : , : , :
1reference31  ⊢  
2instantiation4, 22, 54, 5, 6, , , , , , , ,  ⊢  
  : , : , : , :
3instantiation39, 7, 8  ⊢  
  : , : , :
4theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_ket_is_ket
5instantiation45, 22, 54, 9, , , , , , ,  ⊢  
  : , : , :
6assumption  ⊢  
7theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat5
8instantiation10  ⊢  
  : , : , : , : , :
9instantiation31, 11, 12, , , , , , ,  ⊢  
  : , : , :
10theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
11instantiation36, 13, 22, 54, 14, , , , , , ,  ⊢  
  : , : , : , :
12instantiation39, 15, 16  ⊢  
  : , : , :
13assumption  ⊢  
14instantiation45, 22, 54, 17, , , , , ,  ⊢  
  : , : , :
15theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat4
16instantiation18  ⊢  
  : , : , : , :
17instantiation31, 19, 20, , , , , ,  ⊢  
  : , : , :
18theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
19instantiation21, 22, 60, 54, 23, 24, , , , , ,  ⊢  
  : , : , : , : , :
20instantiation39, 25, 26  ⊢  
  : , : , :
21theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_op_is_op
22instantiation62, 49  ⊢  
  :
23instantiation45, 60, 54, 27, , ,  ⊢  
  : , : , :
24instantiation28, 63, 49, 29, , ,  ⊢  
  : , : , :
25theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat3
26instantiation30  ⊢  
  : , : , :
27instantiation31, 32, 33, , ,  ⊢  
  : , : , :
28theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_matrix_is_linmap
29modus ponens34, 35, , ,  ⊢  
30theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
31theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
32instantiation36, 37, 60, 54, 38, , ,  ⊢  
  : , : , : , :
33instantiation39, 40, 41  ⊢  
  : , : , :
34instantiation42, 58, 43, 44, ,  ⊢  
  : , : , : , : , : , :
35assumption  ⊢  
36theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_complex_closure
37assumption  ⊢  
38instantiation45, 60, 54, 46, ,  ⊢  
  : , : , :
39axiom  ⊢  
 proveit.physics.quantum.algebra.multi_qmult_def
40theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
41instantiation47  ⊢  
  : , :
42theorem  ⊢  
 proveit.linear_algebra.addition.summation_closure
43instantiation48, 63, 49,  ⊢  
  : , :
44instantiation50, 51  ⊢  
  : , :
45theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_is_linmap
46instantiation52, 53, 60, 54, 55, ,  ⊢  
  : , : , : , :
47theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
48theorem  ⊢  
 proveit.linear_algebra.matrices.complex_matrix_space_is_vec_space
49assumption  ⊢  
50theorem  ⊢  
 proveit.core_expr_types.tuples.range_from1_len_typical_eq
51instantiation56, 57, 58  ⊢  
  : , : , :
52theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_complex_op_closure
53assumption  ⊢  
54theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_set_is_hilbert_space
55instantiation59, 60, 61,  ⊢  
  : , :
56theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
57theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
58assumption  ⊢  
59theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_bra_is_linmap
60instantiation62, 63  ⊢  
  :
61assumption  ⊢  
62theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
63assumption  ⊢