P. 284 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28301-28400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	shle0 28301	No subspace is smaller than the zero subspace. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.)
|- ( A e. SH -> ( A C_ 0H <-> A = 0H ) )
Theorem	chle0 28302	No Hilbert lattice element is smaller than zero. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.)
|- ( A e. CH -> ( A C_ 0H <-> A = 0H ) )
Theorem	chnlen0 28303	A Hilbert lattice element that is not a subset of another is nonzero. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.)
|- ( B e. CH -> ( -. A C_ B -> -. A = 0H ) )
Theorem	ch0pss 28304	The zero subspace is a proper subset of nonzero Hilbert lattice elements. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.)
|- ( A e. CH -> ( 0H C. A <-> A =/= 0H ) )
Theorem	orthin 28305	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 28306	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 28307*	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 28308	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 28309	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 28310	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 28311	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 28312*	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 28313	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 28314	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 28315	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 28316	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 28317	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 28318*	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 28319	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 28320	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 28321	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 28322	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 28323	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 28324	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 28325	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 28326	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 28327	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 28328	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 28329	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 28330	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 28331	Hilbert lattice join is the least upper bound of two elements (one direction of chlubi 28330). (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 28332	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 28333	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 28334	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 28335	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 28336	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 28337	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 28338	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 28339	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 28340	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 28341	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 28342	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 28343	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 28344	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 28345	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 28346	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 28347	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 28348	Join with Hilbert lattice unit. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.)
|- A e. CH   =>    |- ( A vH ~H ) = ~H
Theorem	chm0i 28349	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 28350	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 28351	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 28352	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 28353*	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 28354	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 28355	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 28356	Join with Hilbert lattice zero. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
|- ( A e. CH -> ( A vH 0H ) = A )
Theorem	chslej 28357	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 28358	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 28359	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 28360	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 28361	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 28362	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 28363	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 28364	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 28365	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 28366	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 28367	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 28368	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 28369	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 28370	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 28371	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 28372	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 28373	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 28374	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 28375	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 28376	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 28377	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 28378	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 28379	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 28380	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 28381	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 28382	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 28383	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 28384	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 28385	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 28386	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 28387	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 28388	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 28389	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 28390	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 28391	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 28392	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 28393	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 28394	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 28395	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 28396	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 28397	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 28398	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 28399	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 ) ) )
19.5.4  Span (cont.) and one-dimensional subspaces
Theorem	spansn0 28400	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