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 ⊢ 𝐴 ∈ Cℋ
chjcl.2 ⊢ 𝐵 ∈ Cℋ
Assertion chj00i ( ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) ↔ ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ )

Proof

Step Hyp Ref Expression
1 ch0le.1 ⊢ 𝐴 ∈ Cℋ
2 chjcl.2 ⊢ 𝐵 ∈ Cℋ
3 oveq12 ⊢ ( ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( 0ℋ ∨ℋ 0ℋ ) )
4 h0elch ⊢ 0ℋ ∈ Cℋ
5 4 chj0i ⊢ ( 0ℋ ∨ℋ 0ℋ ) = 0ℋ
6 3 5 eqtrdi ⊢ ( ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ )
7 1 2 chub1i ⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 )
8 sseq2 ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ 𝐴 ⊆ 0ℋ ) )
9 7 8 mpbii ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → 𝐴 ⊆ 0ℋ )
10 1 chle0i ⊢ ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ )
11 9 10 sylib ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → 𝐴 = 0ℋ )
12 2 1 chub2i ⊢ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 )
13 sseq2 ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ 𝐵 ⊆ 0ℋ ) )
14 12 13 mpbii ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → 𝐵 ⊆ 0ℋ )
15 2 chle0i ⊢ ( 𝐵 ⊆ 0ℋ ↔ 𝐵 = 0ℋ )
16 14 15 sylib ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → 𝐵 = 0ℋ )
17 11 16 jca ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) )
18 6 17 impbii ⊢ ( ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) ↔ ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ )