mmtheorems103 - Metamath Proof Explorer

Jump to page: Contents + 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-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10658

Statement List for Metamath Proof Explorer - 10201-10300 - Page 103 of 107

Type	Label	Description
Statement
Theorem	mdslmd3 10201	Modular pair conditions that imply the modular pair property in a sublattice. Lemma 1.5.1 of [MaedaMaeda] p. 2.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- D e. CH   =>   |- (((A MH B /\ (A i^i B) MH C) /\ ((A i^i C) (_ D /\ D (_ A)) -> D MH (B i^i C))
Theorem	mdslmd4 10202	Modular pair condition that implies the modular pair property in a sublattice. Lemma 1.5.2 of [MaedaMaeda] p. 2.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- D e. CH   =>   |- ((A MH B /\ ((A i^i B) (_ C /\ C (_ A) /\ ((A i^i B) (_ D /\ D (_ B)) -> C MH D)
Theorem	csmdsym 10203	Cross-symmetry implies M-symmetry. Theorem 1.9.1 of [MaedaMaeda] p. 3.
|- A e. CH   &   |- B e. CH   =>   |- ((A.c e. CH (c MH B -> B MH* c) /\ A MH B) -> B MH A)
Theorem	mdexch 10204	An exchange lemma for modular pairs. Lemma 1.6 of [MaedaMaeda] p. 2.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   =>   |- ((A MH B /\ C MH (A vH B) /\ (C i^i (A vH B)) (_ A) -> ((C vH A) MH B /\ ((C vH A) i^i B) = (A i^i B)))
Theorem	cvmdt 10205	The covering property implies the modular pair property. Lemma 7.5.1 of [MaedaMaeda] p. 31.
|- ((A e. CH /\ B e. CH /\ (A i^i B) <o B) -> A MH B)
Theorem	cvdmdt 10206	The covering property implies the dual modular pair property. Lemma 7.5.2 of [MaedaMaeda] p. 31.
|- ((A e. CH /\ B e. CH /\ B <o (A vH B)) -> A MH* B)
Atoms
Definition	df-at 10207	Define the set of atoms in a Hilbert lattice. An atom is a non-zero element of a lattice such that anything less than it is zero, i.e. it is a smallest non-zero element of the lattice. Definition of atom in [Kalmbach] p. 15. See elat 10208 and elat2 10209 for membership relations.
|- Atoms = {x e. CH | 0H <o x}
Theorem	elat 10208	Atoms in a Hilbert lattice are the elements that cover the zero subspace. Definition of atom in [Kalmbach] p. 15.
|- (A e. Atoms <-> (A e. CH /\ 0H <o A))
Theorem	elat2 10209	Expanded membership relation for the set of atoms, i.e. the predicate "is an atom (of the Hilbert lattice)." An atom is a non-zero element of a lattice such that anything less than it is zero, i.e. it is a smallest non-zero element of the lattice.
|- (A e. Atoms <-> (A e. CH /\ (A =/= 0H /\ A.x e. CH (x (_ A -> (x = A \/ x = 0H)))))
Theorem	elatcv0 10210	A Hilbert lattice element is an atom iff it covers the zero subspace.
|- (A e. CH -> (A e. Atoms <-> 0H <o A))
Theorem	atcv0 10211	An atom covers the zero subspace.
|- (A e. Atoms -> 0H <o A)
Theorem	atssch 10212	Atoms are a subset of the Hilbert lattice.
|- Atoms (_ CH
Theorem	atelch 10213	An atom is a Hilbert lattice element.
|- (A e. Atoms -> A e. CH)
Theorem	atn0 10214	An atom is not the Hilbert lattice zero.
|- (A e. Atoms -> A =/= 0H)
Theorem	atss 10215	A lattice element smaller than an atom is either the atom or zero.
|- ((A e. CH /\ B e. Atoms) -> (A (_ B -> (A = B \/ A = 0H)))
Theorem	atsseq 10216	Two atoms in a subset relationship are equal.
|- ((A e. Atoms /\ B e. Atoms) -> (A (_ B <-> A = B))
Theorem	atcveq0 10217	A Hilbert lattice element covered by an atom must be the zero subspace.
|- ((A e. CH /\ B e. Atoms) -> (A <o B <-> A = 0H))
Theorem	h1dat 10218	A 1-dimensional subspace is an atom.
|- ((A e. H~ /\ A =/= 0h) -> (_|_` (_|_` {A})) e. Atoms)
Theorem	spansnat 10219	The span of the singleton of a vector is an atom.
|- ((A e. H~ /\ A =/= 0h) -> (span` {A}) e. Atoms)
Theorem	sh1dle 10220	A 1-dimensional subspace is less than or equal to any subspace containing its generating vector.
|- ((A e. SH /\ B e. A) -> (_|_` (_|_` {B})) (_ A)
Theorem	ch1dle 10221	A 1-dimensional subspace is less than or equal to any member of CH containing its generating vector.
|- ((A e. CH /\ B e. A) -> (_|_` (_|_` {B})) (_ A)
Theorem	atom1d 10222	The 1-dimensional subspaces of Hilbert space are its atoms. Part of Remark 10.3.5 of [BeltramettiCassinelli] p. 107.
|- (A e. Atoms <-> E.x e. H~ (x =/= 0h /\ A = (span` {x})))
Superposition principle
Theorem	superpos 10223	Superposition Principle. If A and B are distinct atoms, there exists a third atom, distinct from A and B, that is the superposition of A and B. Definition 3.4-3(a) in [MegillPavicic] p. 2345 (PDF p. 8).
|- ((A e. Atoms /\ B e. Atoms /\ A =/= B) -> E.x e. Atoms (x =/= A /\ x =/= B /\ x (_ (A vH B)))
Atoms, exchange and covering properties, atomicity
Theorem	chcv1t 10224	The Hilbert lattice has the covering property. Proposition 1(ii) of [Kalmbach] p. 140 (and its converse).
|- ((A e. CH /\ B e. Atoms) -> (-. B (_ A <-> A <o (A vH B)))
Theorem	chcv2t 10225	The Hilbert lattice has the covering property.
|- ((A e. CH /\ B e. Atoms) -> (A (. (A vH B) <-> A <o (A vH B)))
Theorem	chjatom 10226	The join of a closed subspace and an atom equals their subspace sum. Special case of remark in [Kalmbach] p. 65, stating that if A or B is finite dimensional, then this equality holds.
|- ((A e. CH /\ B e. Atoms) -> (A +H B) = (A vH B))
Theorem	shatomic 10227	The lattice of Hilbert subspaces is atomic, i.e. any non-zero element is greater than or equal to some atom. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70.
|- A e. SH   =>   |- (A =/= 0H -> E.x e. Atoms x (_ A)
Theorem	hatomic 10228	The Hilbert lattice is atomic, i.e. any non-zero element is greater than or equal to some atom. Remark in [Kalmbach] p. 140.
|- A e. CH   =>   |- (A =/= 0H -> E.x e. Atoms x (_ A)
Theorem	hatomict 10229	A Hilbert lattice is atomic, i.e. any non-zero element is greater than or equal to some atom. Remark in [Kalmbach] p. 140. Also Definition 3.4-2 in [MegillPavicic] p. 2345 (PDF p. 8).
|- ((A e. CH /\ A =/= 0H) -> E.x e. Atoms x (_ A)
Theorem	shatomistic 10230	The lattice of Hilbert subspaces is atomistic, i.e. any element is the supremum of its atoms. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70.
|- A e. SH   =>   |- A = (span` U.{x e. Atoms | x (_ A})
Theorem	hatomistic 10231	CH is atomistic, i.e. any element is the supremum of its atoms. Remark in [Kalmbach] p. 140.
|- A e. CH   =>   |- A = ( \/H ` {x e. Atoms | x (_ A})
Theorem	chpssat 10232	Two Hilbert lattice elements in a proper subset relationship imply the existence of an atom less than or equal to one but not the other.
|- A e. CH   &   |- B e. CH   =>   |- (A (. B -> E.x e. Atoms (x (_ B /\ -. x (_ A))
Theorem	chrelat 10233	The Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149.
|- A e. CH   &   |- B e. CH   =>   |- (A (. B -> E.x e. Atoms (A (. (A vH x) /\ (A vH x) (_ B))
Theorem	chrelat2 10234	A consequence of relative atomicity.
|- A e. CH   &   |- B e. CH   =>   |- (-. A (_ B <-> E.x e. Atoms (x (_ A /\ -. x (_ B))
Theorem	cvat 10235	If a Hilbert lattice element covers another, it equals the other joined with some atom. This is a consequence of the relative atomicity of Hilbert space.
|- A e. CH   &   |- B e. CH   =>   |- (A <o B -> E.x e. Atoms (A vH x) = B)
Theorem	cvbr3 10236	An alternate way to express the covering property.
|- A e. CH   &   |- B e. CH   =>   |- (A <o B <-> (A (. B /\ E.x e. Atoms (A vH x) = B))
Theorem	cvexchlem 10237	Lemma for cvexch 10238.
Theorem	cvexch 10238	The Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933.
|- A e. CH   &   |- B e. CH   =>   |- ((A i^i B) <o B <-> A <o (A vH B))
Theorem	chrelat2t 10239	A consequence of relative atomicity.
|- ((A e. CH /\ B e. CH) -> (-. A (_ B <-> E.x e. Atoms (x (_ A /\ -. x (_ B)))
Theorem	chrelat3t 10240	A consequence of relative atomicity.
|- ((A e. CH /\ B e. CH) -> (A (_ B <-> A.x e. Atoms (x (_ A -> x (_ B)))
Theorem	chrelat3 10241	A consequence of the relative atomicity of Hilbert space: the ordering of Hilbert lattice elements is completely determined by the atoms they majorize.
|- A e. CH   &   |- B e. CH   =>   |- (A (_ B <-> A.x e. Atoms (x (_ A -> x (_ B))
Theorem	chrelat4 10242	A consequence of relative atomicity. Extensionality principle: two lattice elements are equal iff they majorize the same atoms.
|- A e. CH   &   |- B e. CH   =>   |- (A = B <-> A.x e. Atoms (x (_ A <-> x (_ B))
Theorem	cvexcht 10243	The Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933.
|- ((A e. CH /\ B e. CH) -> ((A i^i B) <o B <-> A <o (A vH B)))
Theorem	cvp 10244	The Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse.
|- ((A e. CH /\ B e. Atoms) -> ((A i^i B) = 0H <-> A <o (A vH B)))
Theorem	atnssm0 10245	The meet of a Hilbert lattice element and an incomparable atom is the zero subspace.
|- ((A e. CH /\ B e. Atoms) -> (-. B (_ A <-> (A i^i B) = 0H))
Theorem	atnem0 10246	The meet of distinct atoms is the zero subspace.
|- ((A e. Atoms /\ B e. Atoms) -> (-. A = B <-> (A i^i B) = 0H))
Theorem	atssmat 10247	The meet with an atom's superset is the atom.
|- ((A e. Atoms /\ B e. CH) -> (A (_ B <-> (A i^i B) e. Atoms))
Theorem	atcv0eq 10248	Two atoms covering the zero subspace are equal.
|- ((A e. Atoms /\ B e. Atoms) -> (0H <o (A vH B) <-> A = B))
Theorem	atcv1t 10249	Two atoms covering the zero subspace are equal.
|- (((A e. CH /\ B e. Atoms /\ C e. Atoms) /\ A <o (B vH C)) -> (A = 0H <-> B = C))
Theorem	atexcht 10250	The Hilbert lattice satisfies the atom exchange property. Proposition 1(i) of [Kalmbach] p. 140. A version of this theorem related to vector analysis was originally proved by Hermann Grassmann in 1862. Also Definition 3.4-3(b) in [MegillPavicic] p. 2345 (PDF p. 8) (use atnem0 10246 to obtain atom inequality).
|- ((A e. CH /\ B e. Atoms /\ C e. Atoms) -> ((B (_ (A vH C) /\ (A i^i B) = 0H) -> C (_ (A vH B)))
Theorem	atoml 10251	An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition 3.2.17 of [PtakPulmannova] p. 66.
|- A e. CH   =>   |- (B e. Atoms -> ((A vH B) i^i (_|_` A)) e. (Atoms u. {0H}))
Theorem	atoml2 10252	An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition P8(ii) of [BeltramettiCassinelli1] p. 400.
|- A e. CH   =>   |- ((B e. Atoms /\ -. B (_ A) -> ((A vH B) i^i (_|_` A)) e. Atoms)
Theorem	atord 10253	An ordering law for a Hilbert lattice atom and a commuting subspace.
|- A e. CH   =>   |- ((B e. Atoms /\ A C_H B) -> (B (_ A \/ B (_ (_|_` A)))
Theorem	atcvatlem 10254	Lemma for atcvat 10255.