Metamath Proof Explorer

Theorem cdlemm10N

Description: The image of the map G is the entire one-dimensional subspace ( IV ) . Remark after Lemma M of Crawley p. 121 line 23. (Contributed by NM, 24-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemm10.l 
|- .<_ = ( le ` K )
cdlemm10.j 
|- .\/ = ( join ` K )
cdlemm10.a 
|- A = ( Atoms ` K )
cdlemm10.h 
|- H = ( LHyp ` K )
cdlemm10.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemm10.r 
|- R = ( ( trL ` K ) ` W )
cdlemm10.i 
|- I = ( ( DIsoA ` K ) ` W )
cdlemm10.c 
|- C = { r e. A | ( r .<_ ( P .\/ V ) /\ -. r .<_ W ) }
cdlemm10.f 
|- F = ( iota_ f e. T ( f ` P ) = s )
cdlemm10.g 
|- G = ( q e. C |-> ( iota_ f e. T ( f ` P ) = q ) )
Assertion cdlemm10N 
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ran G = ( I ` V ) )

Proof

Step Hyp Ref Expression
1 cdlemm10.l 
 |-  .<_ = ( le ` K )
2 cdlemm10.j 
 |-  .\/ = ( join ` K )
3 cdlemm10.a 
 |-  A = ( Atoms ` K )
4 cdlemm10.h 
 |-  H = ( LHyp ` K )
5 cdlemm10.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 cdlemm10.r 
 |-  R = ( ( trL ` K ) ` W )
7 cdlemm10.i 
 |-  I = ( ( DIsoA ` K ) ` W )
8 cdlemm10.c 
 |-  C = { r e. A | ( r .<_ ( P .\/ V ) /\ -. r .<_ W ) }
9 cdlemm10.f 
 |-  F = ( iota_ f e. T ( f ` P ) = s )
10 cdlemm10.g 
 |-  G = ( q e. C |-> ( iota_ f e. T ( f ` P ) = q ) )
11 riotaex 
 |-  ( iota_ f e. T ( f ` P ) = q ) e. _V
12 11 10 fnmpti 
 |-  G Fn C
13 fvelrnb 
 |-  ( G Fn C -> ( g e. ran G <-> E. s e. C ( G ` s ) = g ) )
14 12 13 ax-mp 
 |-  ( g e. ran G <-> E. s e. C ( G ` s ) = g )
15 eqeq2 
 |-  ( q = s -> ( ( f ` P ) = q <-> ( f ` P ) = s ) )
16 15 riotabidv 
 |-  ( q = s -> ( iota_ f e. T ( f ` P ) = q ) = ( iota_ f e. T ( f ` P ) = s ) )
17 riotaex 
 |-  ( iota_ f e. T ( f ` P ) = s ) e. _V
18 16 10 17 fvmpt 
 |-  ( s e. C -> ( G ` s ) = ( iota_ f e. T ( f ` P ) = s ) )
19 18 9 eqtr4di 
 |-  ( s e. C -> ( G ` s ) = F )
20 19 adantl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ s e. C ) -> ( G ` s ) = F )
21 20 eqeq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ s e. C ) -> ( ( G ` s ) = g <-> F = g ) )
22 21 rexbidva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( E. s e. C ( G ` s ) = g <-> E. s e. C F = g ) )
23 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( K e. HL /\ W e. H ) )
24 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> g e. T )
25 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> P e. A )
26 1 3 4 5 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ g e. T /\ P e. A ) -> ( g ` P ) e. A )
27 23 24 25 26 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( g ` P ) e. A )
28 eqid 
 |-  ( Base ` K ) = ( Base ` K )
29 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> K e. HL )
30 29 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> K e. Lat )
31 28 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
32 25 31 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> P e. ( Base ` K ) )
33 28 4 5 ltrncl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ g e. T /\ P e. ( Base ` K ) ) -> ( g ` P ) e. ( Base ` K ) )
34 23 24 32 33 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( g ` P ) e. ( Base ` K ) )
35 28 2 latjcl 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ ( g ` P ) e. ( Base ` K ) ) -> ( P .\/ ( g ` P ) ) e. ( Base ` K ) )
36 30 32 34 35 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( P .\/ ( g ` P ) ) e. ( Base ` K ) )
37 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> V e. A )
38 28 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ V e. A ) -> ( P .\/ V ) e. ( Base ` K ) )
39 29 25 37 38 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( P .\/ V ) e. ( Base ` K ) )
40 28 1 2 latlej2 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ ( g ` P ) e. ( Base ` K ) ) -> ( g ` P ) .<_ ( P .\/ ( g ` P ) ) )
41 30 32 34 40 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( g ` P ) .<_ ( P .\/ ( g ` P ) ) )
42 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( P e. A /\ -. P .<_ W ) )
43 1 2 3 4 5 6 trljat1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ g e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( R ` g ) ) = ( P .\/ ( g ` P ) ) )
44 23 24 42 43 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( P .\/ ( R ` g ) ) = ( P .\/ ( g ` P ) ) )
45 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( R ` g ) .<_ V )
46 28 4 5 6 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ g e. T ) -> ( R ` g ) e. ( Base ` K ) )
47 23 24 46 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( R ` g ) e. ( Base ` K ) )
48 28 3 atbase 
 |-  ( V e. A -> V e. ( Base ` K ) )
49 37 48 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> V e. ( Base ` K ) )
50 28 1 2 latjlej2 
 |-  ( ( K e. Lat /\ ( ( R ` g ) e. ( Base ` K ) /\ V e. ( Base ` K ) /\ P e. ( Base ` K ) ) ) -> ( ( R ` g ) .<_ V -> ( P .\/ ( R ` g ) ) .<_ ( P .\/ V ) ) )
51 30 47 49 32 50 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( ( R ` g ) .<_ V -> ( P .\/ ( R ` g ) ) .<_ ( P .\/ V ) ) )
52 45 51 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( P .\/ ( R ` g ) ) .<_ ( P .\/ V ) )
53 44 52 eqbrtrrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( P .\/ ( g ` P ) ) .<_ ( P .\/ V ) )
54 28 1 30 34 36 39 41 53 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( g ` P ) .<_ ( P .\/ V ) )
55 1 3 4 5 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ g e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( g ` P ) e. A /\ -. ( g ` P ) .<_ W ) )
56 55 simprd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ g e. T /\ ( P e. A /\ -. P .<_ W ) ) -> -. ( g ` P ) .<_ W )
57 23 24 42 56 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> -. ( g ` P ) .<_ W )
58 54 57 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( ( g ` P ) .<_ ( P .\/ V ) /\ -. ( g ` P ) .<_ W ) )
59 breq1 
 |-  ( r = ( g ` P ) -> ( r .<_ ( P .\/ V ) <-> ( g ` P ) .<_ ( P .\/ V ) ) )
60 breq1 
 |-  ( r = ( g ` P ) -> ( r .<_ W <-> ( g ` P ) .<_ W ) )
61 60 notbid 
 |-  ( r = ( g ` P ) -> ( -. r .<_ W <-> -. ( g ` P ) .<_ W ) )
62 59 61 anbi12d 
 |-  ( r = ( g ` P ) -> ( ( r .<_ ( P .\/ V ) /\ -. r .<_ W ) <-> ( ( g ` P ) .<_ ( P .\/ V ) /\ -. ( g ` P ) .<_ W ) ) )
63 62 8 elrab2 
 |-  ( ( g ` P ) e. C <-> ( ( g ` P ) e. A /\ ( ( g ` P ) .<_ ( P .\/ V ) /\ -. ( g ` P ) .<_ W ) ) )
64 27 58 63 sylanbrc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( g ` P ) e. C )
65 1 3 4 5 cdlemeiota 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ g e. T ) -> g = ( iota_ f e. T ( f ` P ) = ( g ` P ) ) )
66 23 42 24 65 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> g = ( iota_ f e. T ( f ` P ) = ( g ` P ) ) )
67 66 eqcomd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> ( iota_ f e. T ( f ` P ) = ( g ` P ) ) = g )
68 eqeq2 
 |-  ( s = ( g ` P ) -> ( ( f ` P ) = s <-> ( f ` P ) = ( g ` P ) ) )
69 68 riotabidv 
 |-  ( s = ( g ` P ) -> ( iota_ f e. T ( f ` P ) = s ) = ( iota_ f e. T ( f ` P ) = ( g ` P ) ) )
70 9 69 syl5eq 
 |-  ( s = ( g ` P ) -> F = ( iota_ f e. T ( f ` P ) = ( g ` P ) ) )
71 70 eqeq1d 
 |-  ( s = ( g ` P ) -> ( F = g <-> ( iota_ f e. T ( f ` P ) = ( g ` P ) ) = g ) )
72 71 rspcev 
 |-  ( ( ( g ` P ) e. C /\ ( iota_ f e. T ( f ` P ) = ( g ` P ) ) = g ) -> E. s e. C F = g )
73 64 67 72 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( g e. T /\ ( R ` g ) .<_ V ) ) -> E. s e. C F = g )
74 73 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( ( g e. T /\ ( R ` g ) .<_ V ) -> E. s e. C F = g ) )
75 breq1 
 |-  ( r = s -> ( r .<_ ( P .\/ V ) <-> s .<_ ( P .\/ V ) ) )
76 breq1 
 |-  ( r = s -> ( r .<_ W <-> s .<_ W ) )
77 76 notbid 
 |-  ( r = s -> ( -. r .<_ W <-> -. s .<_ W ) )
78 75 77 anbi12d 
 |-  ( r = s -> ( ( r .<_ ( P .\/ V ) /\ -. r .<_ W ) <-> ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) )
79 78 8 elrab2 
 |-  ( s e. C <-> ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) )
80 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> ( K e. HL /\ W e. H ) )
81 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> P e. A )
82 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> -. P .<_ W )
83 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> s e. A )
84 simprrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> -. s .<_ W )
85 1 3 4 5 9 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( s e. A /\ -. s .<_ W ) ) -> F e. T )
86 1 3 4 5 9 ltrniotaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( F ` P ) = s )
87 85 86 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( s e. A /\ -. s .<_ W ) ) -> ( F e. T /\ ( F ` P ) = s ) )
88 80 81 82 83 84 87 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> ( F e. T /\ ( F ` P ) = s ) )
89 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) /\ ( F e. T /\ ( F ` P ) = s ) ) -> F e. T )
90 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) /\ ( F e. T /\ ( F ` P ) = s ) ) -> ( K e. HL /\ W e. H ) )
91 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) /\ ( F e. T /\ ( F ` P ) = s ) ) -> ( P e. A /\ -. P .<_ W ) )
92 eqid 
 |-  ( meet ` K ) = ( meet ` K )
93 1 2 92 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 ) )
94 90 89 91 93 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) /\ ( F e. T /\ ( F ` P ) = s ) ) -> ( R ` F ) = ( ( P .\/ ( F ` P ) ) ( meet ` K ) W ) )
95 simp3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) /\ ( F e. T /\ ( F ` P ) = s ) ) -> ( F ` P ) = s )
96 95 oveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) /\ ( F e. T /\ ( F ` P ) = s ) ) -> ( P .\/ ( F ` P ) ) = ( P .\/ s ) )
97 96 oveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) /\ ( F e. T /\ ( F ` P ) = s ) ) -> ( ( P .\/ ( F ` P ) ) ( meet ` K ) W ) = ( ( P .\/ s ) ( meet ` K ) W ) )
98 94 97 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) /\ ( F e. T /\ ( F ` P ) = s ) ) -> ( R ` F ) = ( ( P .\/ s ) ( meet ` K ) W ) )
99 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> K e. HL )
100 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> V e. A )
101 1 2 3 hlatlej1 
 |-  ( ( K e. HL /\ P e. A /\ V e. A ) -> P .<_ ( P .\/ V ) )
102 99 81 100 101 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> P .<_ ( P .\/ V ) )
103 simprrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> s .<_ ( P .\/ V ) )
104 99 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> K e. Lat )
105 81 31 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> P e. ( Base ` K ) )
106 28 3 atbase 
 |-  ( s e. A -> s e. ( Base ` K ) )
107 106 ad2antrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> s e. ( Base ` K ) )
108 99 81 100 38 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> ( P .\/ V ) e. ( Base ` K ) )
109 28 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ s e. ( Base ` K ) /\ ( P .\/ V ) e. ( Base ` K ) ) ) -> ( ( P .<_ ( P .\/ V ) /\ s .<_ ( P .\/ V ) ) <-> ( P .\/ s ) .<_ ( P .\/ V ) ) )
110 104 105 107 108 109 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> ( ( P .<_ ( P .\/ V ) /\ s .<_ ( P .\/ V ) ) <-> ( P .\/ s ) .<_ ( P .\/ V ) ) )
111 102 103 110 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> ( P .\/ s ) .<_ ( P .\/ V ) )
112 28 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ s e. A ) -> ( P .\/ s ) e. ( Base ` K ) )
113 99 81 83 112 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> ( P .\/ s ) e. ( Base ` K ) )
114 simpl1r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> W e. H )
115 28 4 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
116 114 115 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> W e. ( Base ` K ) )
117 28 1 92 latmlem1 
 |-  ( ( K e. Lat /\ ( ( P .\/ s ) e. ( Base ` K ) /\ ( P .\/ V ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( P .\/ s ) .<_ ( P .\/ V ) -> ( ( P .\/ s ) ( meet ` K ) W ) .<_ ( ( P .\/ V ) ( meet ` K ) W ) ) )
118 104 113 108 116 117 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> ( ( P .\/ s ) .<_ ( P .\/ V ) -> ( ( P .\/ s ) ( meet ` K ) W ) .<_ ( ( P .\/ V ) ( meet ` K ) W ) ) )
119 111 118 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> ( ( P .\/ s ) ( meet ` K ) W ) .<_ ( ( P .\/ V ) ( meet ` K ) W ) )
120 1 2 92 3 4 lhpat4N 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( ( P .\/ V ) ( meet ` K ) W ) = V )
121 120 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> ( ( P .\/ V ) ( meet ` K ) W ) = V )
122 119 121 breqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> ( ( P .\/ s ) ( meet ` K ) W ) .<_ V )
123 122 3adant3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) /\ ( F e. T /\ ( F ` P ) = s ) ) -> ( ( P .\/ s ) ( meet ` K ) W ) .<_ V )
124 98 123 eqbrtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) /\ ( F e. T /\ ( F ` P ) = s ) ) -> ( R ` F ) .<_ V )
125 89 124 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) /\ ( F e. T /\ ( F ` P ) = s ) ) -> ( F e. T /\ ( R ` F ) .<_ V ) )
126 88 125 mpd3an3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( s e. A /\ ( s .<_ ( P .\/ V ) /\ -. s .<_ W ) ) ) -> ( F e. T /\ ( R ` F ) .<_ V ) )
127 79 126 sylan2b 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ s e. C ) -> ( F e. T /\ ( R ` F ) .<_ V ) )
128 127 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( s e. C -> ( F e. T /\ ( R ` F ) .<_ V ) ) )
129 eleq1 
 |-  ( F = g -> ( F e. T <-> g e. T ) )
130 fveq2 
 |-  ( F = g -> ( R ` F ) = ( R ` g ) )
131 130 breq1d 
 |-  ( F = g -> ( ( R ` F ) .<_ V <-> ( R ` g ) .<_ V ) )
132 129 131 anbi12d 
 |-  ( F = g -> ( ( F e. T /\ ( R ` F ) .<_ V ) <-> ( g e. T /\ ( R ` g ) .<_ V ) ) )
133 132 biimpcd 
 |-  ( ( F e. T /\ ( R ` F ) .<_ V ) -> ( F = g -> ( g e. T /\ ( R ` g ) .<_ V ) ) )
134 128 133 syl6 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( s e. C -> ( F = g -> ( g e. T /\ ( R ` g ) .<_ V ) ) ) )
135 134 rexlimdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( E. s e. C F = g -> ( g e. T /\ ( R ` g ) .<_ V ) ) )
136 74 135 impbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( ( g e. T /\ ( R ` g ) .<_ V ) <-> E. s e. C F = g ) )
137 22 136 bitr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( E. s e. C ( G ` s ) = g <-> ( g e. T /\ ( R ` g ) .<_ V ) ) )
138 fveq2 
 |-  ( f = g -> ( R ` f ) = ( R ` g ) )
139 138 breq1d 
 |-  ( f = g -> ( ( R ` f ) .<_ V <-> ( R ` g ) .<_ V ) )
140 139 elrab 
 |-  ( g e. { f e. T | ( R ` f ) .<_ V } <-> ( g e. T /\ ( R ` g ) .<_ V ) )
141 137 140 bitr4di 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( E. s e. C ( G ` s ) = g <-> g e. { f e. T | ( R ` f ) .<_ V } ) )
142 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> K e. HL )
143 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> W e. H )
144 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> V e. A )
145 144 48 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> V e. ( Base ` K ) )
146 simp3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> V .<_ W )
147 28 1 4 5 6 7 diaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( V e. ( Base ` K ) /\ V .<_ W ) ) -> ( I ` V ) = { f e. T | ( R ` f ) .<_ V } )
148 142 143 145 146 147 syl22anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( I ` V ) = { f e. T | ( R ` f ) .<_ V } )
149 148 eleq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( g e. ( I ` V ) <-> g e. { f e. T | ( R ` f ) .<_ V } ) )
150 141 149 bitr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( E. s e. C ( G ` s ) = g <-> g e. ( I ` V ) ) )
151 14 150 syl5bb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( g e. ran G <-> g e. ( I ` V ) ) )
152 151 eqrdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ran G = ( I ` V ) )