This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. HAtoms /\ B e. HAtoms ) -> ( 0H  A = B ) )

Proof

Step Hyp Ref Expression
1 atnemeq0 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A =/= B <-> ( A i^i B ) = 0H ) )
2 atelch 
 |-  ( A e. HAtoms -> A e. CH )
3 cvp 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( ( A i^i B ) = 0H <-> A
4 2 3 sylan 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( ( A i^i B ) = 0H <-> A
5 atcv0 
 |-  ( A e. HAtoms -> 0H
6 5 adantr 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> 0H
7 6 biantrurd 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A  ( 0H
8 1 4 7 3bitrd 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A =/= B <-> ( 0H
9 atelch 
 |-  ( B e. HAtoms -> B e. CH )
10 chjcl 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A vH B ) e. CH )
11 h0elch 
 |-  0H e. CH
12 cvntr 
 |-  ( ( 0H e. CH /\ A e. CH /\ ( A vH B ) e. CH ) -> ( ( 0H  -. 0H
13 11 12 mp3an1 
 |-  ( ( A e. CH /\ ( A vH B ) e. CH ) -> ( ( 0H  -. 0H
14 10 13 syldan 
 |-  ( ( A e. CH /\ B e. CH ) -> ( ( 0H  -. 0H
15 2 9 14 syl2an 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( ( 0H  -. 0H
16 8 15 sylbid 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A =/= B -> -. 0H
17 16 necon4ad 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( 0H  A = B ) )
18 oveq1 
 |-  ( A = B -> ( A vH B ) = ( B vH B ) )
19 chjidm 
 |-  ( B e. CH -> ( B vH B ) = B )
20 9 19 syl 
 |-  ( B e. HAtoms -> ( B vH B ) = B )
21 18 20 sylan9eq 
 |-  ( ( A = B /\ B e. HAtoms ) -> ( A vH B ) = B )
22 21 eqcomd 
 |-  ( ( A = B /\ B e. HAtoms ) -> B = ( A vH B ) )
23 22 eleq1d 
 |-  ( ( A = B /\ B e. HAtoms ) -> ( B e. HAtoms <-> ( A vH B ) e. HAtoms ) )
24 23 ex 
 |-  ( A = B -> ( B e. HAtoms -> ( B e. HAtoms <-> ( A vH B ) e. HAtoms ) ) )
25 24 ibd 
 |-  ( A = B -> ( B e. HAtoms -> ( A vH B ) e. HAtoms ) )
26 atcv0 
 |-  ( ( A vH B ) e. HAtoms -> 0H
27 25 26 syl6com 
 |-  ( B e. HAtoms -> ( A = B -> 0H
28 27 adantl 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A = B -> 0H
29 17 28 impbid 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( 0H  A = B ) )