Metamath Proof Explorer

Theorem lhpat3

Description: There is only one atom under both P .\/ Q and co-atom W . (Contributed by NM, 21-Nov-2012)

Ref Expression
Hypotheses lhpat.l 
|- .<_ = ( le ` K )
lhpat.j 
|- .\/ = ( join ` K )
lhpat.m 
|- ./\ = ( meet ` K )
lhpat.a 
|- A = ( Atoms ` K )
lhpat.h 
|- H = ( LHyp ` K )
lhpat2.r 
|- R = ( ( P .\/ Q ) ./\ W )
Assertion lhpat3 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> ( -. S .<_ W <-> S =/= R ) )

Proof

Step Hyp Ref Expression
1 lhpat.l 
 |-  .<_ = ( le ` K )
2 lhpat.j 
 |-  .\/ = ( join ` K )
3 lhpat.m 
 |-  ./\ = ( meet ` K )
4 lhpat.a 
 |-  A = ( Atoms ` K )
5 lhpat.h 
 |-  H = ( LHyp ` K )
6 lhpat2.r 
 |-  R = ( ( P .\/ Q ) ./\ W )
7 simpl3r 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> S .<_ ( P .\/ Q ) )
8 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> S .<_ W )
9 simp1ll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> K e. HL )
10 9 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> K e. Lat )
11 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> S e. A )
12 eqid 
 |-  ( Base ` K ) = ( Base ` K )
13 12 4 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
14 11 13 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> S e. ( Base ` K ) )
15 simp1rl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> P e. A )
16 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> Q e. A )
17 12 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
18 9 15 16 17 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
19 simp1lr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> W e. H )
20 12 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
21 19 20 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> W e. ( Base ` K ) )
22 12 1 3 latlem12 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( S .<_ ( P .\/ Q ) /\ S .<_ W ) <-> S .<_ ( ( P .\/ Q ) ./\ W ) ) )
23 10 14 18 21 22 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> ( ( S .<_ ( P .\/ Q ) /\ S .<_ W ) <-> S .<_ ( ( P .\/ Q ) ./\ W ) ) )
24 23 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> ( ( S .<_ ( P .\/ Q ) /\ S .<_ W ) <-> S .<_ ( ( P .\/ Q ) ./\ W ) ) )
25 7 8 24 mpbi2and 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> S .<_ ( ( P .\/ Q ) ./\ W ) )
26 25 6 breqtrrdi 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> S .<_ R )
27 9 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> K e. HL )
28 hlatl 
 |-  ( K e. HL -> K e. AtLat )
29 27 28 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> K e. AtLat )
30 simpl2r 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> S e. A )
31 simpl1l 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> ( K e. HL /\ W e. H ) )
32 simpl1r 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> ( P e. A /\ -. P .<_ W ) )
33 simpl2l 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> Q e. A )
34 simpl3l 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> P =/= Q )
35 1 2 3 4 5 6 lhpat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> R e. A )
36 31 32 33 34 35 syl112anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> R e. A )
37 1 4 atcmp 
 |-  ( ( K e. AtLat /\ S e. A /\ R e. A ) -> ( S .<_ R <-> S = R ) )
38 29 30 36 37 syl3anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> ( S .<_ R <-> S = R ) )
39 26 38 mpbid 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) /\ S .<_ W ) -> S = R )
40 39 ex 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> ( S .<_ W -> S = R ) )
41 12 1 3 latmle2 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ W ) .<_ W )
42 10 18 21 41 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> ( ( P .\/ Q ) ./\ W ) .<_ W )
43 6 42 eqbrtrid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> R .<_ W )
44 breq1 
 |-  ( S = R -> ( S .<_ W <-> R .<_ W ) )
45 43 44 syl5ibrcom 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> ( S = R -> S .<_ W ) )
46 40 45 impbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> ( S .<_ W <-> S = R ) )
47 46 necon3bbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> ( -. S .<_ W <-> S =/= R ) )