Step |
Hyp |
Ref |
Expression |
1 |
|
mapdh.q |
|- Q = ( 0g ` C ) |
2 |
|
mapdh.i |
|- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) |
3 |
|
mapdh0.o |
|- .0. = ( 0g ` U ) |
4 |
|
mapdh0.x |
|- ( ph -> X e. A ) |
5 |
|
mapdh0.f |
|- ( ph -> F e. B ) |
6 |
3
|
fvexi |
|- .0. e. _V |
7 |
6
|
a1i |
|- ( ph -> .0. e. _V ) |
8 |
1 2 4 5 7
|
mapdhval |
|- ( ph -> ( I ` <. X , F , .0. >. ) = if ( .0. = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { .0. } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- .0. ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) ) |
9 |
|
eqid |
|- .0. = .0. |
10 |
9
|
iftruei |
|- if ( .0. = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { .0. } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- .0. ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) = Q |
11 |
8 10
|
eqtrdi |
|- ( ph -> ( I ` <. X , F , .0. >. ) = Q ) |