P. 239 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 23801-23900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	atne0 23801	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 23802	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 23803	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 23804	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 23805	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 23806	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 23807	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 23808	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 23809*	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 } ) ) )
18.8.3  Superposition principle
Theorem	superpos 23810*	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 ) ) )
18.8.4  Atoms, exchange and covering properties, atomicity
Theorem	chcv1 23811	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 23812	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 23813	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 23814*	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 23815*	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 23816*	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 23817*	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 23818*	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 23819*	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 23820*	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 23821*	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 23822*	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 23823*	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 23824	Lemma for cvexchi 23825. (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 23825	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 23826*	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 23827*	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 23828*	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 23829*	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 23830	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 23831	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 23832	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 23833	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 23834	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 23835	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 23836	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 23837	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 23833 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 23838	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 23839	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 23840	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 23841	Lemma for atcvati 23842. (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 23842	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 23843	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 23844	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 23845	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 ) )
18.8.5  Irreducibility
Theorem	chirredlem1 23846*	Lemma for chirredi 23850. (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 23847*	Lemma for chirredi 23850. (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 23848*	Lemma for chirredi 23850. (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 23849*	Lemma for chirredi 23850. (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 23850*	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 23851*	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 ) )
18.8.6  Atoms (cont.)
Theorem	atcvat3i 23852	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 23853*	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 23854	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 23855	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 23856	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 23857	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 23858	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 ) )
18.8.7  Modular symmetry
Theorem	mdsymlem1 23859*	Lemma for mdsymi 23867. (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 23860*	Lemma for mdsymi 23867. (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 23861*	Lemma for mdsymi 23867. (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 23862*	Lemma for mdsymi 23867. 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 23863*	Lemma for mdsymi 23867. (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 23864*	Lemma for mdsymi 23867. 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 23865*	Lemma for mdsymi 23867. 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 23866*	Lemma for mdsymi 23867. 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 23867	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 23868	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 23869	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 23870	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 23871	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 23872	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 23873	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 23874	Lemma for sumdmdi 23876. 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 23875*	Lemma for sumdmdi 23876. (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 23876	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 23877*	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 23878*	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 23879*	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 23880*	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 23881	Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- A MH ( _|_ ` A )
Theorem	mdoc2i 23882	Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- ( _|_ ` A ) MH A
Theorem	dmdoc1i 23883	Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- A MH* ( _|_ ` A )
Theorem	dmdoc2i 23884	Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- ( _|_ ` A ) MH* A
Theorem	mdcompli 23885	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 23886	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 23887*	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 23888*	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 23889*	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 23890*	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 23891*	Lemma for cdj3i 23897. 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 23892*	Lemma for cdj3i 23897. 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 23893*	Lemma for cdj3i 23897. 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 23894*	Lemma for cdj3i 23897. 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 23895*	Lemma for cdj3i 23897. 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 23896*	Lemma for cdj3i 23897. 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 23897*	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 ) )
PART 19  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
19.1  Mathboxes for user contributions
19.1.1  Mathbox guidelines
Theorem	mathbox 23898	(This theorem is a dummy placeholder for these guidelines. The name of this theorem, "mathbox", is hard-coded into the Metamath program to identify the start of the mathbox section for web page generation.) A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm. Mathboxes are provided to help keep your work synchronized with changes in set.mm, but they shouldn't be depended on as a permanent archive. If you want to preserve your original contribution, it is your responsibility to keep your own copy of it along with the version of set.mm that works with it. Guidelines: 1. If at all possible, please use only 0-ary class constants for new definitions, for example as in df-div 9634. 2. Try to follow the style of the rest of set.mm. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of wrapping comment lines and indentation conventions. All mathbox content will be on public display and should hopefully reflect the overall quality of the website. 3. Before submitting a revised mathbox, please make sure it verifies against the current set.mm. 4. Mathboxes should be independent i.e. the proofs should verify with all other mathboxes removed. If you need a theorem from another mathbox, that is fine (and encouraged), but let me know, so I can move the theorem to the main section. One way avoid undesired accidental use of other mathbox theorems is to develop your mathbox using a modified set.mm that has mathboxes removed. Notes: 1. I may decide to move some theorems to the main part of set.mm for general use. In that case, an author acknowledgment will be added to the description of the theorem. 2. I may make changes to mathboxes to maintain the overall quality of set.mm. Normally I will let you know if a change might impact what you are working on. 3. If you use theorems from another user's mathbox, I don't provide assurance that they are based on correct or consistent $a statements. (If you find such a problem, please let me know so it can be corrected.) (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.)
|- x = x
19.2  Mathbox for Stefan Allan
Theorem	foo3 23899	A theorem about the universal class. (Contributed by Stefan Allan, 9-Dec-2008.)
|- ph   =>    |- _V = { x | ph }
Theorem	xfree 23900	A partial converse to 19.9t 1789. (Contributed by Stefan Allan, 21-Dec-2008.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- ( A. x ( ph -> A. x ph ) <-> A. x ( E. x ph -> ph ) )