Metamath Proof Explorer - mmtheorems56

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 5501-5600 - Page 56 of 58

Type	Label	Description
Statement
Theorem	cmcm 5501	Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22.
|- A e. CH   &   |- B e. CH   =>   |- (A Com B <-> B Com A)
Theorem	cmcm2 5502	Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39.
|- A e. CH   &   |- B e. CH   =>   |- (A Com B <-> A Com (_|_` B))
Theorem	cmcm3 5503	Commutation with orthocomplement. Remark in [Kalmbach] p. 23.
|- A e. CH   &   |- B e. CH   =>   |- (A Com B <-> (_|_` A) Com B)
Theorem	cmcm4 5504	Commutation with orthocomplement. Remark in [Kalmbach] p. 23.
|- A e. CH   &   |- B e. CH   =>   |- (A Com B <-> (_|_` A) Com (_|_` B))
Theorem	cmbr2 5505	Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23.
|- A e. CH   &   |- B e. CH   =>   |- (A Com B <-> A = ((A vH B) i^i (A vH (_|_` B))))
Theorem	cmcmi 5506	Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22.
|- A e. CH   &   |- B e. CH   &   |- A Com B   =>   |- B Com A
Theorem	cmcm2i 5507	Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39.
|- A e. CH   &   |- B e. CH   &   |- A Com B   =>   |- A Com (_|_` B)
Theorem	cmcm3i 5508	Commutation with orthocomplement. Remark of [Kalmbach] p. 23.
|- A e. CH   &   |- B e. CH   &   |- A Com B   =>   |- (_|_` A) Com B
Theorem	cmbr3 5509	Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23.
|- A e. CH   &   |- B e. CH   =>   |- (A Com B <-> (A i^i ((_|_` A) vH B)) = (A i^i B))
Theorem	cmbr4 5510	Alternate definition for the commutes relation.
|- A e. CH   &   |- B e. CH   =>   |- (A Com B <-> (A i^i ((_|_` A) vH B)) (_ B)
Theorem	cmle 5511	Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of [Beran] p. 40.
|- A e. CH   &   |- B e. CH   &   |- A (_ B   =>   |- A Com B
Theorem	cmj1 5512	A Hilbert lattice element commutes with its join.
|- A e. CH   &   |- B e. CH   =>   |- A Com (A vH B)
Theorem	cmj2 5513	A Hilbert lattice element commutes with its join.
|- A e. CH   &   |- B e. CH   =>   |- B Com (A vH B)
Theorem	cmm1 5514	A Hilbert lattice element commutes with its meet.
|- A e. CH   &   |- B e. CH   =>   |- A Com (A i^i B)
Theorem	cmm2 5515	A Hilbert lattice element commutes with its meet.
|- A e. CH   &   |- B e. CH   =>   |- B Com (A i^i B)
Theorem	cmid 5516	The commutes relation is reflexive.
|- A e. CH   =>   |- A Com A
Theorem	pjoml3t 5517	Variation of orthomodular law.
|- ((A e. CH /\ B e. CH) -> (B (_ A -> (A i^i ((_|_` A) vH B)) = B))
Theorem	fh1 5518	Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. First of two parts. Theorem 5 of [Kalmbach] p. 25.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- A Com B   &   |- A Com C   =>   |- (A i^i (B vH C)) = ((A i^i B) vH (A i^i C))
Theorem	fh2 5519	Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Second of two parts. Theorem 5 of [Kalmbach] p. 25.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- A Com B   &   |- A Com C   =>   |- (B i^i (A vH C)) = ((B i^i A) vH (B i^i C))
Theorem	qlax1 5520	One of the equations showing CH is an ortholattice. (This corresponds to axiom "ax-1" in the Quantum Logic Explorer.)
|- A e. CH   =>   |- A = (_|_` (_|_` A))
Theorem	qlax2 5521	One of the equations showing CH is an ortholattice. (This corresponds to axiom "ax-2" in the Quantum Logic Explorer.)
|- A e. CH   &   |- B e. CH   =>   |- (A vH B) = (B vH A)
Theorem	qlax3 5522	One of the equations showing CH is an ortholattice. (This corresponds to axiom "ax-3" in the Quantum Logic Explorer.)
|- A e. CH   &   |- B e. CH   &   |- C e. CH   =>   |- ((A vH B) vH C) = (A vH (B vH C))
Theorem	qlax4 5523	One of the equations showing CH is an ortholattice. (This corresponds to axiom "ax-4" in the Quantum Logic Explorer.)
|- A e. CH   &   |- B e. CH   =>   |- (A vH (B vH (_|_` B))) = (B vH (_|_` B))
Theorem	qlax5 5524	One of the equations showing CH is an ortholattice. (This corresponds to axiom "ax-5" in the Quantum Logic Explorer.)
|- A e. CH   &   |- B e. CH   =>   |- (A vH (_|_` ((_|_` A) vH B))) = A
Theorem	qlaxr1 5525	One of the conditions showing CH is an ortholattice. (This corresponds to axiom "ax-r1" in the Quantum Logic Explorer.)
|- A e. CH   &   |- B e. CH   &   |- A = B   =>   |- B = A
Theorem	qlaxr2 5526	One of the conditions showing CH is an ortholattice. (This corresponds to axiom "ax-r2" in the Quantum Logic Explorer.)
|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- A = B   &   |- B = C   =>   |- A = C
Theorem	qlaxr4 5527	One of the conditions showing CH is an ortholattice. (This corresponds to axiom "ax-r4" in the Quantum Logic Explorer.)
|- A e. CH   &   |- B e. CH   &   |- A = B   =>   |- (_|_` A) = (_|_` B)
Theorem	qlaxr5 5528	One of the conditions showing CH is an ortholattice. (This corresponds to axiom "ax-r5" in the Quantum Logic Explorer.)
|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- A = B   =>   |- (A vH C) = (B vH C)
Theorem	qlaxr3 5529	A variation of the orthomodular law, showing CH is an orthomodular lattice. (This corresponds to axiom "ax-r3" in the Quantum Logic Explorer.)
|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- (C vH (_|_` C)) = ((_|_` ((_|_` A) vH (_|_` B))) vH (_|_` (A vH B)))   =>   |- A = B
Theorem	osumlem1 5530	Lemma for osum 5538.
|- A e. CH   &   |- B e. CH   &   |- B (_ (_|_` A)   &   |- (ph <-> (((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))))   =>   |- (ph -> (((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)))
Theorem	osumlem2 5531	Lemma for osum 5538.
|- A e. CH   &   |- B e. CH   &   |- B (_ (_|_` A)   &   |- (ph <-> (((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))))   =>   |- (ph -> (((norm` (C -v x))^2) + ((norm` (D -v y))^2)) = ((norm` (R -v z))^2))
Theorem	osumlem3 5532	Lemma for osum 5538.
|- A e. CH   &   |- B e. CH   &   |- B (_ (_|_` A)   &   |- (ph <-> (((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))))   =>   |- (ph -> (norm` (D -v y)) <_ (norm` (R -v z)))
Theorem	osumlem4 5533	Lemma for osum 5538.
|- A e. CH   &   |- B e. CH   &   |- B (_ (_|_` A)   &   |- G e. V   &   |- H e. V   =>   |- ((((F:NN-->A /\ G:NN-->B) /\ A.w e. NN (H` w) = ((F` w) +v (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (H ~~>v z -> G ~~>v y))
Theorem	osumlem5 5534	Lemma for osum 5538.
|- A e. CH   &   |- B e. CH   =>   |- (H:NN-->(A +H B) -> E.fE.g((f:NN-->A /\ g:NN-->B) /\ A.w e. NN (H` w) = ((f` w) +v (g` w))))
Theorem	osumlem6 5535	Lemma for osum 5538.
|- A e. CH   &   |- B e. CH   &   |- B (_ (_|_` A)   &   |- H e. V   =>   |- (((H:NN-->(A +H B) /\ H ~~>v z) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> y e. B)
Theorem	osumlem7 5536	Lemma for osum 5538.
|- A e. CH   &   |- B e. CH   &   |- B (_ (_|_` A)   =>   |- (A +H B) e. CH
Theorem	osumlem8 5537	Lemma for osum 5538.
|- A e. CH   &   |- B e. CH   =>   |- (B (_ (_|_` A) -> (A +H B) e. CH)
Theorem	osum 5538	If two closed subspaces of a Hilbert space are orthogonal, their subspace sum equals their subspace join. Lemma 3 of [Kalmbach] p. 67. Note that the Axiom of Choice is used for this proof (in osumlem5 5534 and via pjpjtht 5262 in osumlem7 5536).
|- A e. CH   &   |- B e. CH   =>   |- (A (_ (_|_` B) -> (A +H B) = (A vH B))
Theorem	spansnj 5539	The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Proof suggested by Eric Schechter 1-Jun-04.)
|- A e. CH   &   |- B e. H~   =>   |- (A +H (span` {B})) = (A vH (span` {B}))
Theorem	spansnjt 5540	The subspace sum of a closed subspace and a one-dimensional subspace equals their join.
|- ((A e. CH /\ B e. H~) -> (A +H (span` {B})) = (A vH (span` {B})))
Theorem	spansnsclt 5541	The subspace sum of a closed subspace and a one-dimensional subspace is closed.
|- ((A e. CH /\ B e. H~) -> (A +H (span` {B})) e. CH)
Theorem	spansncv 5542	Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153.
|- A e. CH   &   |- B e. CH   &   |- C e. H~   =>   |- ((A (. B /\ B (_ (A vH (span` {C}))) -> B = (A vH (span` {C})))
Theorem	spansncvt 5543	Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153.
|- ((A e. CH /\ B e. CH /\ C e. H~) -> ((A (. B /\ B (_ (A vH (span` {C}))) -> B = (A vH (span` {C})))