Metamath Proof Explorer

Theorem cdlemd2

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 29-May-2012)

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

Proof

Step Hyp Ref Expression
1 cdlemd2.l 
 |-  .<_ = ( le ` K )
2 cdlemd2.j 
 |-  .\/ = ( join ` K )
3 cdlemd2.a 
 |-  A = ( Atoms ` K )
4 cdlemd2.h 
 |-  H = ( LHyp ` K )
5 cdlemd2.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` P ) = ( G ` P ) )
7 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( K e. HL /\ W e. H ) )
8 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> F e. T )
9 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> K e. HL )
10 9 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> K e. Lat )
11 simp21l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> P e. A )
12 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> R e. A )
13 eqid 
 |-  ( Base ` K ) = ( Base ` K )
14 13 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ R e. A ) -> ( P .\/ R ) e. ( Base ` K ) )
15 9 11 12 14 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( P .\/ R ) e. ( Base ` K ) )
16 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> W e. H )
17 13 4 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
18 16 17 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> W e. ( Base ` K ) )
19 eqid 
 |-  ( meet ` K ) = ( meet ` K )
20 13 19 latmcl 
 |-  ( ( K e. Lat /\ ( P .\/ R ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) )
21 10 15 18 20 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( ( P .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) )
22 13 1 19 latmle2 
 |-  ( ( K e. Lat /\ ( P .\/ R ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ R ) ( meet ` K ) W ) .<_ W )
23 10 15 18 22 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( ( P .\/ R ) ( meet ` K ) W ) .<_ W )
24 13 1 4 5 ltrnval1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( ( ( P .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( P .\/ R ) ( meet ` K ) W ) .<_ W ) ) -> ( F ` ( ( P .\/ R ) ( meet ` K ) W ) ) = ( ( P .\/ R ) ( meet ` K ) W ) )
25 7 8 21 23 24 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` ( ( P .\/ R ) ( meet ` K ) W ) ) = ( ( P .\/ R ) ( meet ` K ) W ) )
26 simp12r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> G e. T )
27 13 1 4 5 ltrnval1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( ( ( P .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( P .\/ R ) ( meet ` K ) W ) .<_ W ) ) -> ( G ` ( ( P .\/ R ) ( meet ` K ) W ) ) = ( ( P .\/ R ) ( meet ` K ) W ) )
28 7 26 21 23 27 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( G ` ( ( P .\/ R ) ( meet ` K ) W ) ) = ( ( P .\/ R ) ( meet ` K ) W ) )
29 25 28 eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` ( ( P .\/ R ) ( meet ` K ) W ) ) = ( G ` ( ( P .\/ R ) ( meet ` K ) W ) ) )
30 6 29 oveq12d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( ( F ` P ) .\/ ( F ` ( ( P .\/ R ) ( meet ` K ) W ) ) ) = ( ( G ` P ) .\/ ( G ` ( ( P .\/ R ) ( meet ` K ) W ) ) ) )
31 13 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
32 11 31 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> P e. ( Base ` K ) )
33 13 2 4 5 ltrnj 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. ( Base ` K ) /\ ( ( P .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) ) ) -> ( F ` ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ) = ( ( F ` P ) .\/ ( F ` ( ( P .\/ R ) ( meet ` K ) W ) ) ) )
34 7 8 32 21 33 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ) = ( ( F ` P ) .\/ ( F ` ( ( P .\/ R ) ( meet ` K ) W ) ) ) )
35 13 2 4 5 ltrnj 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. ( Base ` K ) /\ ( ( P .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) ) ) -> ( G ` ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ) = ( ( G ` P ) .\/ ( G ` ( ( P .\/ R ) ( meet ` K ) W ) ) ) )
36 7 26 32 21 35 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( G ` ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ) = ( ( G ` P ) .\/ ( G ` ( ( P .\/ R ) ( meet ` K ) W ) ) ) )
37 30 34 36 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ) = ( G ` ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ) )
38 simp3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` Q ) = ( G ` Q ) )
39 simp22l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> Q e. A )
40 13 2 3 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )
41 9 39 12 40 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( Q .\/ R ) e. ( Base ` K ) )
42 13 19 latmcl 
 |-  ( ( K e. Lat /\ ( Q .\/ R ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( Q .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) )
43 10 41 18 42 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( ( Q .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) )
44 13 1 19 latmle2 
 |-  ( ( K e. Lat /\ ( Q .\/ R ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( Q .\/ R ) ( meet ` K ) W ) .<_ W )
45 10 41 18 44 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( ( Q .\/ R ) ( meet ` K ) W ) .<_ W )
46 13 1 4 5 ltrnval1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( ( ( Q .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( Q .\/ R ) ( meet ` K ) W ) .<_ W ) ) -> ( F ` ( ( Q .\/ R ) ( meet ` K ) W ) ) = ( ( Q .\/ R ) ( meet ` K ) W ) )
47 7 8 43 45 46 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` ( ( Q .\/ R ) ( meet ` K ) W ) ) = ( ( Q .\/ R ) ( meet ` K ) W ) )
48 13 1 4 5 ltrnval1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( ( ( Q .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( Q .\/ R ) ( meet ` K ) W ) .<_ W ) ) -> ( G ` ( ( Q .\/ R ) ( meet ` K ) W ) ) = ( ( Q .\/ R ) ( meet ` K ) W ) )
49 7 26 43 45 48 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( G ` ( ( Q .\/ R ) ( meet ` K ) W ) ) = ( ( Q .\/ R ) ( meet ` K ) W ) )
50 47 49 eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` ( ( Q .\/ R ) ( meet ` K ) W ) ) = ( G ` ( ( Q .\/ R ) ( meet ` K ) W ) ) )
51 38 50 oveq12d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( ( F ` Q ) .\/ ( F ` ( ( Q .\/ R ) ( meet ` K ) W ) ) ) = ( ( G ` Q ) .\/ ( G ` ( ( Q .\/ R ) ( meet ` K ) W ) ) ) )
52 13 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
53 39 52 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> Q e. ( Base ` K ) )
54 13 2 4 5 ltrnj 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( Q e. ( Base ` K ) /\ ( ( Q .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) ) ) -> ( F ` ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) = ( ( F ` Q ) .\/ ( F ` ( ( Q .\/ R ) ( meet ` K ) W ) ) ) )
55 7 8 53 43 54 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) = ( ( F ` Q ) .\/ ( F ` ( ( Q .\/ R ) ( meet ` K ) W ) ) ) )
56 13 2 4 5 ltrnj 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( Q e. ( Base ` K ) /\ ( ( Q .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) ) ) -> ( G ` ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) = ( ( G ` Q ) .\/ ( G ` ( ( Q .\/ R ) ( meet ` K ) W ) ) ) )
57 7 26 53 43 56 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( G ` ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) = ( ( G ` Q ) .\/ ( G ` ( ( Q .\/ R ) ( meet ` K ) W ) ) ) )
58 51 55 57 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) = ( G ` ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) )
59 37 58 oveq12d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( ( F ` ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ) ( meet ` K ) ( F ` ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) = ( ( G ` ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ) ( meet ` K ) ( G ` ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) )
60 13 2 latjcl 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ ( ( P .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) ) -> ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) e. ( Base ` K ) )
61 10 32 21 60 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) e. ( Base ` K ) )
62 13 2 latjcl 
 |-  ( ( K e. Lat /\ Q e. ( Base ` K ) /\ ( ( Q .\/ R ) ( meet ` K ) W ) e. ( Base ` K ) ) -> ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) e. ( Base ` K ) )
63 10 53 43 62 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) e. ( Base ` K ) )
64 13 19 4 5 ltrnm 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) e. ( Base ` K ) /\ ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) e. ( Base ` K ) ) ) -> ( F ` ( ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ( meet ` K ) ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) = ( ( F ` ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ) ( meet ` K ) ( F ` ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) )
65 7 8 61 63 64 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` ( ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ( meet ` K ) ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) = ( ( F ` ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ) ( meet ` K ) ( F ` ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) )
66 13 19 4 5 ltrnm 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) e. ( Base ` K ) /\ ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) e. ( Base ` K ) ) ) -> ( G ` ( ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ( meet ` K ) ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) = ( ( G ` ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ) ( meet ` K ) ( G ` ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) )
67 7 26 61 63 66 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( G ` ( ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ( meet ` K ) ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) = ( ( G ` ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ) ( meet ` K ) ( G ` ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) )
68 59 65 67 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` ( ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ( meet ` K ) ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) = ( G ` ( ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ( meet ` K ) ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) )
69 simp21 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( P e. A /\ -. P .<_ W ) )
70 simp22 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
71 simp23l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> P =/= Q )
72 simp23r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> -. R .<_ ( P .\/ Q ) )
73 12 71 72 3jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( R e. A /\ P =/= Q /\ -. R .<_ ( P .\/ Q ) ) )
74 1 2 19 3 4 cdlemd1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) ) -> R = ( ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ( meet ` K ) ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) )
75 7 69 70 73 74 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> R = ( ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ( meet ` K ) ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) )
76 75 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` R ) = ( F ` ( ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ( meet ` K ) ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) )
77 75 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( G ` R ) = ( G ` ( ( P .\/ ( ( P .\/ R ) ( meet ` K ) W ) ) ( meet ` K ) ( Q .\/ ( ( Q .\/ R ) ( meet ` K ) W ) ) ) ) )
78 68 76 77 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` R ) = ( G ` R ) )