Step |
Hyp |
Ref |
Expression |
1 |
|
diaglb.g |
|- G = ( glb ` K ) |
2 |
|
diaglb.h |
|- H = ( LHyp ` K ) |
3 |
|
diaglb.i |
|- I = ( ( DIsoA ` K ) ` W ) |
4 |
|
simpl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( K e. HL /\ W e. H ) ) |
5 |
|
hlclat |
|- ( K e. HL -> K e. CLat ) |
6 |
5
|
ad2antrr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> K e. CLat ) |
7 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
8 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
9 |
7 8 2 3
|
diadm |
|- ( ( K e. HL /\ W e. H ) -> dom I = { y e. ( Base ` K ) | y ( le ` K ) W } ) |
10 |
9
|
sseq2d |
|- ( ( K e. HL /\ W e. H ) -> ( S C_ dom I <-> S C_ { y e. ( Base ` K ) | y ( le ` K ) W } ) ) |
11 |
10
|
biimpa |
|- ( ( ( K e. HL /\ W e. H ) /\ S C_ dom I ) -> S C_ { y e. ( Base ` K ) | y ( le ` K ) W } ) |
12 |
11
|
adantrr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> S C_ { y e. ( Base ` K ) | y ( le ` K ) W } ) |
13 |
|
ssrab2 |
|- { y e. ( Base ` K ) | y ( le ` K ) W } C_ ( Base ` K ) |
14 |
12 13
|
sstrdi |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> S C_ ( Base ` K ) ) |
15 |
7 1
|
clatglbcl |
|- ( ( K e. CLat /\ S C_ ( Base ` K ) ) -> ( G ` S ) e. ( Base ` K ) ) |
16 |
6 14 15
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( G ` S ) e. ( Base ` K ) ) |
17 |
|
simprr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> S =/= (/) ) |
18 |
|
n0 |
|- ( S =/= (/) <-> E. x x e. S ) |
19 |
17 18
|
sylib |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> E. x x e. S ) |
20 |
|
hllat |
|- ( K e. HL -> K e. Lat ) |
21 |
20
|
ad3antrrr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> K e. Lat ) |
22 |
16
|
adantr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( G ` S ) e. ( Base ` K ) ) |
23 |
|
ssel2 |
|- ( ( S C_ dom I /\ x e. S ) -> x e. dom I ) |
24 |
23
|
adantlr |
|- ( ( ( S C_ dom I /\ S =/= (/) ) /\ x e. S ) -> x e. dom I ) |
25 |
24
|
adantll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> x e. dom I ) |
26 |
7 8 2 3
|
diaeldm |
|- ( ( K e. HL /\ W e. H ) -> ( x e. dom I <-> ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) ) |
27 |
26
|
ad2antrr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( x e. dom I <-> ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) ) |
28 |
25 27
|
mpbid |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) |
29 |
28
|
simpld |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> x e. ( Base ` K ) ) |
30 |
7 2
|
lhpbase |
|- ( W e. H -> W e. ( Base ` K ) ) |
31 |
30
|
ad3antlr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> W e. ( Base ` K ) ) |
32 |
5
|
ad3antrrr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> K e. CLat ) |
33 |
14
|
adantr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> S C_ ( Base ` K ) ) |
34 |
|
simpr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> x e. S ) |
35 |
7 8 1
|
clatglble |
|- ( ( K e. CLat /\ S C_ ( Base ` K ) /\ x e. S ) -> ( G ` S ) ( le ` K ) x ) |
36 |
32 33 34 35
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( G ` S ) ( le ` K ) x ) |
37 |
28
|
simprd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> x ( le ` K ) W ) |
38 |
7 8 21 22 29 31 36 37
|
lattrd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( G ` S ) ( le ` K ) W ) |
39 |
19 38
|
exlimddv |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( G ` S ) ( le ` K ) W ) |
40 |
|
eqid |
|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
41 |
|
eqid |
|- ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W ) |
42 |
7 8 2 40 41 3
|
diaelval |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( G ` S ) e. ( Base ` K ) /\ ( G ` S ) ( le ` K ) W ) ) -> ( f e. ( I ` ( G ` S ) ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) ) ) ) |
43 |
4 16 39 42
|
syl12anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( f e. ( I ` ( G ` S ) ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) ) ) ) |
44 |
|
r19.28zv |
|- ( S =/= (/) -> ( A. x e. S ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ A. x e. S ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) ) |
45 |
44
|
ad2antll |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( A. x e. S ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ A. x e. S ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) ) |
46 |
|
simpll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( K e. HL /\ W e. H ) ) |
47 |
7 8 2 40 41 3
|
diaelval |
|- ( ( ( K e. HL /\ W e. H ) /\ ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) -> ( f e. ( I ` x ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) ) |
48 |
46 28 47
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( f e. ( I ` x ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) ) |
49 |
48
|
ralbidva |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( A. x e. S f e. ( I ` x ) <-> A. x e. S ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) ) |
50 |
5
|
ad3antrrr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> K e. CLat ) |
51 |
7 2 40 41
|
trlcl |
|- ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` f ) e. ( Base ` K ) ) |
52 |
51
|
adantlr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` f ) e. ( Base ` K ) ) |
53 |
14
|
adantr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> S C_ ( Base ` K ) ) |
54 |
7 8 1
|
clatleglb |
|- ( ( K e. CLat /\ ( ( ( trL ` K ) ` W ) ` f ) e. ( Base ` K ) /\ S C_ ( Base ` K ) ) -> ( ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) <-> A. x e. S ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) |
55 |
50 52 53 54
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) <-> A. x e. S ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) |
56 |
55
|
pm5.32da |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ A. x e. S ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) ) |
57 |
45 49 56
|
3bitr4rd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) ) <-> A. x e. S f e. ( I ` x ) ) ) |
58 |
|
vex |
|- f e. _V |
59 |
|
eliin |
|- ( f e. _V -> ( f e. |^|_ x e. S ( I ` x ) <-> A. x e. S f e. ( I ` x ) ) ) |
60 |
58 59
|
ax-mp |
|- ( f e. |^|_ x e. S ( I ` x ) <-> A. x e. S f e. ( I ` x ) ) |
61 |
57 60
|
bitr4di |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) ) <-> f e. |^|_ x e. S ( I ` x ) ) ) |
62 |
43 61
|
bitrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( f e. ( I ` ( G ` S ) ) <-> f e. |^|_ x e. S ( I ` x ) ) ) |
63 |
62
|
eqrdv |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) ) |