Metamath Proof Explorer

Theorem atcvrj0

Description: Two atoms covering the zero subspace are equal. ( atcv1 analog.) (Contributed by NM, 29-Nov-2011)

Ref Expression
Hypotheses atcvrj0.b 
|- B = ( Base ` K )
atcvrj0.j 
|- .\/ = ( join ` K )
atcvrj0.z 
|- .0. = ( 0. ` K )
atcvrj0.c 
|- C = (
atcvrj0.a 
|- A = ( Atoms ` K )
Assertion atcvrj0 
|- ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ X C ( P .\/ Q ) ) -> ( X = .0. <-> P = Q ) )

Proof

Step Hyp Ref Expression
1 atcvrj0.b 
 |-  B = ( Base ` K )
2 atcvrj0.j 
 |-  .\/ = ( join ` K )
3 atcvrj0.z 
 |-  .0. = ( 0. ` K )
4 atcvrj0.c 
 |-  C = (
5 atcvrj0.a 
 |-  A = ( Atoms ` K )
6 breq1 
 |-  ( X = .0. -> ( X C ( P .\/ Q ) <-> .0. C ( P .\/ Q ) ) )
7 6 biimpd 
 |-  ( X = .0. -> ( X C ( P .\/ Q ) -> .0. C ( P .\/ Q ) ) )
8 7 adantl 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ X = .0. ) -> ( X C ( P .\/ Q ) -> .0. C ( P .\/ Q ) ) )
9 2 3 4 5 atcvr0eq 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( .0. C ( P .\/ Q ) <-> P = Q ) )
10 9 3adant3r1 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( .0. C ( P .\/ Q ) <-> P = Q ) )
11 10 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ X = .0. ) -> ( .0. C ( P .\/ Q ) <-> P = Q ) )
12 8 11 sylibd 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ X = .0. ) -> ( X C ( P .\/ Q ) -> P = Q ) )
13 12 ex 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X = .0. -> ( X C ( P .\/ Q ) -> P = Q ) ) )
14 13 com23 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X C ( P .\/ Q ) -> ( X = .0. -> P = Q ) ) )
15 14 3impia 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ X C ( P .\/ Q ) ) -> ( X = .0. -> P = Q ) )
16 oveq1 
 |-  ( P = Q -> ( P .\/ Q ) = ( Q .\/ Q ) )
17 16 breq2d 
 |-  ( P = Q -> ( X C ( P .\/ Q ) <-> X C ( Q .\/ Q ) ) )
18 17 biimpac 
 |-  ( ( X C ( P .\/ Q ) /\ P = Q ) -> X C ( Q .\/ Q ) )
19 simpr3 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> Q e. A )
20 2 5 hlatjidm 
 |-  ( ( K e. HL /\ Q e. A ) -> ( Q .\/ Q ) = Q )
21 19 20 syldan 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( Q .\/ Q ) = Q )
22 21 breq2d 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X C ( Q .\/ Q ) <-> X C Q ) )
23 hlatl 
 |-  ( K e. HL -> K e. AtLat )
24 23 adantr 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> K e. AtLat )
25 simpr1 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> X e. B )
26 eqid 
 |-  ( le ` K ) = ( le ` K )
27 1 26 3 4 5 atcvreq0 
 |-  ( ( K e. AtLat /\ X e. B /\ Q e. A ) -> ( X C Q <-> X = .0. ) )
28 24 25 19 27 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X C Q <-> X = .0. ) )
29 28 biimpd 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X C Q -> X = .0. ) )
30 22 29 sylbid 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X C ( Q .\/ Q ) -> X = .0. ) )
31 18 30 syl5 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( X C ( P .\/ Q ) /\ P = Q ) -> X = .0. ) )
32 31 expd 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X C ( P .\/ Q ) -> ( P = Q -> X = .0. ) ) )
33 32 3impia 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ X C ( P .\/ Q ) ) -> ( P = Q -> X = .0. ) )
34 15 33 impbid 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ X C ( P .\/ Q ) ) -> ( X = .0. <-> P = Q ) )