P. 293 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29201-29300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	atcv0 29201	An atom covers the zero subspace. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
|- ( A e. HAtoms -> 0H <oH A )
Theorem	atssch 29202	Atoms are a subset of the Hilbert lattice. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.)
|- HAtoms C_ CH
Theorem	atelch 29203	An atom is a Hilbert lattice element. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
|- ( A e. HAtoms -> A e. CH )
Theorem	atne0 29204	An atom is not the Hilbert lattice zero. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
|- ( A e. HAtoms -> A =/= 0H )
Theorem	atss 29205	A lattice element smaller than an atom is either the atom or zero. (Contributed by NM, 25-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. HAtoms ) -> ( A C_ B -> ( A = B \/ A = 0H ) ) )
Theorem	atsseq 29206	Two atoms in a subset relationship are equal. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A C_ B <-> A = B ) )
Theorem	atcveq0 29207	A Hilbert lattice element covered by an atom must be the zero subspace. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. HAtoms ) -> ( A <oH B <-> A = 0H ) )
Theorem	h1da 29208	A 1-dimensional subspace is an atom. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.)
|- ( ( A e. ~H /\ A =/= 0h ) -> ( _|_ ` ( _|_ ` { A } ) ) e. HAtoms )
Theorem	spansna 29209	The span of the singleton of a vector is an atom. (Contributed by NM, 18-Dec-2004.) (New usage is discouraged.)
|- ( ( A e. ~H /\ A =/= 0h ) -> ( span ` { A } ) e. HAtoms )
Theorem	sh1dle 29210	A 1-dimensional subspace is less than or equal to any subspace containing its generating vector. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.)
|- ( ( A e. SH /\ B e. A ) -> ( _|_ ` ( _|_ ` { B } ) ) C_ A )
Theorem	ch1dle 29211	A 1-dimensional subspace is less than or equal to any member of CH containing its generating vector. (Contributed by NM, 30-May-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. A ) -> ( _|_ ` ( _|_ ` { B } ) ) C_ A )
Theorem	atom1d 29212*	The 1-dimensional subspaces of Hilbert space are its atoms. Part of Remark 10.3.5 of [BeltramettiCassinelli] p. 107. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
|- ( A e. HAtoms <-> E. x e. ~H ( x =/= 0h /\ A = ( span ` { x } ) ) )
19.8.3  Superposition principle
Theorem	superpos 29213*	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 [MegPav2000] p. 2345 (PDF p. 8). (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.)
|- ( ( A e. HAtoms /\ B e. HAtoms /\ A =/= B ) -> E. x e. HAtoms ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) )
19.8.4  Atoms, exchange and covering properties, atomicity
Theorem	chcv1 29214	The Hilbert lattice has the covering property. Proposition 1(ii) of [Kalmbach] p. 140 (and its converse). (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. HAtoms ) -> ( -. B C_ A <-> A <oH ( A vH B ) ) )
Theorem	chcv2 29215	The Hilbert lattice has the covering property. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. HAtoms ) -> ( A C. ( A vH B ) <-> A <oH ( A vH B ) ) )
Theorem	chjatom 29216	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. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. HAtoms ) -> ( A +H B ) = ( A vH B ) )
Theorem	shatomici 29217*	The lattice of Hilbert subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.)
|- A e. SH   =>    |- ( A =/= 0H -> E. x e. HAtoms x C_ A )
Theorem	hatomici 29218*	The Hilbert lattice is atomic, i.e. any nonzero element is greater than or equal to some atom. Remark in [Kalmbach] p. 140. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.)
|- A e. CH   =>    |- ( A =/= 0H -> E. x e. HAtoms x C_ A )
Theorem	hatomic 29219*	A Hilbert lattice is atomic, i.e. any nonzero element is greater than or equal to some atom. Remark in [Kalmbach] p. 140. Also Definition 3.4-2 in [MegPav2000] p. 2345 (PDF p. 8). (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ A =/= 0H ) -> E. x e. HAtoms x C_ A )
Theorem	shatomistici 29220*	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. (Contributed by NM, 26-Nov-2004.) (New usage is discouraged.)
|- A e. SH   =>    |- A = ( span ` U. { x e. HAtoms | x C_ A } )
Theorem	hatomistici 29221*	CH is atomistic, i.e. any element is the supremum of its atoms. Remark in [Kalmbach] p. 140. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.)
|- A e. CH   =>    |- A = ( \/H ` { x e. HAtoms | x C_ A } )
Theorem	chpssati 29222*	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. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A C. B -> E. x e. HAtoms ( x C_ B /\ -. x C_ A ) )
Theorem	chrelati 29223*	The Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A C. B -> E. x e. HAtoms ( A C. ( A vH x ) /\ ( A vH x ) C_ B ) )
Theorem	chrelat2i 29224*	A consequence of relative atomicity. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( -. A C_ B <-> E. x e. HAtoms ( x C_ A /\ -. x C_ B ) )
Theorem	cvati 29225*	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. (Contributed by NM, 30-Nov-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A <oH B -> E. x e. HAtoms ( A vH x ) = B )
Theorem	cvbr4i 29226*	An alternate way to express the covering property. (Contributed by NM, 30-Nov-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A <oH B <-> ( A C. B /\ E. x e. HAtoms ( A vH x ) = B ) )
Theorem	cvexchlem 29227	Lemma for cvexchi 29228. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( ( A i^i B ) <oH B -> A <oH ( A vH B ) )
Theorem	cvexchi 29228	The Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( ( A i^i B ) <oH B <-> A <oH ( A vH B ) )
Theorem	chrelat2 29229*	A consequence of relative atomicity. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( -. A C_ B <-> E. x e. HAtoms ( x C_ A /\ -. x C_ B ) ) )
Theorem	chrelat3 29230*	A consequence of relative atomicity. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A C_ B <-> A. x e. HAtoms ( x C_ A -> x C_ B ) ) )
Theorem	chrelat3i 29231*	A consequence of the relative atomicity of Hilbert space: the ordering of Hilbert lattice elements is completely determined by the atoms they majorize. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A C_ B <-> A. x e. HAtoms ( x C_ A -> x C_ B ) )
Theorem	chrelat4i 29232*	A consequence of relative atomicity. Extensionality principle: two lattice elements are equal iff they majorize the same atoms. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A = B <-> A. x e. HAtoms ( x C_ A <-> x C_ B ) )
Theorem	cvexch 29233	The Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( ( A i^i B ) <oH B <-> A <oH ( A vH B ) ) )
Theorem	cvp 29234	The Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. HAtoms ) -> ( ( A i^i B ) = 0H <-> A <oH ( A vH B ) ) )
Theorem	atnssm0 29235	The meet of a Hilbert lattice element and an incomparable atom is the zero subspace. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. HAtoms ) -> ( -. B C_ A <-> ( A i^i B ) = 0H ) )
Theorem	atnemeq0 29236	The meet of distinct atoms is the zero subspace. (Contributed by NM, 25-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A =/= B <-> ( A i^i B ) = 0H ) )
Theorem	atssma 29237	The meet with an atom's superset is the atom. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
|- ( ( A e. HAtoms /\ B e. CH ) -> ( A C_ B <-> ( A i^i B ) e. HAtoms ) )
Theorem	atcv0eq 29238	Two atoms covering the zero subspace are equal. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( 0H <oH ( A vH B ) <-> A = B ) )
Theorem	atcv1 29239	Two atoms covering the zero subspace are equal. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
|- ( ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) /\ A <oH ( B vH C ) ) -> ( A = 0H <-> B = C ) )
Theorem	atexch 29240	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 [MegPav2000] p. 2345 (PDF p. 8) (use atnemeq0 29236 to obtain atom inequality). (Contributed by NM, 27-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) -> C C_ ( A vH B ) ) )
Theorem	atomli 29241	An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition 3.2.17 of [PtakPulmannova] p. 66. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
|- A e. CH   =>    |- ( B e. HAtoms -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. (HAtoms u. { 0H } ) )
Theorem	atoml2i 29242	An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition P8(ii) of [BeltramettiCassinelli1] p. 400. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- ( ( B e. HAtoms /\ -. B C_ A ) -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms )
Theorem	atordi 29243	An ordering law for a Hilbert lattice atom and a commuting subspace. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- ( ( B e. HAtoms /\ A C_H B ) -> ( B C_ A \/ B C_ ( _|_ ` A ) ) )
Theorem	atcvatlem 29244	Lemma for atcvati 29245. (Contributed by NM, 27-Jun-2004.) (New usage is discouraged.)
|- A e. CH   =>    |- ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( A =/= 0H /\ A C. ( B vH C ) ) ) -> ( -. B C_ A -> A e. HAtoms ) )
Theorem	atcvati 29245	A nonzero Hilbert lattice element less than the join of two atoms is an atom. (Contributed by NM, 28-Jun-2004.) (New usage is discouraged.)
|- A e. CH   =>    |- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( A =/= 0H /\ A C. ( B vH C ) ) -> A e. HAtoms ) )
Theorem	atcvat2i 29246	A Hilbert lattice element covered by the join of two distinct atoms is an atom. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
|- A e. CH   =>    |- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ A <oH ( B vH C ) ) -> A e. HAtoms ) )
Theorem	atord 29247	An ordering law for a Hilbert lattice atom and a commuting subspace. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. HAtoms /\ A C_H B ) -> ( B C_ A \/ B C_ ( _|_ ` A ) ) )
Theorem	atcvat2 29248	A Hilbert lattice element covered by the join of two distinct atoms is an atom. (Contributed by NM, 29-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ A <oH ( B vH C ) ) -> A e. HAtoms ) )
19.8.5  Irreducibility
Theorem	chirredlem1 29249*	Lemma for chirredi 29253. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- ( ( ( p e. HAtoms /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( p i^i ( _|_ ` r ) ) = 0H )
Theorem	chirredlem2 29250*	Lemma for chirredi 29253. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( ( _|_ ` r ) i^i ( p vH q ) ) = q )
Theorem	chirredlem3 29251*	Lemma for chirredi 29253. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
|- A e. CH   &    |- ( x e. CH -> A C_H x )   =>    |- ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) ) /\ ( r e. HAtoms /\ r C_ ( p vH q ) ) ) -> ( r C_ A -> r = p ) )
Theorem	chirredlem4 29252*	Lemma for chirredi 29253. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
|- A e. CH   &    |- ( x e. CH -> A C_H x )   =>    |- ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) ) /\ ( r e. HAtoms /\ r C_ ( p vH q ) ) ) -> ( r = p \/ r = q ) )
Theorem	chirredi 29253*	The Hilbert lattice is irreducible: any element that commutes with all elements must be zero or one. Theorem 14.8.4 of [BeltramettiCassinelli] p. 166. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
|- A e. CH   &    |- ( x e. CH -> A C_H x )   =>    |- ( A = 0H \/ A = ~H )
Theorem	chirred 29254*	The Hilbert lattice is irreducible: any element that commutes with all elements must be zero or one. Theorem 14.8.4 of [BeltramettiCassinelli] p. 166. (Contributed by NM, 16-Jun-2006.) (New usage is discouraged.)
|- ( ( A e. CH /\ A. x e. CH A C_H x ) -> ( A = 0H \/ A = ~H ) )
19.8.6  Atoms (cont.)
Theorem	atcvat3i 29255	A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
|- A e. CH   =>    |- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) -> ( A i^i ( B vH C ) ) e. HAtoms ) )
Theorem	atcvat4i 29256*	A condition implying existence of an atom with the properties shown. Lemma 3.2.20 of [PtakPulmannova] p. 68. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
|- A e. CH   =>    |- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( A =/= 0H /\ B C_ ( A vH C ) ) -> E. x e. HAtoms ( x C_ A /\ B C_ ( C vH x ) ) ) )
Theorem	atdmd 29257	Two Hilbert lattice elements have the dual modular pair property if the first is an atom. Theorem 7.6(c) of [MaedaMaeda] p. 31. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. HAtoms /\ B e. CH ) -> A MH* B )
Theorem	atmd 29258	Two Hilbert lattice elements have the modular pair property if the first is an atom. Theorem 7.6(b) of [MaedaMaeda] p. 31. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. HAtoms /\ B e. CH ) -> A MH B )
Theorem	atmd2 29259	Two Hilbert lattice elements have the dual modular pair property if the second is an atom. Part of Exercise 6 of [Kalmbach] p. 103. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. HAtoms ) -> A MH B )
Theorem	atabsi 29260	Absorption of an incomparable atom. Similar to Exercise 7.1 of [MaedaMaeda] p. 34. (Contributed by NM, 15-Jul-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( C e. HAtoms -> ( -. C C_ ( A vH B ) -> ( ( A vH C ) i^i B ) = ( A i^i B ) ) )
Theorem	atabs2i 29261	Absorption of an incomparable atom. (Contributed by NM, 18-Jul-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( C e. HAtoms -> ( -. C C_ ( A vH B ) -> ( ( A vH C ) i^i ( A vH B ) ) = A ) )
19.8.7  Modular symmetry
Theorem	mdsymlem1 29262*	Lemma for mdsymi 29270. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C = ( A vH p )   =>    |- ( ( ( p e. CH /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> p C_ A )
Theorem	mdsymlem2 29263*	Lemma for mdsymi 29270. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C = ( A vH p )   =>    |- ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> ( B =/= 0H -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) )
Theorem	mdsymlem3 29264*	Lemma for mdsymi 29270. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C = ( A vH p )   =>    |- ( ( ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) /\ p C_ ( A vH B ) ) /\ A =/= 0H ) -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) )
Theorem	mdsymlem4 29265*	Lemma for mdsymi 29270. This is the forward direction of Lemma 4(i) of [Maeda] p. 168. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C = ( A vH p )   =>    |- ( p e. HAtoms -> ( ( B MH* A /\ ( ( A =/= 0H /\ B =/= 0H ) /\ p C_ ( A vH B ) ) ) -> E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) )
Theorem	mdsymlem5 29266*	Lemma for mdsymi 29270. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C = ( A vH p )   =>    |- ( ( q e. HAtoms /\ r e. HAtoms ) -> ( -. q = p -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( ( ( c e. CH /\ A C_ c ) /\ p e. HAtoms ) -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) ) ) )
Theorem	mdsymlem6 29267*	Lemma for mdsymi 29270. This is the converse direction of Lemma 4(i) of [Maeda] p. 168, and is based on the proof of Theorem 1(d) to (e) of [Maeda] p. 167. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C = ( A vH p )   =>    |- ( A. p e. HAtoms ( p C_ ( A vH B ) -> E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) -> B MH* A )
Theorem	mdsymlem7 29268*	Lemma for mdsymi 29270. Lemma 4(i) of [Maeda] p. 168. Note that Maeda's 1965 definition of dual modular pair has reversed arguments compared to the later (1970) definition given in Remark 29.6 of [MaedaMaeda] p. 130, which is the one that we use. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C = ( A vH p )   =>    |- ( ( A =/= 0H /\ B =/= 0H ) -> ( B MH* A <-> A. p e. HAtoms ( p C_ ( A vH B ) -> E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
Theorem	mdsymlem8 29269*	Lemma for mdsymi 29270. Lemma 4(ii) of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C = ( A vH p )   =>    |- ( ( A =/= 0H /\ B =/= 0H ) -> ( B MH* A <-> A MH* B ) )
Theorem	mdsymi 29270	M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A MH B <-> B MH A )
Theorem	mdsym 29271	M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> B MH A ) )
Theorem	dmdsym 29272	Dual M-symmetry of the Hilbert lattice. (Contributed by NM, 25-Jul-2007.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> B MH* A ) )
Theorem	atdmd2 29273	Two Hilbert lattice elements have the dual modular pair property if the second is an atom. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. HAtoms ) -> A MH* B )
Theorem	sumdmdii 29274	If the subspace sum of two Hilbert lattice elements is closed, then the elements are a dual modular pair. Remark in [MaedaMaeda] p. 139. (Contributed by NM, 12-Jul-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( ( A +H B ) = ( A vH B ) -> A MH* B )
Theorem	cmmdi 29275	Commuting subspaces form a modular pair. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A C_H B -> A MH B )
Theorem	cmdmdi 29276	Commuting subspaces form a dual modular pair. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A C_H B -> A MH* B )
Theorem	sumdmdlem 29277	Lemma for sumdmdi 29279. The span of vector C not in the subspace sum is "trimmed off." (Contributed by NM, 18-Dec-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( ( C e. ~H /\ -. C e. ( A +H B ) ) -> ( ( B +H ( span ` { C } ) ) i^i A ) = ( B i^i A ) )
Theorem	sumdmdlem2 29278*	Lemma for sumdmdi 29279. (Contributed by NM, 23-Dec-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( A +H B ) = ( A vH B ) )
Theorem	sumdmdi 29279	The subspace sum of two Hilbert lattice elements is closed iff the elements are a dual modular pair. Theorem 2 of [Holland] p. 1519. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( ( A +H B ) = ( A vH B ) <-> A MH* B )
Theorem	dmdbr4ati 29280*	Dual modular pair property in terms of atoms. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A MH* B <-> A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) )
Theorem	dmdbr5ati 29281*	Dual modular pair property in terms of atoms. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A MH* B <-> A. x e. HAtoms ( x C_ ( A vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
Theorem	dmdbr6ati 29282*	Dual modular pair property in terms of atoms. The modular law takes the form of the shearing identity. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A MH* B <-> A. x e. HAtoms ( ( A vH B ) i^i x ) = ( ( ( ( x vH B ) i^i A ) vH B ) i^i x ) )
Theorem	dmdbr7ati 29283*	Dual modular pair property in terms of atoms. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A MH* B <-> A. x e. HAtoms ( ( A vH B ) i^i x ) C_ ( ( ( x vH B ) i^i A ) vH B ) )
Theorem	mdoc1i 29284	Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- A MH ( _|_ ` A )
Theorem	mdoc2i 29285	Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- ( _|_ ` A ) MH A
Theorem	dmdoc1i 29286	Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- A MH* ( _|_ ` A )
Theorem	dmdoc2i 29287	Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- ( _|_ ` A ) MH* A
Theorem	mdcompli 29288	A condition equivalent to the modular pair property. Part of proof of Theorem 1.14 of [MaedaMaeda] p. 4. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A MH B <-> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH ( B i^i ( _|_ ` ( A i^i B ) ) ) )
Theorem	dmdcompli 29289	A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A MH* B <-> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* ( B i^i ( _|_ ` ( A i^i B ) ) ) )
Theorem	mddmdin0i 29290*	If dual modular implies modular whenever meet is zero, then dual modular implies modular for arbitrary lattice elements. This theorem is needed for the remark after Lemma 7 of [Holland] p. 1524 to hold. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- A. x e. CH A. y e. CH ( ( x MH* y /\ ( x i^i y ) = 0H ) -> x MH y )   =>    |- ( A MH* B -> A MH B )
Theorem	cdjreui 29291*	A member of the sum of disjoint subspaces has a unique decomposition. Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 20-May-2005.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   =>    |- ( ( C e. ( A +H B ) /\ ( A i^i B ) = 0H ) -> E! x e. A E. y e. B C = ( x +h y ) )
Theorem	cdj1i 29292*	Two ways to express " A and B are completely disjoint subspaces." (1) => (2) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 21-May-2005.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   =>    |- ( E. w e. RR ( 0 < w /\ A. y e. A A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) ) -> E. x e. RR ( 0 < x /\ A. y e. A A. z e. B ( ( normh ` y ) = 1 -> x <_ ( normh ` ( y -h z ) ) ) ) )
Theorem	cdj3lem1 29293*	A property of " A and B are completely disjoint subspaces." Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   =>    |- ( E. x e. RR ( 0 < x /\ A. y e. A A. z e. B ( ( normh ` y ) + ( normh ` z ) ) <_ ( x x. ( normh ` ( y +h z ) ) ) ) -> ( A i^i B ) = 0H )
Theorem	cdj3lem2 29294*	Lemma for cdj3i 29300. Value of the first-component function S. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- S = ( x e. ( A +H B ) |-> ( iota_ z e. A E. w e. B x = ( z +h w ) ) )   =>    |- ( ( C e. A /\ D e. B /\ ( A i^i B ) = 0H ) -> ( S ` ( C +h D ) ) = C )
Theorem	cdj3lem2a 29295*	Lemma for cdj3i 29300. Closure of the first-component function S. (Contributed by NM, 25-May-2005.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- S = ( x e. ( A +H B ) |-> ( iota_ z e. A E. w e. B x = ( z +h w ) ) )   =>    |- ( ( C e. ( A +H B ) /\ ( A i^i B ) = 0H ) -> ( S ` C ) e. A )
Theorem	cdj3lem2b 29296*	Lemma for cdj3i 29300. The first-component function S is bounded if the subspaces are completely disjoint. (Contributed by NM, 26-May-2005.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- S = ( x e. ( A +H B ) |-> ( iota_ z e. A E. w e. B x = ( z +h w ) ) )   =>    |- ( E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) -> E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) )
Theorem	cdj3lem3 29297*	Lemma for cdj3i 29300. Value of the second-component function T. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- T = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )   =>    |- ( ( C e. A /\ D e. B /\ ( A i^i B ) = 0H ) -> ( T ` ( C +h D ) ) = D )
Theorem	cdj3lem3a 29298*	Lemma for cdj3i 29300. Closure of the second-component function T. (Contributed by NM, 26-May-2005.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- T = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )   =>    |- ( ( C e. ( A +H B ) /\ ( A i^i B ) = 0H ) -> ( T ` C ) e. B )
Theorem	cdj3lem3b 29299*	Lemma for cdj3i 29300. The second-component function T is bounded if the subspaces are completely disjoint. (Contributed by NM, 31-May-2005.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- T = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )   =>    |- ( E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) -> E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) )
Theorem	cdj3i 29300*	Two ways to express " A and B are completely disjoint subspaces." (1) <=> (3) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 1-Jun-2005.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- S = ( x e. ( A +H B ) |-> ( iota_ z e. A E. w e. B x = ( z +h w ) ) )   &    |- T = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )   &    |- ( ph <-> E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) )   &    |- ( ps <-> E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) )   =>    |- ( E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) <-> ( ( A i^i B ) = 0H /\ ph /\ ps ) )