Step |
Hyp |
Ref |
Expression |
1 |
|
dprdval.0 |
|- .0. = ( 0g ` G ) |
2 |
|
dprdval.w |
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. } |
3 |
|
elfvdm |
|- ( A e. ( DProd ` <. G , S >. ) -> <. G , S >. e. dom DProd ) |
4 |
|
df-ov |
|- ( G DProd S ) = ( DProd ` <. G , S >. ) |
5 |
3 4
|
eleq2s |
|- ( A e. ( G DProd S ) -> <. G , S >. e. dom DProd ) |
6 |
|
df-br |
|- ( G dom DProd S <-> <. G , S >. e. dom DProd ) |
7 |
5 6
|
sylibr |
|- ( A e. ( G DProd S ) -> G dom DProd S ) |
8 |
7
|
pm4.71ri |
|- ( A e. ( G DProd S ) <-> ( G dom DProd S /\ A e. ( G DProd S ) ) ) |
9 |
1 2
|
dprdval |
|- ( ( G dom DProd S /\ dom S = I ) -> ( G DProd S ) = ran ( f e. W |-> ( G gsum f ) ) ) |
10 |
9
|
eleq2d |
|- ( ( G dom DProd S /\ dom S = I ) -> ( A e. ( G DProd S ) <-> A e. ran ( f e. W |-> ( G gsum f ) ) ) ) |
11 |
|
eqid |
|- ( f e. W |-> ( G gsum f ) ) = ( f e. W |-> ( G gsum f ) ) |
12 |
|
ovex |
|- ( G gsum f ) e. _V |
13 |
11 12
|
elrnmpti |
|- ( A e. ran ( f e. W |-> ( G gsum f ) ) <-> E. f e. W A = ( G gsum f ) ) |
14 |
10 13
|
bitrdi |
|- ( ( G dom DProd S /\ dom S = I ) -> ( A e. ( G DProd S ) <-> E. f e. W A = ( G gsum f ) ) ) |
15 |
14
|
ancoms |
|- ( ( dom S = I /\ G dom DProd S ) -> ( A e. ( G DProd S ) <-> E. f e. W A = ( G gsum f ) ) ) |
16 |
15
|
pm5.32da |
|- ( dom S = I -> ( ( G dom DProd S /\ A e. ( G DProd S ) ) <-> ( G dom DProd S /\ E. f e. W A = ( G gsum f ) ) ) ) |
17 |
8 16
|
syl5bb |
|- ( dom S = I -> ( A e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. W A = ( G gsum f ) ) ) ) |