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

Metamath Proof Explorer

Theorem trlcolem

Description: Lemma for trlco . (Contributed by NM, 1-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 trlco.l 
 |-  .<_ = ( le ` K )
2 trlco.j 
 |-  .\/ = ( join ` K )
3 trlco.h 
 |-  H = ( LHyp ` K )
4 trlco.t 
 |-  T = ( ( LTrn ` K ) ` W )
5 trlco.r 
 |-  R = ( ( trL ` K ) ` W )
6 trlcolem.m 
 |-  ./\ = ( meet ` K )
7 trlcolem.a 
 |-  A = ( Atoms ` K )
8 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> K e. HL )
9 8 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> K e. Lat )
10 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> P e. A )
11 eqid 
 |-  ( Base ` K ) = ( Base ` K )
12 11 7 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
13 10 12 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> P e. ( Base ` K ) )
14 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( K e. HL /\ W e. H ) )
15 simp2r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> G e. T )
16 1 7 3 4 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ P e. A ) -> ( G ` P ) e. A )
17 14 15 10 16 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( G ` P ) e. A )
18 11 7 atbase 
 |-  ( ( G ` P ) e. A -> ( G ` P ) e. ( Base ` K ) )
19 17 18 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( G ` P ) e. ( Base ` K ) )
20 11 1 2 latlej1 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ ( G ` P ) e. ( Base ` K ) ) -> P .<_ ( P .\/ ( G ` P ) ) )
21 9 13 19 20 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> P .<_ ( P .\/ ( G ` P ) ) )
22 11 2 7 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ ( G ` P ) e. A ) -> ( P .\/ ( G ` P ) ) e. ( Base ` K ) )
23 8 10 17 22 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( G ` P ) ) e. ( Base ` K ) )
24 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> F e. T )
25 11 3 4 ltrncl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( G ` P ) e. ( Base ` K ) ) -> ( F ` ( G ` P ) ) e. ( Base ` K ) )
26 14 24 19 25 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` ( G ` P ) ) e. ( Base ` K ) )
27 11 1 2 latjlej1 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ ( P .\/ ( G ` P ) ) e. ( Base ` K ) /\ ( F ` ( G ` P ) ) e. ( Base ` K ) ) ) -> ( P .<_ ( P .\/ ( G ` P ) ) -> ( P .\/ ( F ` ( G ` P ) ) ) .<_ ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) ) )
28 9 13 23 26 27 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .<_ ( P .\/ ( G ` P ) ) -> ( P .\/ ( F ` ( G ` P ) ) ) .<_ ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) ) )
29 21 28 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( F ` ( G ` P ) ) ) .<_ ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) )
30 11 2 latjcl 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ ( F ` ( G ` P ) ) e. ( Base ` K ) ) -> ( P .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) )
31 9 13 26 30 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) )
32 11 2 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ ( G ` P ) ) e. ( Base ` K ) /\ ( F ` ( G ` P ) ) e. ( Base ` K ) ) -> ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) )
33 9 23 26 32 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) )
34 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> W e. H )
35 11 3 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
36 34 35 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> W e. ( Base ` K ) )
37 11 1 6 latmlem1 
 |-  ( ( K e. Lat /\ ( ( P .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) /\ ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) .<_ ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) .<_ ( ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) ) )
38 9 31 33 36 37 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) .<_ ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) .<_ ( ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) ) )
39 29 38 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) .<_ ( ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) )
40 3 4 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( F o. G ) e. T )
41 14 24 15 40 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( F o. G ) e. T )
42 1 2 6 7 3 4 5 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F o. G ) e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` ( F o. G ) ) = ( ( P .\/ ( ( F o. G ) ` P ) ) ./\ W ) )
43 41 42 syld3an2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` ( F o. G ) ) = ( ( P .\/ ( ( F o. G ) ` P ) ) ./\ W ) )
44 1 7 3 4 ltrncoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ P e. A ) -> ( ( F o. G ) ` P ) = ( F ` ( G ` P ) ) )
45 44 3adant3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F o. G ) ` P ) = ( F ` ( G ` P ) ) )
46 45 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( ( F o. G ) ` P ) ) = ( P .\/ ( F ` ( G ` P ) ) ) )
47 46 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( P .\/ ( ( F o. G ) ` P ) ) ./\ W ) = ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) )
48 43 47 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` ( F o. G ) ) = ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) )
49 1 7 3 4 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) )
50 15 49 syld3an2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) )
51 1 2 6 7 3 4 5 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) ) -> ( R ` F ) = ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) )
52 14 24 50 51 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` F ) = ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) )
53 1 2 6 7 3 4 5 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` G ) = ( ( P .\/ ( G ` P ) ) ./\ W ) )
54 15 53 syld3an2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` G ) = ( ( P .\/ ( G ` P ) ) ./\ W ) )
55 52 54 oveq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( R ` F ) .\/ ( R ` G ) ) = ( ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) .\/ ( ( P .\/ ( G ` P ) ) ./\ W ) ) )
56 1 7 3 4 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( G ` P ) e. A ) -> ( F ` ( G ` P ) ) e. A )
57 14 24 17 56 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` ( G ` P ) ) e. A )
58 11 2 7 hlatjcl 
 |-  ( ( K e. HL /\ ( G ` P ) e. A /\ ( F ` ( G ` P ) ) e. A ) -> ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) )
59 8 17 57 58 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) )
60 11 6 latmcl 
 |-  ( ( K e. Lat /\ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) e. ( Base ` K ) )
61 9 59 36 60 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) e. ( Base ` K ) )
62 11 6 latmcl 
 |-  ( ( K e. Lat /\ ( P .\/ ( G ` P ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ ( G ` P ) ) ./\ W ) e. ( Base ` K ) )
63 9 23 36 62 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( P .\/ ( G ` P ) ) ./\ W ) e. ( Base ` K ) )
64 11 2 latjcom 
 |-  ( ( K e. Lat /\ ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) e. ( Base ` K ) /\ ( ( P .\/ ( G ` P ) ) ./\ W ) e. ( Base ` K ) ) -> ( ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) .\/ ( ( P .\/ ( G ` P ) ) ./\ W ) ) = ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) ) )
65 9 61 63 64 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) .\/ ( ( P .\/ ( G ` P ) ) ./\ W ) ) = ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) ) )
66 11 2 latjcl 
 |-  ( ( K e. Lat /\ ( G ` P ) e. ( Base ` K ) /\ ( F ` ( G ` P ) ) e. ( Base ` K ) ) -> ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) )
67 9 19 26 66 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) )
68 11 1 6 latmle2 
 |-  ( ( K e. Lat /\ ( P .\/ ( G ` P ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ ( G ` P ) ) ./\ W ) .<_ W )
69 9 23 36 68 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( P .\/ ( G ` P ) ) ./\ W ) .<_ W )
70 11 1 2 6 3 lhpmod6i1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( P .\/ ( G ` P ) ) ./\ W ) e. ( Base ` K ) /\ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) ) /\ ( ( P .\/ ( G ` P ) ) ./\ W ) .<_ W ) -> ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) ) = ( ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ) ./\ W ) )
71 14 63 67 69 70 syl121anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) ) = ( ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ) ./\ W ) )
72 11 2 latjass 
 |-  ( ( K e. Lat /\ ( ( ( P .\/ ( G ` P ) ) ./\ W ) e. ( Base ` K ) /\ ( G ` P ) e. ( Base ` K ) /\ ( F ` ( G ` P ) ) e. ( Base ` K ) ) ) -> ( ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) = ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ) )
73 9 63 19 26 72 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) = ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ) )
74 11 1 2 latlej2 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ ( G ` P ) e. ( Base ` K ) ) -> ( G ` P ) .<_ ( P .\/ ( G ` P ) ) )
75 9 13 19 74 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( G ` P ) .<_ ( P .\/ ( G ` P ) ) )
76 11 1 2 6 3 lhpmod2i2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P .\/ ( G ` P ) ) e. ( Base ` K ) /\ ( G ` P ) e. ( Base ` K ) ) /\ ( G ` P ) .<_ ( P .\/ ( G ` P ) ) ) -> ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( G ` P ) ) = ( ( P .\/ ( G ` P ) ) ./\ ( W .\/ ( G ` P ) ) ) )
77 14 23 19 75 76 syl121anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( G ` P ) ) = ( ( P .\/ ( G ` P ) ) ./\ ( W .\/ ( G ` P ) ) ) )
78 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
79 1 2 78 7 3 lhpjat1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) ) -> ( W .\/ ( G ` P ) ) = ( 1. ` K ) )
80 14 50 79 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( W .\/ ( G ` P ) ) = ( 1. ` K ) )
81 80 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( P .\/ ( G ` P ) ) ./\ ( W .\/ ( G ` P ) ) ) = ( ( P .\/ ( G ` P ) ) ./\ ( 1. ` K ) ) )
82 hlol 
 |-  ( K e. HL -> K e. OL )
83 8 82 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> K e. OL )
84 11 6 78 olm11 
 |-  ( ( K e. OL /\ ( P .\/ ( G ` P ) ) e. ( Base ` K ) ) -> ( ( P .\/ ( G ` P ) ) ./\ ( 1. ` K ) ) = ( P .\/ ( G ` P ) ) )
85 83 23 84 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( P .\/ ( G ` P ) ) ./\ ( 1. ` K ) ) = ( P .\/ ( G ` P ) ) )
86 77 81 85 3eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( G ` P ) ) = ( P .\/ ( G ` P ) ) )
87 86 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) = ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) )
88 73 87 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ) = ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) )
89 88 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ) ./\ W ) = ( ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) )
90 71 89 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( P .\/ ( G ` P ) ) ./\ W ) .\/ ( ( ( G ` P ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) ) = ( ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) )
91 55 65 90 3eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( R ` F ) .\/ ( R ` G ) ) = ( ( ( P .\/ ( G ` P ) ) .\/ ( F ` ( G ` P ) ) ) ./\ W ) )
92 39 48 91 3brtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` ( F o. G ) ) .<_ ( ( R ` F ) .\/ ( R ` G ) ) )