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