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