Metamath Proof Explorer

Theorem atcv0eq

Description: Two atoms covering the zero subspace are equal. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atcv0eq ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 0ℋ ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 atnemeq0 ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) )
2 atelch ⊢ ( 𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ )
3 cvp ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
4 2 3 sylan ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
5 atcv0 ⊢ ( 𝐴 ∈ HAtoms → 0ℋ ⋖ℋ 𝐴 )
6 5 adantr ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → 0ℋ ⋖ℋ 𝐴 )
7 6 biantrurd ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 0ℋ ⋖ℋ 𝐴 ∧ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
8 1 4 7 3bitrd ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ≠ 𝐵 ↔ ( 0ℋ ⋖ℋ 𝐴 ∧ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
9 atelch ⊢ ( 𝐵 ∈ HAtoms → 𝐵 ∈ Cℋ )
10 chjcl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ )
11 h0elch ⊢ 0ℋ ∈ Cℋ
12 cvntr ⊢ ( ( 0ℋ ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) → ( ( 0ℋ ⋖ℋ 𝐴 ∧ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) → ¬ 0ℋ ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
13 11 12 mp3an1 ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) → ( ( 0ℋ ⋖ℋ 𝐴 ∧ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) → ¬ 0ℋ ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
14 10 13 syldan ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 0ℋ ⋖ℋ 𝐴 ∧ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) → ¬ 0ℋ ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
15 2 9 14 syl2an ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ( 0ℋ ⋖ℋ 𝐴 ∧ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) → ¬ 0ℋ ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
16 8 15 sylbid ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ≠ 𝐵 → ¬ 0ℋ ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
17 16 necon4ad ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 0ℋ ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 = 𝐵 ) )
18 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ 𝐵 ) )
19 chjidm ⊢ ( 𝐵 ∈ Cℋ → ( 𝐵 ∨ℋ 𝐵 ) = 𝐵 )
20 9 19 syl ⊢ ( 𝐵 ∈ HAtoms → ( 𝐵 ∨ℋ 𝐵 ) = 𝐵 )
21 18 20 sylan9eq ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ∨ℋ 𝐵 ) = 𝐵 )
22 21 eqcomd ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 ∈ HAtoms ) → 𝐵 = ( 𝐴 ∨ℋ 𝐵 ) )
23 22 eleq1d ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 ∈ HAtoms ) → ( 𝐵 ∈ HAtoms ↔ ( 𝐴 ∨ℋ 𝐵 ) ∈ HAtoms ) )
24 23 ex ⊢ ( 𝐴 = 𝐵 → ( 𝐵 ∈ HAtoms → ( 𝐵 ∈ HAtoms ↔ ( 𝐴 ∨ℋ 𝐵 ) ∈ HAtoms ) ) )
25 24 ibd ⊢ ( 𝐴 = 𝐵 → ( 𝐵 ∈ HAtoms → ( 𝐴 ∨ℋ 𝐵 ) ∈ HAtoms ) )
26 atcv0 ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∈ HAtoms → 0ℋ ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) )
27 25 26 syl6com ⊢ ( 𝐵 ∈ HAtoms → ( 𝐴 = 𝐵 → 0ℋ ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
28 27 adantl ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 = 𝐵 → 0ℋ ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
29 17 28 impbid ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 0ℋ ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ↔ 𝐴 = 𝐵 ) )