Step |
Hyp |
Ref |
Expression |
1 |
|
dihglblem.b |
|- B = ( Base ` K ) |
2 |
|
dihglblem.l |
|- .<_ = ( le ` K ) |
3 |
|
dihglblem.m |
|- ./\ = ( meet ` K ) |
4 |
|
dihglblem.g |
|- G = ( glb ` K ) |
5 |
|
dihglblem.h |
|- H = ( LHyp ` K ) |
6 |
|
dihglblem.t |
|- T = { u e. B | E. v e. S u = ( v ./\ W ) } |
7 |
|
dihglblem.i |
|- J = ( ( DIsoB ` K ) ` W ) |
8 |
|
dihglblem.ih |
|- I = ( ( DIsoH ` K ) ` W ) |
9 |
|
simp1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( K e. HL /\ W e. H ) ) |
10 |
|
simp11l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ u e. B /\ v e. S ) -> K e. HL ) |
11 |
10
|
hllatd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ u e. B /\ v e. S ) -> K e. Lat ) |
12 |
|
simp12l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ u e. B /\ v e. S ) -> S C_ B ) |
13 |
|
simp3 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ u e. B /\ v e. S ) -> v e. S ) |
14 |
12 13
|
sseldd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ u e. B /\ v e. S ) -> v e. B ) |
15 |
|
simp11r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ u e. B /\ v e. S ) -> W e. H ) |
16 |
1 5
|
lhpbase |
|- ( W e. H -> W e. B ) |
17 |
15 16
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ u e. B /\ v e. S ) -> W e. B ) |
18 |
1 2 3
|
latmle2 |
|- ( ( K e. Lat /\ v e. B /\ W e. B ) -> ( v ./\ W ) .<_ W ) |
19 |
11 14 17 18
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ u e. B /\ v e. S ) -> ( v ./\ W ) .<_ W ) |
20 |
19
|
3expia |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ u e. B ) -> ( v e. S -> ( v ./\ W ) .<_ W ) ) |
21 |
|
breq1 |
|- ( u = ( v ./\ W ) -> ( u .<_ W <-> ( v ./\ W ) .<_ W ) ) |
22 |
21
|
biimprcd |
|- ( ( v ./\ W ) .<_ W -> ( u = ( v ./\ W ) -> u .<_ W ) ) |
23 |
20 22
|
syl6 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ u e. B ) -> ( v e. S -> ( u = ( v ./\ W ) -> u .<_ W ) ) ) |
24 |
23
|
rexlimdv |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ u e. B ) -> ( E. v e. S u = ( v ./\ W ) -> u .<_ W ) ) |
25 |
24
|
ss2rabdv |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> { u e. B | E. v e. S u = ( v ./\ W ) } C_ { u e. B | u .<_ W } ) |
26 |
6 25
|
eqsstrid |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> T C_ { u e. B | u .<_ W } ) |
27 |
1 2 5 7
|
dibdmN |
|- ( ( K e. HL /\ W e. H ) -> dom J = { u e. B | u .<_ W } ) |
28 |
27
|
3ad2ant1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> dom J = { u e. B | u .<_ W } ) |
29 |
26 28
|
sseqtrrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> T C_ dom J ) |
30 |
1 2 3 4 5 6
|
dihglblem2aN |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> T =/= (/) ) |
31 |
30
|
3adant3 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> T =/= (/) ) |
32 |
4 5 7
|
dibglbN |
|- ( ( ( K e. HL /\ W e. H ) /\ ( T C_ dom J /\ T =/= (/) ) ) -> ( J ` ( G ` T ) ) = |^|_ x e. T ( J ` x ) ) |
33 |
9 29 31 32
|
syl12anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( J ` ( G ` T ) ) = |^|_ x e. T ( J ` x ) ) |
34 |
1 2 3 4 5 6
|
dihglblem2N |
|- ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) -> ( G ` S ) = ( G ` T ) ) |
35 |
34
|
3adant2r |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( G ` S ) = ( G ` T ) ) |
36 |
35
|
fveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( J ` ( G ` S ) ) = ( J ` ( G ` T ) ) ) |
37 |
|
simpl1 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ x e. T ) -> ( K e. HL /\ W e. H ) ) |
38 |
26
|
sselda |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ x e. T ) -> x e. { u e. B | u .<_ W } ) |
39 |
|
breq1 |
|- ( u = x -> ( u .<_ W <-> x .<_ W ) ) |
40 |
39
|
elrab |
|- ( x e. { u e. B | u .<_ W } <-> ( x e. B /\ x .<_ W ) ) |
41 |
38 40
|
sylib |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ x e. T ) -> ( x e. B /\ x .<_ W ) ) |
42 |
1 2 5 8 7
|
dihvalb |
|- ( ( ( K e. HL /\ W e. H ) /\ ( x e. B /\ x .<_ W ) ) -> ( I ` x ) = ( J ` x ) ) |
43 |
37 41 42
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) /\ x e. T ) -> ( I ` x ) = ( J ` x ) ) |
44 |
43
|
iineq2dv |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> |^|_ x e. T ( I ` x ) = |^|_ x e. T ( J ` x ) ) |
45 |
33 36 44
|
3eqtr4rd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> |^|_ x e. T ( I ` x ) = ( J ` ( G ` S ) ) ) |
46 |
|
simp1l |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> K e. HL ) |
47 |
|
hlclat |
|- ( K e. HL -> K e. CLat ) |
48 |
46 47
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> K e. CLat ) |
49 |
|
simp2l |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> S C_ B ) |
50 |
1 4
|
clatglbcl |
|- ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B ) |
51 |
48 49 50
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( G ` S ) e. B ) |
52 |
|
simp3 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( G ` S ) .<_ W ) |
53 |
1 2 5 8 7
|
dihvalb |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( G ` S ) e. B /\ ( G ` S ) .<_ W ) ) -> ( I ` ( G ` S ) ) = ( J ` ( G ` S ) ) ) |
54 |
9 51 52 53
|
syl12anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( I ` ( G ` S ) ) = ( J ` ( G ` S ) ) ) |
55 |
35
|
fveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( I ` ( G ` S ) ) = ( I ` ( G ` T ) ) ) |
56 |
45 54 55
|
3eqtr2rd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ ( G ` S ) .<_ W ) -> ( I ` ( G ` T ) ) = |^|_ x e. T ( I ` x ) ) |