Step |
Hyp |
Ref |
Expression |
1 |
|
dihglbc.b |
|- B = ( Base ` K ) |
2 |
|
dihglbc.g |
|- G = ( glb ` K ) |
3 |
|
dihglbc.h |
|- H = ( LHyp ` K ) |
4 |
|
dihglbc.i |
|- I = ( ( DIsoH ` K ) ` W ) |
5 |
|
dihglbc.l |
|- .<_ = ( le ` K ) |
6 |
|
dihglbcpre.j |
|- .\/ = ( join ` K ) |
7 |
|
dihglbcpre.m |
|- ./\ = ( meet ` K ) |
8 |
|
dihglbcpre.a |
|- A = ( Atoms ` K ) |
9 |
|
dihglbcpre.p |
|- P = ( ( oc ` K ) ` W ) |
10 |
|
dihglbcpre.t |
|- T = ( ( LTrn ` K ) ` W ) |
11 |
|
dihglbcpre.r |
|- R = ( ( trL ` K ) ` W ) |
12 |
|
dihglbcpre.e |
|- E = ( ( TEndo ` K ) ` W ) |
13 |
|
dihglbcpre.f |
|- F = ( iota_ g e. T ( g ` P ) = q ) |
14 |
3 4
|
dihvalrel |
|- ( ( K e. HL /\ W e. H ) -> Rel ( I ` ( G ` S ) ) ) |
15 |
14
|
3ad2ant1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> Rel ( I ` ( G ` S ) ) ) |
16 |
|
simp2r |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> S =/= (/) ) |
17 |
|
n0 |
|- ( S =/= (/) <-> E. x x e. S ) |
18 |
16 17
|
sylib |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> E. x x e. S ) |
19 |
|
simpr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ x e. S ) -> x e. S ) |
20 |
|
simpl1 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ x e. S ) -> ( K e. HL /\ W e. H ) ) |
21 |
3 4
|
dihvalrel |
|- ( ( K e. HL /\ W e. H ) -> Rel ( I ` x ) ) |
22 |
20 21
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ x e. S ) -> Rel ( I ` x ) ) |
23 |
19 22
|
jca |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ x e. S ) -> ( x e. S /\ Rel ( I ` x ) ) ) |
24 |
23
|
ex |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( x e. S -> ( x e. S /\ Rel ( I ` x ) ) ) ) |
25 |
24
|
eximdv |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( E. x x e. S -> E. x ( x e. S /\ Rel ( I ` x ) ) ) ) |
26 |
18 25
|
mpd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> E. x ( x e. S /\ Rel ( I ` x ) ) ) |
27 |
|
df-rex |
|- ( E. x e. S Rel ( I ` x ) <-> E. x ( x e. S /\ Rel ( I ` x ) ) ) |
28 |
26 27
|
sylibr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> E. x e. S Rel ( I ` x ) ) |
29 |
|
reliin |
|- ( E. x e. S Rel ( I ` x ) -> Rel |^|_ x e. S ( I ` x ) ) |
30 |
28 29
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> Rel |^|_ x e. S ( I ` x ) ) |
31 |
|
id |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) ) |
32 |
|
simp1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( K e. HL /\ W e. H ) ) |
33 |
|
simp1l |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> K e. HL ) |
34 |
|
hlclat |
|- ( K e. HL -> K e. CLat ) |
35 |
33 34
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> K e. CLat ) |
36 |
|
simp2l |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> S C_ B ) |
37 |
1 2
|
clatglbcl |
|- ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B ) |
38 |
35 36 37
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( G ` S ) e. B ) |
39 |
|
simp3 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> -. ( G ` S ) .<_ W ) |
40 |
1 5 6 7 8 3
|
lhpmcvr2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( G ` S ) e. B /\ -. ( G ` S ) .<_ W ) ) -> E. q e. A ( -. q .<_ W /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) |
41 |
32 38 39 40
|
syl12anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> E. q e. A ( -. q .<_ W /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) |
42 |
|
simpl1 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( K e. HL /\ W e. H ) ) |
43 |
38
|
adantr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( G ` S ) e. B ) |
44 |
|
simpl3 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> -. ( G ` S ) .<_ W ) |
45 |
|
simpr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) |
46 |
|
vex |
|- f e. _V |
47 |
|
vex |
|- s e. _V |
48 |
1 5 6 7 8 3 9 10 11 12 4 13 46 47
|
dihopelvalc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( G ` S ) e. B /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) ) ) ) |
49 |
42 43 44 45 48
|
syl121anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) ) ) ) |
50 |
|
simpl2r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> S =/= (/) ) |
51 |
|
r19.28zv |
|- ( S =/= (/) -> ( A. x e. S ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) <-> ( ( f e. T /\ s e. E ) /\ A. x e. S ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) ) |
52 |
50 51
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( A. x e. S ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) <-> ( ( f e. T /\ s e. E ) /\ A. x e. S ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) ) |
53 |
|
simp11 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( K e. HL /\ W e. H ) ) |
54 |
|
simp12l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> S C_ B ) |
55 |
|
simp3 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> x e. S ) |
56 |
54 55
|
sseldd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> x e. B ) |
57 |
|
simp13 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> -. ( G ` S ) .<_ W ) |
58 |
|
simp11l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> K e. HL ) |
59 |
58 34
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> K e. CLat ) |
60 |
1 5 2
|
clatglble |
|- ( ( K e. CLat /\ S C_ B /\ x e. S ) -> ( G ` S ) .<_ x ) |
61 |
59 54 55 60
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( G ` S ) .<_ x ) |
62 |
58
|
hllatd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> K e. Lat ) |
63 |
38
|
3ad2ant1 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( G ` S ) e. B ) |
64 |
|
simp11r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> W e. H ) |
65 |
1 3
|
lhpbase |
|- ( W e. H -> W e. B ) |
66 |
64 65
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> W e. B ) |
67 |
1 5
|
lattr |
|- ( ( K e. Lat /\ ( ( G ` S ) e. B /\ x e. B /\ W e. B ) ) -> ( ( ( G ` S ) .<_ x /\ x .<_ W ) -> ( G ` S ) .<_ W ) ) |
68 |
62 63 56 66 67
|
syl13anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( ( ( G ` S ) .<_ x /\ x .<_ W ) -> ( G ` S ) .<_ W ) ) |
69 |
61 68
|
mpand |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( x .<_ W -> ( G ` S ) .<_ W ) ) |
70 |
57 69
|
mtod |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> -. x .<_ W ) |
71 |
|
simp2l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( q e. A /\ -. q .<_ W ) ) |
72 |
|
simp2ll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> q e. A ) |
73 |
1 8
|
atbase |
|- ( q e. A -> q e. B ) |
74 |
72 73
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> q e. B ) |
75 |
1 7
|
latmcl |
|- ( ( K e. Lat /\ ( G ` S ) e. B /\ W e. B ) -> ( ( G ` S ) ./\ W ) e. B ) |
76 |
62 63 66 75
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( ( G ` S ) ./\ W ) e. B ) |
77 |
1 5 6
|
latlej1 |
|- ( ( K e. Lat /\ q e. B /\ ( ( G ` S ) ./\ W ) e. B ) -> q .<_ ( q .\/ ( ( G ` S ) ./\ W ) ) ) |
78 |
62 74 76 77
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> q .<_ ( q .\/ ( ( G ` S ) ./\ W ) ) ) |
79 |
|
simp2r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) |
80 |
78 79
|
breqtrd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> q .<_ ( G ` S ) ) |
81 |
1 5 62 74 63 56 80 61
|
lattrd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> q .<_ x ) |
82 |
1 5 6 7 8
|
atmod3i1 |
|- ( ( K e. HL /\ ( q e. A /\ x e. B /\ W e. B ) /\ q .<_ x ) -> ( q .\/ ( x ./\ W ) ) = ( x ./\ ( q .\/ W ) ) ) |
83 |
58 72 56 66 81 82
|
syl131anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( q .\/ ( x ./\ W ) ) = ( x ./\ ( q .\/ W ) ) ) |
84 |
|
eqid |
|- ( 1. ` K ) = ( 1. ` K ) |
85 |
5 6 84 8 3
|
lhpjat2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( q e. A /\ -. q .<_ W ) ) -> ( q .\/ W ) = ( 1. ` K ) ) |
86 |
53 71 85
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( q .\/ W ) = ( 1. ` K ) ) |
87 |
86
|
oveq2d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( x ./\ ( q .\/ W ) ) = ( x ./\ ( 1. ` K ) ) ) |
88 |
|
hlol |
|- ( K e. HL -> K e. OL ) |
89 |
58 88
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> K e. OL ) |
90 |
1 7 84
|
olm11 |
|- ( ( K e. OL /\ x e. B ) -> ( x ./\ ( 1. ` K ) ) = x ) |
91 |
89 56 90
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( x ./\ ( 1. ` K ) ) = x ) |
92 |
83 87 91
|
3eqtrd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( q .\/ ( x ./\ W ) ) = x ) |
93 |
1 5 6 7 8 3 9 10 11 12 4 13 46 47
|
dihopelvalc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( x e. B /\ -. x .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( x ./\ W ) ) = x ) ) -> ( <. f , s >. e. ( I ` x ) <-> ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) ) |
94 |
53 56 70 71 92 93
|
syl122anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( <. f , s >. e. ( I ` x ) <-> ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) ) |
95 |
94
|
3expa |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) /\ x e. S ) -> ( <. f , s >. e. ( I ` x ) <-> ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) ) |
96 |
95
|
ralbidva |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( A. x e. S <. f , s >. e. ( I ` x ) <-> A. x e. S ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) ) |
97 |
|
simp11l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> K e. HL ) |
98 |
97 34
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> K e. CLat ) |
99 |
|
simp11 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( K e. HL /\ W e. H ) ) |
100 |
|
simp3l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> f e. T ) |
101 |
|
simp3r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> s e. E ) |
102 |
5 8 3 9
|
lhpocnel2 |
|- ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) ) |
103 |
99 102
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( P e. A /\ -. P .<_ W ) ) |
104 |
|
simp2l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( q e. A /\ -. q .<_ W ) ) |
105 |
5 8 3 10 13
|
ltrniotacl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( q e. A /\ -. q .<_ W ) ) -> F e. T ) |
106 |
99 103 104 105
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> F e. T ) |
107 |
3 10 12
|
tendocl |
|- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ F e. T ) -> ( s ` F ) e. T ) |
108 |
99 101 106 107
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( s ` F ) e. T ) |
109 |
3 10
|
ltrncnv |
|- ( ( ( K e. HL /\ W e. H ) /\ ( s ` F ) e. T ) -> `' ( s ` F ) e. T ) |
110 |
99 108 109
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> `' ( s ` F ) e. T ) |
111 |
3 10
|
ltrnco |
|- ( ( ( K e. HL /\ W e. H ) /\ f e. T /\ `' ( s ` F ) e. T ) -> ( f o. `' ( s ` F ) ) e. T ) |
112 |
99 100 110 111
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( f o. `' ( s ` F ) ) e. T ) |
113 |
1 3 10 11
|
trlcl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( f o. `' ( s ` F ) ) e. T ) -> ( R ` ( f o. `' ( s ` F ) ) ) e. B ) |
114 |
99 112 113
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( R ` ( f o. `' ( s ` F ) ) ) e. B ) |
115 |
|
simp12l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> S C_ B ) |
116 |
1 5 2
|
clatleglb |
|- ( ( K e. CLat /\ ( R ` ( f o. `' ( s ` F ) ) ) e. B /\ S C_ B ) -> ( ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) <-> A. x e. S ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) |
117 |
98 114 115 116
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) <-> A. x e. S ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) |
118 |
117
|
3expa |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) /\ ( f e. T /\ s e. E ) ) -> ( ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) <-> A. x e. S ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) |
119 |
118
|
pm5.32da |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) ) <-> ( ( f e. T /\ s e. E ) /\ A. x e. S ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) ) |
120 |
52 96 119
|
3bitr4rd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) ) <-> A. x e. S <. f , s >. e. ( I ` x ) ) ) |
121 |
|
opex |
|- <. f , s >. e. _V |
122 |
|
eliin |
|- ( <. f , s >. e. _V -> ( <. f , s >. e. |^|_ x e. S ( I ` x ) <-> A. x e. S <. f , s >. e. ( I ` x ) ) ) |
123 |
121 122
|
ax-mp |
|- ( <. f , s >. e. |^|_ x e. S ( I ` x ) <-> A. x e. S <. f , s >. e. ( I ` x ) ) |
124 |
120 123
|
bitr4di |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) ) |
125 |
49 124
|
bitrd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) ) |
126 |
125
|
exp44 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( q e. A -> ( -. q .<_ W -> ( ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) ) ) ) ) |
127 |
126
|
imp4a |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( q e. A -> ( ( -. q .<_ W /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) ) ) ) |
128 |
127
|
rexlimdv |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( E. q e. A ( -. q .<_ W /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) ) ) |
129 |
41 128
|
mpd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) ) |
130 |
129
|
eqrelrdv2 |
|- ( ( ( Rel ( I ` ( G ` S ) ) /\ Rel |^|_ x e. S ( I ` x ) ) /\ ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) ) |
131 |
15 30 31 130
|
syl21anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) ) |