Metamath Proof Explorer

Theorem cdleme9

Description: Part of proof of Lemma E in Crawley p. 113, 2nd paragraph on p. 114. C and F represent s_1 and f(s) respectively. In their notation, we prove f(s) \/ s_1 = q \/ s_1. (Contributed by NM, 10-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 cdleme9.l 
 |-  .<_ = ( le ` K )
2 cdleme9.j 
 |-  .\/ = ( join ` K )
3 cdleme9.m 
 |-  ./\ = ( meet ` K )
4 cdleme9.a 
 |-  A = ( Atoms ` K )
5 cdleme9.h 
 |-  H = ( LHyp ` K )
6 cdleme9.u 
 |-  U = ( ( P .\/ Q ) ./\ W )
7 cdleme9.f 
 |-  F = ( ( S .\/ U ) ./\ ( Q .\/ ( ( P .\/ S ) ./\ W ) ) )
8 cdleme9.c 
 |-  C = ( ( P .\/ S ) ./\ W )
9 1 2 3 4 5 6 7 8 cdleme3d 
 |-  F = ( ( S .\/ U ) ./\ ( Q .\/ C ) )
10 9 oveq1i 
 |-  ( F .\/ C ) = ( ( ( S .\/ U ) ./\ ( Q .\/ C ) ) .\/ C )
11 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> K e. HL )
12 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( K e. HL /\ W e. H ) )
13 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( P e. A /\ -. P .<_ W ) )
14 simp23l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> S e. A )
15 11 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> K e. Lat )
16 eqid 
 |-  ( Base ` K ) = ( Base ` K )
17 16 4 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
18 14 17 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> S e. ( Base ` K ) )
19 simp21l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> P e. A )
20 16 4 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
21 19 20 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> P e. ( Base ` K ) )
22 simp22 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> Q e. A )
23 16 4 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
24 22 23 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> Q e. ( Base ` K ) )
25 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> -. S .<_ ( P .\/ Q ) )
26 16 1 2 latnlej1l 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) /\ -. S .<_ ( P .\/ Q ) ) -> S =/= P )
27 26 necomd 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) /\ -. S .<_ ( P .\/ Q ) ) -> P =/= S )
28 15 18 21 24 25 27 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> P =/= S )
29 1 2 3 4 5 8 cdleme9a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( S e. A /\ P =/= S ) ) -> C e. A )
30 12 13 14 28 29 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> C e. A )
31 1 2 3 4 5 6 16 cdleme0aa 
 |-  ( ( ( K e. HL /\ W e. H ) /\ P e. A /\ Q e. A ) -> U e. ( Base ` K ) )
32 12 19 22 31 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> U e. ( Base ` K ) )
33 16 2 latjcl 
 |-  ( ( K e. Lat /\ S e. ( Base ` K ) /\ U e. ( Base ` K ) ) -> ( S .\/ U ) e. ( Base ` K ) )
34 15 18 32 33 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( S .\/ U ) e. ( Base ` K ) )
35 16 2 4 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ C e. A ) -> ( Q .\/ C ) e. ( Base ` K ) )
36 11 22 30 35 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( Q .\/ C ) e. ( Base ` K ) )
37 1 2 4 hlatlej2 
 |-  ( ( K e. HL /\ Q e. A /\ C e. A ) -> C .<_ ( Q .\/ C ) )
38 11 22 30 37 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> C .<_ ( Q .\/ C ) )
39 16 1 2 3 4 atmod4i1 
 |-  ( ( K e. HL /\ ( C e. A /\ ( S .\/ U ) e. ( Base ` K ) /\ ( Q .\/ C ) e. ( Base ` K ) ) /\ C .<_ ( Q .\/ C ) ) -> ( ( ( S .\/ U ) ./\ ( Q .\/ C ) ) .\/ C ) = ( ( ( S .\/ U ) .\/ C ) ./\ ( Q .\/ C ) ) )
40 11 30 34 36 38 39 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( ( S .\/ U ) ./\ ( Q .\/ C ) ) .\/ C ) = ( ( ( S .\/ U ) .\/ C ) ./\ ( Q .\/ C ) ) )
41 8 oveq2i 
 |-  ( S .\/ C ) = ( S .\/ ( ( P .\/ S ) ./\ W ) )
42 16 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ S e. A ) -> ( P .\/ S ) e. ( Base ` K ) )
43 11 19 14 42 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( P .\/ S ) e. ( Base ` K ) )
44 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> W e. H )
45 16 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
46 44 45 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> W e. ( Base ` K ) )
47 1 2 4 hlatlej2 
 |-  ( ( K e. HL /\ P e. A /\ S e. A ) -> S .<_ ( P .\/ S ) )
48 11 19 14 47 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> S .<_ ( P .\/ S ) )
49 16 1 2 3 4 atmod3i1 
 |-  ( ( K e. HL /\ ( S e. A /\ ( P .\/ S ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ S .<_ ( P .\/ S ) ) -> ( S .\/ ( ( P .\/ S ) ./\ W ) ) = ( ( P .\/ S ) ./\ ( S .\/ W ) ) )
50 11 14 43 46 48 49 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( S .\/ ( ( P .\/ S ) ./\ W ) ) = ( ( P .\/ S ) ./\ ( S .\/ W ) ) )
51 simp23r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> -. S .<_ W )
52 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
53 1 2 52 4 5 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) ) -> ( S .\/ W ) = ( 1. ` K ) )
54 12 14 51 53 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( S .\/ W ) = ( 1. ` K ) )
55 54 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( P .\/ S ) ./\ ( S .\/ W ) ) = ( ( P .\/ S ) ./\ ( 1. ` K ) ) )
56 hlol 
 |-  ( K e. HL -> K e. OL )
57 11 56 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> K e. OL )
58 16 3 52 olm11 
 |-  ( ( K e. OL /\ ( P .\/ S ) e. ( Base ` K ) ) -> ( ( P .\/ S ) ./\ ( 1. ` K ) ) = ( P .\/ S ) )
59 57 43 58 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( P .\/ S ) ./\ ( 1. ` K ) ) = ( P .\/ S ) )
60 50 55 59 3eqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( P .\/ S ) = ( S .\/ ( ( P .\/ S ) ./\ W ) ) )
61 41 60 eqtr4id 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( S .\/ C ) = ( P .\/ S ) )
62 61 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( S .\/ C ) .\/ U ) = ( ( P .\/ S ) .\/ U ) )
63 16 4 atbase 
 |-  ( C e. A -> C e. ( Base ` K ) )
64 30 63 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> C e. ( Base ` K ) )
65 16 2 latj32 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ U e. ( Base ` K ) /\ C e. ( Base ` K ) ) ) -> ( ( S .\/ U ) .\/ C ) = ( ( S .\/ C ) .\/ U ) )
66 15 18 32 64 65 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( S .\/ U ) .\/ C ) = ( ( S .\/ C ) .\/ U ) )
67 2 4 hlatj32 
 |-  ( ( K e. HL /\ ( P e. A /\ S e. A /\ Q e. A ) ) -> ( ( P .\/ S ) .\/ Q ) = ( ( P .\/ Q ) .\/ S ) )
68 11 19 14 22 67 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( P .\/ S ) .\/ Q ) = ( ( P .\/ Q ) .\/ S ) )
69 16 2 latjcom 
 |-  ( ( K e. Lat /\ Q e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) ) -> ( Q .\/ ( P .\/ S ) ) = ( ( P .\/ S ) .\/ Q ) )
70 15 24 43 69 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( Q .\/ ( P .\/ S ) ) = ( ( P .\/ S ) .\/ Q ) )
71 6 oveq2i 
 |-  ( P .\/ U ) = ( P .\/ ( ( P .\/ Q ) ./\ W ) )
72 16 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
73 11 19 22 72 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
74 1 2 4 hlatlej1 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> P .<_ ( P .\/ Q ) )
75 11 19 22 74 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> P .<_ ( P .\/ Q ) )
76 16 1 2 3 4 atmod3i1 
 |-  ( ( K e. HL /\ ( P e. A /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ P .<_ ( P .\/ Q ) ) -> ( P .\/ ( ( P .\/ Q ) ./\ W ) ) = ( ( P .\/ Q ) ./\ ( P .\/ W ) ) )
77 11 19 73 46 75 76 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( P .\/ ( ( P .\/ Q ) ./\ W ) ) = ( ( P .\/ Q ) ./\ ( P .\/ W ) ) )
78 1 2 52 4 5 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ W ) = ( 1. ` K ) )
79 12 13 78 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( P .\/ W ) = ( 1. ` K ) )
80 79 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( P .\/ Q ) ./\ ( P .\/ W ) ) = ( ( P .\/ Q ) ./\ ( 1. ` K ) ) )
81 16 3 52 olm11 
 |-  ( ( K e. OL /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ ( 1. ` K ) ) = ( P .\/ Q ) )
82 57 73 81 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( P .\/ Q ) ./\ ( 1. ` K ) ) = ( P .\/ Q ) )
83 77 80 82 3eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( P .\/ ( ( P .\/ Q ) ./\ W ) ) = ( P .\/ Q ) )
84 71 83 eqtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( P .\/ U ) = ( P .\/ Q ) )
85 84 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( P .\/ U ) .\/ S ) = ( ( P .\/ Q ) .\/ S ) )
86 68 70 85 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( Q .\/ ( P .\/ S ) ) = ( ( P .\/ U ) .\/ S ) )
87 16 2 latj32 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ U e. ( Base ` K ) /\ S e. ( Base ` K ) ) ) -> ( ( P .\/ U ) .\/ S ) = ( ( P .\/ S ) .\/ U ) )
88 15 21 32 18 87 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( P .\/ U ) .\/ S ) = ( ( P .\/ S ) .\/ U ) )
89 86 88 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( Q .\/ ( P .\/ S ) ) = ( ( P .\/ S ) .\/ U ) )
90 62 66 89 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( S .\/ U ) .\/ C ) = ( Q .\/ ( P .\/ S ) ) )
91 90 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( ( S .\/ U ) .\/ C ) ./\ ( Q .\/ C ) ) = ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ C ) ) )
92 16 1 3 latmle1 
 |-  ( ( K e. Lat /\ ( P .\/ S ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ S ) ./\ W ) .<_ ( P .\/ S ) )
93 15 43 46 92 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( P .\/ S ) ./\ W ) .<_ ( P .\/ S ) )
94 8 93 eqbrtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> C .<_ ( P .\/ S ) )
95 16 1 2 latjlej2 
 |-  ( ( K e. Lat /\ ( C e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) /\ Q e. ( Base ` K ) ) ) -> ( C .<_ ( P .\/ S ) -> ( Q .\/ C ) .<_ ( Q .\/ ( P .\/ S ) ) ) )
96 15 64 43 24 95 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( C .<_ ( P .\/ S ) -> ( Q .\/ C ) .<_ ( Q .\/ ( P .\/ S ) ) ) )
97 94 96 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( Q .\/ C ) .<_ ( Q .\/ ( P .\/ S ) ) )
98 16 2 latjcl 
 |-  ( ( K e. Lat /\ Q e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) ) -> ( Q .\/ ( P .\/ S ) ) e. ( Base ` K ) )
99 15 24 43 98 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( Q .\/ ( P .\/ S ) ) e. ( Base ` K ) )
100 16 1 3 latleeqm2 
 |-  ( ( K e. Lat /\ ( Q .\/ C ) e. ( Base ` K ) /\ ( Q .\/ ( P .\/ S ) ) e. ( Base ` K ) ) -> ( ( Q .\/ C ) .<_ ( Q .\/ ( P .\/ S ) ) <-> ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ C ) ) = ( Q .\/ C ) ) )
101 15 36 99 100 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( Q .\/ C ) .<_ ( Q .\/ ( P .\/ S ) ) <-> ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ C ) ) = ( Q .\/ C ) ) )
102 97 101 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ C ) ) = ( Q .\/ C ) )
103 40 91 102 3eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( ( S .\/ U ) ./\ ( Q .\/ C ) ) .\/ C ) = ( Q .\/ C ) )
104 10 103 eqtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ ( S e. A /\ -. S .<_ W ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( F .\/ C ) = ( Q .\/ C ) )