P. 230 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 - 22901-23000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	orthin 22901	The intersection of orthogonal subspaces is the zero subspace. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. SH /\ B e. SH ) -> ( A C_ ( _|_ ` B ) -> ( A i^i B ) = 0H ) )
Theorem	ssjo 22902	The lattice join of a subset with its orthocomplement is the whole space. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
|- ( A C_ ~H -> ( A vH ( _|_ ` A ) ) = ~H )
Theorem	shne0i 22903*	A nonzero subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.)
|- A e. SH   =>    |- ( A =/= 0H <-> E. x e. A x =/= 0h )
Theorem	shs0i 22904	Hilbert subspace sum with the zero subspace. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
|- A e. SH   =>    |- ( A +H 0H ) = A
Theorem	shs00i 22905	Two subspaces are zero iff their join is zero. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   =>    |- ( ( A = 0H /\ B = 0H ) <-> ( A +H B ) = 0H )
Theorem	ch0lei 22906	The closed subspace zero is the smallest member of CH. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
|- A e. CH   =>    |- 0H C_ A
Theorem	chle0i 22907	No Hilbert closed subspace is smaller than zero. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.)
|- A e. CH   =>    |- ( A C_ 0H <-> A = 0H )
Theorem	chne0i 22908*	A nonzero closed subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.)
|- A e. CH   =>    |- ( A =/= 0H <-> E. x e. A x =/= 0h )
Theorem	chocini 22909	Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.)
|- A e. CH   =>    |- ( A i^i ( _|_ ` A ) ) = 0H
Theorem	chj0i 22910	Join with lattice zero in CH. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
|- A e. CH   =>    |- ( A vH 0H ) = A
Theorem	chm1i 22911	Meet with lattice one in CH. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
|- A e. CH   =>    |- ( A i^i ~H ) = A
Theorem	chjcli 22912	Closure of CH join. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A vH B ) e. CH
Theorem	chsleji 22913	Subspace sum is smaller than subspace join. Remark in [Kalmbach] p. 65. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A +H B ) C_ ( A vH B )
Theorem	chseli 22914*	Membership in subspace sum. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( C e. ( A +H B ) <-> E. x e. A E. y e. B C = ( x +h y ) )
Theorem	chincli 22915	Closure of Hilbert lattice intersection. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A i^i B ) e. CH
Theorem	chsscon3i 22916	Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A C_ B <-> ( _|_ ` B ) C_ ( _|_ ` A ) )
Theorem	chsscon1i 22917	Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( ( _|_ ` A ) C_ B <-> ( _|_ ` B ) C_ A )
Theorem	chsscon2i 22918	Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A C_ ( _|_ ` B ) <-> B C_ ( _|_ ` A ) )
Theorem	chcon2i 22919	Hilbert lattice contraposition law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A = ( _|_ ` B ) <-> B = ( _|_ ` A ) )
Theorem	chcon1i 22920	Hilbert lattice contraposition law. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( ( _|_ ` A ) = B <-> ( _|_ ` B ) = A )
Theorem	chcon3i 22921	Hilbert lattice contraposition law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A = B <-> ( _|_ ` B ) = ( _|_ ` A ) )
Theorem	chunssji 22922	Union is smaller than CH join. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A u. B ) C_ ( A vH B )
Theorem	chjcomi 22923	Commutative law for join in CH. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A vH B ) = ( B vH A )
Theorem	chub1i 22924	CH join is an upper bound of two elements. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- A C_ ( A vH B )
Theorem	chub2i 22925	CH join is an upper bound of two elements. (Contributed by NM, 5-Nov-2000.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- A C_ ( B vH A )
Theorem	chlubi 22926	Hilbert lattice join is the least upper bound of two elements. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   =>    |- ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C )
Theorem	chlubii 22927	Hilbert lattice join is the least upper bound of two elements (one direction of chlubi 22926). (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   =>    |- ( ( A C_ C /\ B C_ C ) -> ( A vH B ) C_ C )
Theorem	chlej1i 22928	Add join to both sides of a Hilbert lattice ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   =>    |- ( A C_ B -> ( A vH C ) C_ ( B vH C ) )
Theorem	chlej2i 22929	Add join to both sides of a Hilbert lattice ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   =>    |- ( A C_ B -> ( C vH A ) C_ ( C vH B ) )
Theorem	chlej12i 22930	Add join to both sides of a Hilbert lattice ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   &    |- D e. CH   =>    |- ( ( A C_ B /\ C C_ D ) -> ( A vH C ) C_ ( B vH D ) )
Theorem	chlejb1i 22931	Hilbert lattice ordering in terms of join. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A C_ B <-> ( A vH B ) = B )
Theorem	chdmm1i 22932	De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( _|_ ` ( A i^i B ) ) = ( ( _|_ ` A ) vH ( _|_ ` B ) )
Theorem	chdmm2i 22933	De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( _|_ ` ( ( _|_ ` A ) i^i B ) ) = ( A vH ( _|_ ` B ) )
Theorem	chdmm3i 22934	De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( _|_ ` ( A i^i ( _|_ ` B ) ) ) = ( ( _|_ ` A ) vH B )
Theorem	chdmm4i 22935	De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( _|_ ` ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) = ( A vH B )
Theorem	chdmj1i 22936	De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( _|_ ` ( A vH B ) ) = ( ( _|_ ` A ) i^i ( _|_ ` B ) )
Theorem	chdmj2i 22937	De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( _|_ ` ( ( _|_ ` A ) vH B ) ) = ( A i^i ( _|_ ` B ) )
Theorem	chdmj3i 22938	De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( _|_ ` ( A vH ( _|_ ` B ) ) ) = ( ( _|_ ` A ) i^i B )
Theorem	chdmj4i 22939	De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( _|_ ` ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i B )
Theorem	chnlei 22940	Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( -. B C_ A <-> A C. ( A vH B ) )
Theorem	chjassi 22941	Associative law for Hilbert lattice join. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   =>    |- ( ( A vH B ) vH C ) = ( A vH ( B vH C ) )
Theorem	chj00i 22942	Two Hilbert lattice elements are zero iff their join is zero. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( ( A = 0H /\ B = 0H ) <-> ( A vH B ) = 0H )
Theorem	chjoi 22943	The join of a closed subspace and its orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
|- A e. CH   =>    |- ( A vH ( _|_ ` A ) ) = ~H
Theorem	chj1i 22944	Join with Hilbert lattice unit. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.)
|- A e. CH   =>    |- ( A vH ~H ) = ~H
Theorem	chm0i 22945	Meet with Hilbert lattice zero. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.)
|- A e. CH   =>    |- ( A i^i 0H ) = 0H
Theorem	chm0 22946	Meet with Hilbert lattice zero. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
|- ( A e. CH -> ( A i^i 0H ) = 0H )
Theorem	shjshsi 22947	Hilbert lattice join equals the double orthocomplement of subspace sum. (Contributed by NM, 27-Nov-2004.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   =>    |- ( A vH B ) = ( _|_ ` ( _|_ ` ( A +H B ) ) )
Theorem	shjshseli 22948	A closed subspace sum equals Hilbert lattice join. Part of Lemma 31.1.5 of [MaedaMaeda] p. 136. (Contributed by NM, 30-Nov-2004.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   =>    |- ( ( A +H B ) e. CH <-> ( A +H B ) = ( A vH B ) )
Theorem	chne0 22949*	A nonzero closed subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.)
|- ( A e. CH -> ( A =/= 0H <-> E. x e. A x =/= 0h ) )
Theorem	chocin 22950	Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
|- ( A e. CH -> ( A i^i ( _|_ ` A ) ) = 0H )
Theorem	chssoc 22951	A closed subspace less than its orthocomplement is zero. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
|- ( A e. CH -> ( A C_ ( _|_ ` A ) <-> A = 0H ) )
Theorem	chj0 22952	Join with Hilbert lattice zero. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
|- ( A e. CH -> ( A vH 0H ) = A )
Theorem	chslej 22953	Subspace sum is smaller than subspace join. Remark in [Kalmbach] p. 65. (Contributed by NM, 12-Jul-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A +H B ) C_ ( A vH B ) )
Theorem	chincl 22954	Closure of Hilbert lattice intersection. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A i^i B ) e. CH )
Theorem	chsscon3 22955	Hilbert lattice contraposition law. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A C_ B <-> ( _|_ ` B ) C_ ( _|_ ` A ) ) )
Theorem	chsscon1 22956	Hilbert lattice contraposition law. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( ( _|_ ` A ) C_ B <-> ( _|_ ` B ) C_ A ) )
Theorem	chsscon2 22957	Hilbert lattice contraposition law. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A C_ ( _|_ ` B ) <-> B C_ ( _|_ ` A ) ) )
Theorem	chpsscon3 22958	Hilbert lattice contraposition law for strict ordering. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A C. B <-> ( _|_ ` B ) C. ( _|_ ` A ) ) )
Theorem	chpsscon1 22959	Hilbert lattice contraposition law for strict ordering. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( ( _|_ ` A ) C. B <-> ( _|_ ` B ) C. A ) )
Theorem	chpsscon2 22960	Hilbert lattice contraposition law for strict ordering. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A C. ( _|_ ` B ) <-> B C. ( _|_ ` A ) ) )
Theorem	chjcom 22961	Commutative law for Hilbert lattice join. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A vH B ) = ( B vH A ) )
Theorem	chub1 22962	Hilbert lattice join is greater than or equal to its first argument. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> A C_ ( A vH B ) )
Theorem	chub2 22963	Hilbert lattice join is greater than or equal to its second argument. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> A C_ ( B vH A ) )
Theorem	chlub 22964	Hilbert lattice join is the least upper bound of two elements. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C ) )
Theorem	chlej1 22965	Add join to both sides of Hilbert lattice ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
|- ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ A C_ B ) -> ( A vH C ) C_ ( B vH C ) )
Theorem	chlej2 22966	Add join to both sides of Hilbert lattice ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
|- ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ A C_ B ) -> ( C vH A ) C_ ( C vH B ) )
Theorem	chlejb1 22967	Hilbert lattice ordering in terms of join. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A C_ B <-> ( A vH B ) = B ) )
Theorem	chlejb2 22968	Hilbert lattice ordering in terms of join. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A C_ B <-> ( B vH A ) = B ) )
Theorem	chnle 22969	Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( -. B C_ A <-> A C. ( A vH B ) ) )
Theorem	chjo 22970	The join of a closed subspace and its orthocomplement is all of Hilbert space. (Contributed by NM, 31-Oct-2005.) (New usage is discouraged.)
|- ( A e. CH -> ( A vH ( _|_ ` A ) ) = ~H )
Theorem	chabs1 22971	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A vH ( A i^i B ) ) = A )
Theorem	chabs2 22972	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 16-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( A i^i ( A vH B ) ) = A )
Theorem	chabs1i 22973	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A vH ( A i^i B ) ) = A
Theorem	chabs2i 22974	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 16-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A i^i ( A vH B ) ) = A
Theorem	chjidm 22975	Idempotent law for Hilbert lattice join. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
|- ( A e. CH -> ( A vH A ) = A )
Theorem	chjidmi 22976	Idempotent law for Hilbert lattice join. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.)
|- A e. CH   =>    |- ( A vH A ) = A
Theorem	chj12i 22977	A rearrangement of Hilbert lattice join. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   =>    |- ( A vH ( B vH C ) ) = ( B vH ( A vH C ) )
Theorem	chj4i 22978	Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   &    |- D e. CH   =>    |- ( ( A vH B ) vH ( C vH D ) ) = ( ( A vH C ) vH ( B vH D ) )
Theorem	chjjdiri 22979	Hilbert lattice join distributes over itself. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   =>    |- ( ( A vH B ) vH C ) = ( ( A vH C ) vH ( B vH C ) )
Theorem	chdmm1 22980	De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( _|_ ` ( A i^i B ) ) = ( ( _|_ ` A ) vH ( _|_ ` B ) ) )
Theorem	chdmm2 22981	De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( _|_ ` ( ( _|_ ` A ) i^i B ) ) = ( A vH ( _|_ ` B ) ) )
Theorem	chdmm3 22982	De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( _|_ ` ( A i^i ( _|_ ` B ) ) ) = ( ( _|_ ` A ) vH B ) )
Theorem	chdmm4 22983	De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( _|_ ` ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) = ( A vH B ) )
Theorem	chdmj1 22984	De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( _|_ ` ( A vH B ) ) = ( ( _|_ ` A ) i^i ( _|_ ` B ) ) )
Theorem	chdmj2 22985	De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( _|_ ` ( ( _|_ ` A ) vH B ) ) = ( A i^i ( _|_ ` B ) ) )
Theorem	chdmj3 22986	De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( _|_ ` ( A vH ( _|_ ` B ) ) ) = ( ( _|_ ` A ) i^i B ) )
Theorem	chdmj4 22987	De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH ) -> ( _|_ ` ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i B ) )
Theorem	chjass 22988	Associative law for Hilbert lattice join. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A vH B ) vH C ) = ( A vH ( B vH C ) ) )
Theorem	chj12 22989	A rearrangement of Hilbert lattice join. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A vH ( B vH C ) ) = ( B vH ( A vH C ) ) )
Theorem	chj4 22990	Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
|- ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) -> ( ( A vH B ) vH ( C vH D ) ) = ( ( A vH C ) vH ( B vH D ) ) )
Theorem	ledii 22991	An ortholattice is distributive in one ordering direction. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   =>    |- ( ( A i^i B ) vH ( A i^i C ) ) C_ ( A i^i ( B vH C ) )
Theorem	lediri 22992	An ortholattice is distributive in one ordering direction. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   =>    |- ( ( A i^i C ) vH ( B i^i C ) ) C_ ( ( A vH B ) i^i C )
Theorem	lejdii 22993	An ortholattice is distributive in one ordering direction (join version). (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   =>    |- ( A vH ( B i^i C ) ) C_ ( ( A vH B ) i^i ( A vH C ) )
Theorem	lejdiri 22994	An ortholattice is distributive in one ordering direction (join version). (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   =>    |- ( ( A i^i B ) vH C ) C_ ( ( A vH C ) i^i ( B vH C ) )
Theorem	ledi 22995	An ortholattice is distributive in one ordering direction. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A i^i B ) vH ( A i^i C ) ) C_ ( A i^i ( B vH C ) ) )
18.5.4  Span (cont.) and one-dimensional subspaces
Theorem	spansn0 22996	The span of the singleton of the zero vector is the zero subspace. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
|- ( span ` { 0h } ) = 0H
Theorem	span0 22997	The span of the empty set is the zero subspace. Remark 11.6.e of [Schechter] p. 276. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.)
|- ( span ` (/) ) = 0H
Theorem	elspani 22998*	Membership in the span of a subset of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
|- B e. _V   =>    |- ( A C_ ~H -> ( B e. ( span ` A ) <-> A. x e. SH ( A C_ x -> B e. x ) ) )
Theorem	spanuni 22999	The span of a union is the subspace sum of spans. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
|- A C_ ~H   &    |- B C_ ~H   =>    |- ( span ` ( A u. B ) ) = ( ( span ` A ) +H ( span ` B ) )
Theorem	spanun 23000	The span of a union is the subspace sum of spans. (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.)
|- ( ( A C_ ~H /\ B C_ ~H ) -> ( span ` ( A u. B ) ) = ( ( span ` A ) +H ( span ` B ) ) )