| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dprd2d.1 |
|- ( ph -> Rel A ) |
| 2 |
|
dprd2d.2 |
|- ( ph -> S : A --> ( SubGrp ` G ) ) |
| 3 |
|
dprd2d.3 |
|- ( ph -> dom A C_ I ) |
| 4 |
|
dprd2d.4 |
|- ( ( ph /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) |
| 5 |
|
dprd2d.5 |
|- ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) |
| 6 |
|
dprd2d.k |
|- K = ( mrCls ` ( SubGrp ` G ) ) |
| 7 |
1 2 3 4 5 6
|
dprd2da |
|- ( ph -> G dom DProd S ) |
| 8 |
6
|
dprdspan |
|- ( G dom DProd S -> ( G DProd S ) = ( K ` U. ran S ) ) |
| 9 |
7 8
|
syl |
|- ( ph -> ( G DProd S ) = ( K ` U. ran S ) ) |
| 10 |
|
relssres |
|- ( ( Rel A /\ dom A C_ I ) -> ( A |` I ) = A ) |
| 11 |
1 3 10
|
syl2anc |
|- ( ph -> ( A |` I ) = A ) |
| 12 |
11
|
imaeq2d |
|- ( ph -> ( S " ( A |` I ) ) = ( S " A ) ) |
| 13 |
|
ffn |
|- ( S : A --> ( SubGrp ` G ) -> S Fn A ) |
| 14 |
|
fnima |
|- ( S Fn A -> ( S " A ) = ran S ) |
| 15 |
2 13 14
|
3syl |
|- ( ph -> ( S " A ) = ran S ) |
| 16 |
12 15
|
eqtr2d |
|- ( ph -> ran S = ( S " ( A |` I ) ) ) |
| 17 |
16
|
unieqd |
|- ( ph -> U. ran S = U. ( S " ( A |` I ) ) ) |
| 18 |
17
|
fveq2d |
|- ( ph -> ( K ` U. ran S ) = ( K ` U. ( S " ( A |` I ) ) ) ) |
| 19 |
|
ssidd |
|- ( ph -> I C_ I ) |
| 20 |
1 2 3 4 5 6 19
|
dprd2dlem1 |
|- ( ph -> ( K ` U. ( S " ( A |` I ) ) ) = ( G DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) ) |
| 21 |
9 18 20
|
3eqtrd |
|- ( ph -> ( G DProd S ) = ( G DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) ) |