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 ⊢ A ∈ HAtoms ∧ B ∈ HAtoms → 0 ℋ ⋖ ℋ A ∨ ℋ B ↔ A = B

Proof

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