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