This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chj00i

Description: Two Hilbert lattice elements are zero iff their join is zero. (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 
|- A e. CH
chjcl.2 
|- B e. CH
Assertion chj00i 
|- ( ( A = 0H /\ B = 0H ) <-> ( A vH B ) = 0H )

Proof

Step Hyp Ref Expression
1 ch0le.1 
 |-  A e. CH
2 chjcl.2 
 |-  B e. CH
3 oveq12 
 |-  ( ( A = 0H /\ B = 0H ) -> ( A vH B ) = ( 0H vH 0H ) )
4 h0elch 
 |-  0H e. CH
5 4 chj0i 
 |-  ( 0H vH 0H ) = 0H
6 3 5 eqtrdi 
 |-  ( ( A = 0H /\ B = 0H ) -> ( A vH B ) = 0H )
7 1 2 chub1i 
 |-  A C_ ( A vH B )
8 sseq2 
 |-  ( ( A vH B ) = 0H -> ( A C_ ( A vH B ) <-> A C_ 0H ) )
9 7 8 mpbii 
 |-  ( ( A vH B ) = 0H -> A C_ 0H )
10 1 chle0i 
 |-  ( A C_ 0H <-> A = 0H )
11 9 10 sylib 
 |-  ( ( A vH B ) = 0H -> A = 0H )
12 2 1 chub2i 
 |-  B C_ ( A vH B )
13 sseq2 
 |-  ( ( A vH B ) = 0H -> ( B C_ ( A vH B ) <-> B C_ 0H ) )
14 12 13 mpbii 
 |-  ( ( A vH B ) = 0H -> B C_ 0H )
15 2 chle0i 
 |-  ( B C_ 0H <-> B = 0H )
16 14 15 sylib 
 |-  ( ( A vH B ) = 0H -> B = 0H )
17 11 16 jca 
 |-  ( ( A vH B ) = 0H -> ( A = 0H /\ B = 0H ) )
18 6 17 impbii 
 |-  ( ( A = 0H /\ B = 0H ) <-> ( A vH B ) = 0H )