Metamath Proof Explorer

Theorem cdlemg42

Description: Part of proof of Lemma G of Crawley p. 116, first line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013)

Ref Expression
Hypotheses cdlemg42.l 
|- .<_ = ( le ` K )
cdlemg42.j 
|- .\/ = ( join ` K )
cdlemg42.a 
|- A = ( Atoms ` K )
cdlemg42.h 
|- H = ( LHyp ` K )
cdlemg42.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemg42.r 
|- R = ( ( trL ` K ) ` W )
Assertion cdlemg42 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> -. ( G ` P ) .<_ ( P .\/ ( F ` P ) ) )

Proof

Step Hyp Ref Expression
1 cdlemg42.l 
 |-  .<_ = ( le ` K )
2 cdlemg42.j 
 |-  .\/ = ( join ` K )
3 cdlemg42.a 
 |-  A = ( Atoms ` K )
4 cdlemg42.h 
 |-  H = ( LHyp ` K )
5 cdlemg42.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 cdlemg42.r 
 |-  R = ( ( trL ` K ) ` W )
7 simp33 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( R ` F ) =/= ( R ` G ) )
8 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> K e. HL )
9 simp31l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> P e. A )
10 9 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> P e. A )
11 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( K e. HL /\ W e. H ) )
12 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> F e. T )
13 1 3 4 5 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. A ) -> ( F ` P ) e. A )
14 11 12 9 13 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( F ` P ) e. A )
15 14 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( F ` P ) e. A )
16 1 2 3 hlatlej1 
 |-  ( ( K e. HL /\ P e. A /\ ( F ` P ) e. A ) -> P .<_ ( P .\/ ( F ` P ) ) )
17 8 10 15 16 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> P .<_ ( P .\/ ( F ` P ) ) )
18 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( G ` P ) .<_ ( P .\/ ( F ` P ) ) )
19 8 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> K e. Lat )
20 eqid 
 |-  ( Base ` K ) = ( Base ` K )
21 20 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
22 10 21 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> P e. ( Base ` K ) )
23 simp2r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> G e. T )
24 1 3 4 5 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ P e. A ) -> ( G ` P ) e. A )
25 11 23 9 24 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( G ` P ) e. A )
26 25 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( G ` P ) e. A )
27 20 3 atbase 
 |-  ( ( G ` P ) e. A -> ( G ` P ) e. ( Base ` K ) )
28 26 27 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( G ` P ) e. ( Base ` K ) )
29 20 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ ( F ` P ) e. A ) -> ( P .\/ ( F ` P ) ) e. ( Base ` K ) )
30 8 10 15 29 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( P .\/ ( F ` P ) ) e. ( Base ` K ) )
31 20 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ ( G ` P ) e. ( Base ` K ) /\ ( P .\/ ( F ` P ) ) e. ( Base ` K ) ) ) -> ( ( P .<_ ( P .\/ ( F ` P ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) <-> ( P .\/ ( G ` P ) ) .<_ ( P .\/ ( F ` P ) ) ) )
32 19 22 28 30 31 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( ( P .<_ ( P .\/ ( F ` P ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) <-> ( P .\/ ( G ` P ) ) .<_ ( P .\/ ( F ` P ) ) ) )
33 17 18 32 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( P .\/ ( G ` P ) ) .<_ ( P .\/ ( F ` P ) ) )
34 simpl32 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( G ` P ) =/= P )
35 34 necomd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> P =/= ( G ` P ) )
36 1 2 3 ps-1 
 |-  ( ( K e. HL /\ ( P e. A /\ ( G ` P ) e. A /\ P =/= ( G ` P ) ) /\ ( P e. A /\ ( F ` P ) e. A ) ) -> ( ( P .\/ ( G ` P ) ) .<_ ( P .\/ ( F ` P ) ) <-> ( P .\/ ( G ` P ) ) = ( P .\/ ( F ` P ) ) ) )
37 8 10 26 35 10 15 36 syl132anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( ( P .\/ ( G ` P ) ) .<_ ( P .\/ ( F ` P ) ) <-> ( P .\/ ( G ` P ) ) = ( P .\/ ( F ` P ) ) ) )
38 33 37 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( P .\/ ( G ` P ) ) = ( P .\/ ( F ` P ) ) )
39 38 oveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( ( P .\/ ( G ` P ) ) ( meet ` K ) W ) = ( ( P .\/ ( F ` P ) ) ( meet ` K ) W ) )
40 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( K e. HL /\ W e. H ) )
41 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> G e. T )
42 simpl31 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( P e. A /\ -. P .<_ W ) )
43 eqid 
 |-  ( meet ` K ) = ( meet ` K )
44 1 2 43 3 4 5 6 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` G ) = ( ( P .\/ ( G ` P ) ) ( meet ` K ) W ) )
45 40 41 42 44 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( R ` G ) = ( ( P .\/ ( G ` P ) ) ( meet ` K ) W ) )
46 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> F e. T )
47 1 2 43 3 4 5 6 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` F ) = ( ( P .\/ ( F ` P ) ) ( meet ` K ) W ) )
48 40 46 42 47 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( R ` F ) = ( ( P .\/ ( F ` P ) ) ( meet ` K ) W ) )
49 39 45 48 3eqtr4rd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) /\ ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) -> ( R ` F ) = ( R ` G ) )
50 49 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( ( G ` P ) .<_ ( P .\/ ( F ` P ) ) -> ( R ` F ) = ( R ` G ) ) )
51 50 necon3ad 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( ( R ` F ) =/= ( R ` G ) -> -. ( G ` P ) .<_ ( P .\/ ( F ` P ) ) ) )
52 7 51 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> -. ( G ` P ) .<_ ( P .\/ ( F ` P ) ) )