Metamath Proof Explorer

Theorem atcv1

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

Ref Expression
Assertion atcv1 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms ∧ C ∈ HAtoms ∧ A ⋖ ℋ B ∨ ℋ C → A = 0 ℋ ↔ B = C

Proof

Step Hyp Ref Expression
1 breq1 ⊢ A = 0 ℋ → A ⋖ ℋ B ∨ ℋ C ↔ 0 ℋ ⋖ ℋ B ∨ ℋ C
2 atcv0eq ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → 0 ℋ ⋖ ℋ B ∨ ℋ C ↔ B = C
3 1 2 sylan9bbr ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ A = 0 ℋ → A ⋖ ℋ B ∨ ℋ C ↔ B = C
4 3 biimpd ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ A = 0 ℋ → A ⋖ ℋ B ∨ ℋ C → B = C
5 4 ex ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → A = 0 ℋ → A ⋖ ℋ B ∨ ℋ C → B = C
6 5 com23 ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → A ⋖ ℋ B ∨ ℋ C → A = 0 ℋ → B = C
7 6 3adant1 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms ∧ C ∈ HAtoms → A ⋖ ℋ B ∨ ℋ C → A = 0 ℋ → B = C
8 7 imp ⊢ A ∈ C ℋ ∧ B ∈ HAtoms ∧ C ∈ HAtoms ∧ A ⋖ ℋ B ∨ ℋ C → A = 0 ℋ → B = C
9 oveq1 ⊢ B = C → B ∨ ℋ C = C ∨ ℋ C
10 atelch ⊢ C ∈ HAtoms → C ∈ C ℋ
11 chjidm ⊢ C ∈ C ℋ → C ∨ ℋ C = C
12 10 11 syl ⊢ C ∈ HAtoms → C ∨ ℋ C = C
13 9 12 sylan9eq ⊢ B = C ∧ C ∈ HAtoms → B ∨ ℋ C = C
14 13 eqcomd ⊢ B = C ∧ C ∈ HAtoms → C = B ∨ ℋ C
15 14 eleq1d ⊢ B = C ∧ C ∈ HAtoms → C ∈ HAtoms ↔ B ∨ ℋ C ∈ HAtoms
16 15 ex ⊢ B = C → C ∈ HAtoms → C ∈ HAtoms ↔ B ∨ ℋ C ∈ HAtoms
17 16 ibd ⊢ B = C → C ∈ HAtoms → B ∨ ℋ C ∈ HAtoms
18 17 impcom ⊢ C ∈ HAtoms ∧ B = C → B ∨ ℋ C ∈ HAtoms
19 atcveq0 ⊢ A ∈ C ℋ ∧ B ∨ ℋ C ∈ HAtoms → A ⋖ ℋ B ∨ ℋ C ↔ A = 0 ℋ
20 18 19 sylan2 ⊢ A ∈ C ℋ ∧ C ∈ HAtoms ∧ B = C → A ⋖ ℋ B ∨ ℋ C ↔ A = 0 ℋ
21 20 biimpd ⊢ A ∈ C ℋ ∧ C ∈ HAtoms ∧ B = C → A ⋖ ℋ B ∨ ℋ C → A = 0 ℋ
22 21 exp32 ⊢ A ∈ C ℋ → C ∈ HAtoms → B = C → A ⋖ ℋ B ∨ ℋ C → A = 0 ℋ
23 22 com34 ⊢ A ∈ C ℋ → C ∈ HAtoms → A ⋖ ℋ B ∨ ℋ C → B = C → A = 0 ℋ
24 23 imp ⊢ A ∈ C ℋ ∧ C ∈ HAtoms → A ⋖ ℋ B ∨ ℋ C → B = C → A = 0 ℋ
25 24 3adant2 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms ∧ C ∈ HAtoms → A ⋖ ℋ B ∨ ℋ C → B = C → A = 0 ℋ
26 25 imp ⊢ A ∈ C ℋ ∧ B ∈ HAtoms ∧ C ∈ HAtoms ∧ A ⋖ ℋ B ∨ ℋ C → B = C → A = 0 ℋ
27 8 26 impbid ⊢ A ∈ C ℋ ∧ B ∈ HAtoms ∧ C ∈ HAtoms ∧ A ⋖ ℋ B ∨ ℋ C → A = 0 ℋ ↔ B = C