Metamath Proof Explorer

Theorem cdleme5

Description: Part of proof of Lemma E in Crawley p. 113. G represents f_s(r). We show r \/ f_s(r)) = p \/ q at the top of p. 114. (Contributed by NM, 7-Jun-2012)

Ref Expression
Hypotheses cdleme4.l 
|- .<_ = ( le ` K )
cdleme4.j 
|- .\/ = ( join ` K )
cdleme4.m 
|- ./\ = ( meet ` K )
cdleme4.a 
|- A = ( Atoms ` K )
cdleme4.h 
|- H = ( LHyp ` K )
cdleme4.u 
|- U = ( ( P .\/ Q ) ./\ W )
cdleme4.f 
|- F = ( ( S .\/ U ) ./\ ( Q .\/ ( ( P .\/ S ) ./\ W ) ) )
cdleme4.g 
|- G = ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) )
Assertion cdleme5 
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( R .\/ G ) = ( P .\/ Q ) )

Proof

Step Hyp Ref Expression
1 cdleme4.l 
 |-  .<_ = ( le ` K )
2 cdleme4.j 
 |-  .\/ = ( join ` K )
3 cdleme4.m 
 |-  ./\ = ( meet ` K )
4 cdleme4.a 
 |-  A = ( Atoms ` K )
5 cdleme4.h 
 |-  H = ( LHyp ` K )
6 cdleme4.u 
 |-  U = ( ( P .\/ Q ) ./\ W )
7 cdleme4.f 
 |-  F = ( ( S .\/ U ) ./\ ( Q .\/ ( ( P .\/ S ) ./\ W ) ) )
8 cdleme4.g 
 |-  G = ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) )
9 8 oveq2i 
 |-  ( R .\/ G ) = ( R .\/ ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) )
10 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> K e. HL )
11 simp23l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> R e. A )
12 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> P e. A )
13 simp22 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> Q e. A )
14 eqid 
 |-  ( Base ` K ) = ( Base ` K )
15 14 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
16 10 12 13 15 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
17 10 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> K e. Lat )
18 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( K e. HL /\ W e. H ) )
19 simp3ll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> S e. A )
20 1 2 3 4 5 6 7 14 cdleme1b 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ S e. A ) ) -> F e. ( Base ` K ) )
21 18 12 13 19 20 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> F e. ( Base ` K ) )
22 14 2 4 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) e. ( Base ` K ) )
23 10 11 19 22 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( R .\/ S ) e. ( Base ` K ) )
24 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> W e. H )
25 14 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
26 24 25 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> W e. ( Base ` K ) )
27 14 3 latmcl 
 |-  ( ( K e. Lat /\ ( R .\/ S ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( R .\/ S ) ./\ W ) e. ( Base ` K ) )
28 17 23 26 27 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ W ) e. ( Base ` K ) )
29 14 2 latjcl 
 |-  ( ( K e. Lat /\ F e. ( Base ` K ) /\ ( ( R .\/ S ) ./\ W ) e. ( Base ` K ) ) -> ( F .\/ ( ( R .\/ S ) ./\ W ) ) e. ( Base ` K ) )
30 17 21 28 29 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( F .\/ ( ( R .\/ S ) ./\ W ) ) e. ( Base ` K ) )
31 simp3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> R .<_ ( P .\/ Q ) )
32 14 1 2 3 4 atmod3i1 
 |-  ( ( K e. HL /\ ( R e. A /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) e. ( Base ` K ) ) /\ R .<_ ( P .\/ Q ) ) -> ( R .\/ ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) ) = ( ( P .\/ Q ) ./\ ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) ) )
33 10 11 16 30 31 32 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( R .\/ ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) ) = ( ( P .\/ Q ) ./\ ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) ) )
34 14 4 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
35 19 34 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> S e. ( Base ` K ) )
36 14 1 2 latlej2 
 |-  ( ( K e. Lat /\ S e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( P .\/ Q ) .<_ ( S .\/ ( P .\/ Q ) ) )
37 17 35 16 36 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( P .\/ Q ) .<_ ( S .\/ ( P .\/ Q ) ) )
38 14 4 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
39 11 38 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> R e. ( Base ` K ) )
40 14 2 latj12 
 |-  ( ( K e. Lat /\ ( R e. ( Base ` K ) /\ F e. ( Base ` K ) /\ S e. ( Base ` K ) ) ) -> ( R .\/ ( F .\/ S ) ) = ( F .\/ ( R .\/ S ) ) )
41 17 39 21 35 40 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( R .\/ ( F .\/ S ) ) = ( F .\/ ( R .\/ S ) ) )
42 1 2 3 4 5 6 14 cdleme0aa 
 |-  ( ( ( K e. HL /\ W e. H ) /\ P e. A /\ Q e. A ) -> U e. ( Base ` K ) )
43 18 12 13 42 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> U e. ( Base ` K ) )
44 14 2 latj12 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ R e. ( Base ` K ) /\ U e. ( Base ` K ) ) ) -> ( S .\/ ( R .\/ U ) ) = ( R .\/ ( S .\/ U ) ) )
45 17 35 39 43 44 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( S .\/ ( R .\/ U ) ) = ( R .\/ ( S .\/ U ) ) )
46 1 2 3 4 5 6 cdleme4 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ R .<_ ( P .\/ Q ) ) -> ( P .\/ Q ) = ( R .\/ U ) )
47 46 3adant3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( P .\/ Q ) = ( R .\/ U ) )
48 47 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( S .\/ ( P .\/ Q ) ) = ( S .\/ ( R .\/ U ) ) )
49 14 2 latjcom 
 |-  ( ( K e. Lat /\ F e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> ( F .\/ S ) = ( S .\/ F ) )
50 17 21 35 49 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( F .\/ S ) = ( S .\/ F ) )
51 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( S e. A /\ -. S .<_ W ) )
52 1 2 3 4 5 6 7 cdleme1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( S .\/ F ) = ( S .\/ U ) )
53 18 12 13 51 52 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( S .\/ F ) = ( S .\/ U ) )
54 50 53 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( F .\/ S ) = ( S .\/ U ) )
55 54 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( R .\/ ( F .\/ S ) ) = ( R .\/ ( S .\/ U ) ) )
56 45 48 55 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( S .\/ ( P .\/ Q ) ) = ( R .\/ ( F .\/ S ) ) )
57 1 2 4 hlatlej1 
 |-  ( ( K e. HL /\ R e. A /\ S e. A ) -> R .<_ ( R .\/ S ) )
58 10 11 19 57 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> R .<_ ( R .\/ S ) )
59 14 1 2 3 4 atmod3i1 
 |-  ( ( K e. HL /\ ( R e. A /\ ( R .\/ S ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ R .<_ ( R .\/ S ) ) -> ( R .\/ ( ( R .\/ S ) ./\ W ) ) = ( ( R .\/ S ) ./\ ( R .\/ W ) ) )
60 10 11 23 26 58 59 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( R .\/ ( ( R .\/ S ) ./\ W ) ) = ( ( R .\/ S ) ./\ ( R .\/ W ) ) )
61 simp23r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> -. R .<_ W )
62 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
63 1 2 62 4 5 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( R .\/ W ) = ( 1. ` K ) )
64 18 11 61 63 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( R .\/ W ) = ( 1. ` K ) )
65 64 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ ( R .\/ W ) ) = ( ( R .\/ S ) ./\ ( 1. ` K ) ) )
66 hlol 
 |-  ( K e. HL -> K e. OL )
67 10 66 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> K e. OL )
68 14 3 62 olm11 
 |-  ( ( K e. OL /\ ( R .\/ S ) e. ( Base ` K ) ) -> ( ( R .\/ S ) ./\ ( 1. ` K ) ) = ( R .\/ S ) )
69 67 23 68 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ ( 1. ` K ) ) = ( R .\/ S ) )
70 65 69 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ ( R .\/ W ) ) = ( R .\/ S ) )
71 60 70 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( R .\/ ( ( R .\/ S ) ./\ W ) ) = ( R .\/ S ) )
72 71 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( F .\/ ( R .\/ ( ( R .\/ S ) ./\ W ) ) ) = ( F .\/ ( R .\/ S ) ) )
73 41 56 72 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( S .\/ ( P .\/ Q ) ) = ( F .\/ ( R .\/ ( ( R .\/ S ) ./\ W ) ) ) )
74 14 2 latj12 
 |-  ( ( K e. Lat /\ ( F e. ( Base ` K ) /\ R e. ( Base ` K ) /\ ( ( R .\/ S ) ./\ W ) e. ( Base ` K ) ) ) -> ( F .\/ ( R .\/ ( ( R .\/ S ) ./\ W ) ) ) = ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) )
75 17 21 39 28 74 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( F .\/ ( R .\/ ( ( R .\/ S ) ./\ W ) ) ) = ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) )
76 73 75 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( S .\/ ( P .\/ Q ) ) = ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) )
77 37 76 breqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( P .\/ Q ) .<_ ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) )
78 14 2 latjcl 
 |-  ( ( K e. Lat /\ R e. ( Base ` K ) /\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) e. ( Base ` K ) ) -> ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) e. ( Base ` K ) )
79 17 39 30 78 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) e. ( Base ` K ) )
80 14 1 3 latleeqm1 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) .<_ ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) <-> ( ( P .\/ Q ) ./\ ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) ) = ( P .\/ Q ) ) )
81 17 16 79 80 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( ( P .\/ Q ) .<_ ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) <-> ( ( P .\/ Q ) ./\ ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) ) = ( P .\/ Q ) ) )
82 77 81 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( ( P .\/ Q ) ./\ ( R .\/ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) ) = ( P .\/ Q ) )
83 33 82 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( R .\/ ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) ) = ( P .\/ Q ) )
84 9 83 syl5eq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) ) ) -> ( R .\/ G ) = ( P .\/ Q ) )