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, 4, 5, 6, , , , , , , , ,  ⊢  
  : , : , : , : , :
1theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_pulling_scalar_out_front
2theorem  ⊢  
 proveit.numbers.numerals.decimals.nat6
3theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
4assumption  ⊢  
5reference13  ⊢  
6instantiation45, 7, 8, , , , , , , ,  ⊢  
  : , : , :
7instantiation9, 10, 11, , , , , , , ,  ⊢  
  : , :
8instantiation53, 12, 13  ⊢  
  : , : , :
9theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_complex_left_closure
10instantiation45, 14, 15, , , , , , , ,  ⊢  
  : , : , :
11instantiation16, 74, 75,  ⊢  
  : , :
12theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat6
13instantiation17  ⊢  
  : , : , : , : , : , :
14instantiation18, 36, 68, 19, 20, , , , , , , ,  ⊢  
  : , : , : , :
15instantiation53, 21, 22  ⊢  
  : , : , :
16theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_bra_in_QmultCodomain
17theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_6_typical_eq
18theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_ket_is_ket
19instantiation59, 36, 68, 23, , , , , , ,  ⊢  
  : , : , :
20assumption  ⊢  
21theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat5
22instantiation24  ⊢  
  : , : , : , : , :
23instantiation45, 25, 26, , , , , , ,  ⊢  
  : , : , :
24theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
25instantiation50, 27, 36, 68, 28, , , , , , ,  ⊢  
  : , : , : , :
26instantiation53, 29, 30  ⊢  
  : , : , :
27assumption  ⊢  
28instantiation59, 36, 68, 31, , , , , ,  ⊢  
  : , : , :
29theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat4
30instantiation32  ⊢  
  : , : , : , :
31instantiation45, 33, 34, , , , , ,  ⊢  
  : , : , :
32theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
33instantiation35, 36, 74, 68, 37, 38, , , , , ,  ⊢  
  : , : , : , : , :
34instantiation53, 39, 40  ⊢  
  : , : , :
35theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_op_is_op
36instantiation76, 63  ⊢  
  :
37instantiation59, 74, 68, 41, , ,  ⊢  
  : , : , :
38instantiation42, 77, 63, 43, , ,  ⊢  
  : , : , :
39theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat3
40instantiation44  ⊢  
  : , : , :
41instantiation45, 46, 47, , ,  ⊢  
  : , : , :
42theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_matrix_is_linmap
43modus ponens48, 49, , ,  ⊢  
44theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
45theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
46instantiation50, 51, 74, 68, 52, , ,  ⊢  
  : , : , : , :
47instantiation53, 54, 55  ⊢  
  : , : , :
48instantiation56, 72, 57, 58, ,  ⊢  
  : , : , : , : , : , :
49assumption  ⊢  
50theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_complex_closure
51assumption  ⊢  
52instantiation59, 74, 68, 60, ,  ⊢  
  : , : , :
53axiom  ⊢  
 proveit.physics.quantum.algebra.multi_qmult_def
54theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
55instantiation61  ⊢  
  : , :
56theorem  ⊢  
 proveit.linear_algebra.addition.summation_closure
57instantiation62, 77, 63,  ⊢  
  : , :
58instantiation64, 65  ⊢  
  : , :
59theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_is_linmap
60instantiation66, 67, 74, 68, 69, ,  ⊢  
  : , : , : , :
61theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
62theorem  ⊢  
 proveit.linear_algebra.matrices.complex_matrix_space_is_vec_space
63assumption  ⊢  
64theorem  ⊢  
 proveit.core_expr_types.tuples.range_from1_len_typical_eq
65instantiation70, 71, 72  ⊢  
  : , : , :
66theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_complex_op_closure
67assumption  ⊢  
68theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_set_is_hilbert_space
69instantiation73, 74, 75,  ⊢  
  : , :
70theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
71theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
72assumption  ⊢  
73theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_bra_is_linmap
74instantiation76, 77  ⊢  
  :
75assumption  ⊢  
76theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
77assumption  ⊢