Step |
Hyp |
Ref |
Expression |
1 |
|
dochval.b |
|- B = ( Base ` K ) |
2 |
|
dochval.g |
|- G = ( glb ` K ) |
3 |
|
dochval.o |
|- ._|_ = ( oc ` K ) |
4 |
|
dochval.h |
|- H = ( LHyp ` K ) |
5 |
|
elex |
|- ( K e. V -> K e. _V ) |
6 |
|
fveq2 |
|- ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) ) |
7 |
6 4
|
eqtr4di |
|- ( k = K -> ( LHyp ` k ) = H ) |
8 |
|
fveq2 |
|- ( k = K -> ( DVecH ` k ) = ( DVecH ` K ) ) |
9 |
8
|
fveq1d |
|- ( k = K -> ( ( DVecH ` k ) ` w ) = ( ( DVecH ` K ) ` w ) ) |
10 |
9
|
fveq2d |
|- ( k = K -> ( Base ` ( ( DVecH ` k ) ` w ) ) = ( Base ` ( ( DVecH ` K ) ` w ) ) ) |
11 |
10
|
pweqd |
|- ( k = K -> ~P ( Base ` ( ( DVecH ` k ) ` w ) ) = ~P ( Base ` ( ( DVecH ` K ) ` w ) ) ) |
12 |
|
fveq2 |
|- ( k = K -> ( DIsoH ` k ) = ( DIsoH ` K ) ) |
13 |
12
|
fveq1d |
|- ( k = K -> ( ( DIsoH ` k ) ` w ) = ( ( DIsoH ` K ) ` w ) ) |
14 |
|
fveq2 |
|- ( k = K -> ( oc ` k ) = ( oc ` K ) ) |
15 |
14 3
|
eqtr4di |
|- ( k = K -> ( oc ` k ) = ._|_ ) |
16 |
|
fveq2 |
|- ( k = K -> ( glb ` k ) = ( glb ` K ) ) |
17 |
16 2
|
eqtr4di |
|- ( k = K -> ( glb ` k ) = G ) |
18 |
|
fveq2 |
|- ( k = K -> ( Base ` k ) = ( Base ` K ) ) |
19 |
18 1
|
eqtr4di |
|- ( k = K -> ( Base ` k ) = B ) |
20 |
13
|
fveq1d |
|- ( k = K -> ( ( ( DIsoH ` k ) ` w ) ` y ) = ( ( ( DIsoH ` K ) ` w ) ` y ) ) |
21 |
20
|
sseq2d |
|- ( k = K -> ( x C_ ( ( ( DIsoH ` k ) ` w ) ` y ) <-> x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) ) ) |
22 |
19 21
|
rabeqbidv |
|- ( k = K -> { y e. ( Base ` k ) | x C_ ( ( ( DIsoH ` k ) ` w ) ` y ) } = { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) |
23 |
17 22
|
fveq12d |
|- ( k = K -> ( ( glb ` k ) ` { y e. ( Base ` k ) | x C_ ( ( ( DIsoH ` k ) ` w ) ` y ) } ) = ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) |
24 |
15 23
|
fveq12d |
|- ( k = K -> ( ( oc ` k ) ` ( ( glb ` k ) ` { y e. ( Base ` k ) | x C_ ( ( ( DIsoH ` k ) ` w ) ` y ) } ) ) = ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) |
25 |
13 24
|
fveq12d |
|- ( k = K -> ( ( ( DIsoH ` k ) ` w ) ` ( ( oc ` k ) ` ( ( glb ` k ) ` { y e. ( Base ` k ) | x C_ ( ( ( DIsoH ` k ) ` w ) ` y ) } ) ) ) = ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) |
26 |
11 25
|
mpteq12dv |
|- ( k = K -> ( x e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( ( ( DIsoH ` k ) ` w ) ` ( ( oc ` k ) ` ( ( glb ` k ) ` { y e. ( Base ` k ) | x C_ ( ( ( DIsoH ` k ) ` w ) ` y ) } ) ) ) ) = ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) ) |
27 |
7 26
|
mpteq12dv |
|- ( k = K -> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( ( ( DIsoH ` k ) ` w ) ` ( ( oc ` k ) ` ( ( glb ` k ) ` { y e. ( Base ` k ) | x C_ ( ( ( DIsoH ` k ) ` w ) ` y ) } ) ) ) ) ) = ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) ) ) |
28 |
|
df-doch |
|- ocH = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( ( ( DIsoH ` k ) ` w ) ` ( ( oc ` k ) ` ( ( glb ` k ) ` { y e. ( Base ` k ) | x C_ ( ( ( DIsoH ` k ) ` w ) ` y ) } ) ) ) ) ) ) |
29 |
27 28 4
|
mptfvmpt |
|- ( K e. _V -> ( ocH ` K ) = ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) ) ) |
30 |
5 29
|
syl |
|- ( K e. V -> ( ocH ` K ) = ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) ) ) |