Step |
Hyp |
Ref |
Expression |
1 |
|
dpjfval.1 |
|- ( ph -> G dom DProd S ) |
2 |
|
dpjfval.2 |
|- ( ph -> dom S = I ) |
3 |
|
dpjfval.p |
|- P = ( G dProj S ) |
4 |
|
dpjidcl.3 |
|- ( ph -> A e. ( G DProd S ) ) |
5 |
|
dpjidcl.0 |
|- .0. = ( 0g ` G ) |
6 |
|
dpjidcl.w |
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. } |
7 |
|
dpjeq.c |
|- ( ph -> ( x e. I |-> C ) e. W ) |
8 |
1 2 3 4 5 6
|
dpjidcl |
|- ( ph -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) e. W /\ A = ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) ) ) |
9 |
8
|
simprd |
|- ( ph -> A = ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) ) |
10 |
9
|
eqeq1d |
|- ( ph -> ( A = ( G gsum ( x e. I |-> C ) ) <-> ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) = ( G gsum ( x e. I |-> C ) ) ) ) |
11 |
8
|
simpld |
|- ( ph -> ( x e. I |-> ( ( P ` x ) ` A ) ) e. W ) |
12 |
5 6 1 2 11 7
|
dprdf11 |
|- ( ph -> ( ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) = ( G gsum ( x e. I |-> C ) ) <-> ( x e. I |-> ( ( P ` x ) ` A ) ) = ( x e. I |-> C ) ) ) |
13 |
|
fvex |
|- ( ( P ` x ) ` A ) e. _V |
14 |
13
|
rgenw |
|- A. x e. I ( ( P ` x ) ` A ) e. _V |
15 |
|
mpteqb |
|- ( A. x e. I ( ( P ` x ) ` A ) e. _V -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) = ( x e. I |-> C ) <-> A. x e. I ( ( P ` x ) ` A ) = C ) ) |
16 |
14 15
|
mp1i |
|- ( ph -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) = ( x e. I |-> C ) <-> A. x e. I ( ( P ` x ) ` A ) = C ) ) |
17 |
10 12 16
|
3bitrd |
|- ( ph -> ( A = ( G gsum ( x e. I |-> C ) ) <-> A. x e. I ( ( P ` x ) ` A ) = C ) ) |