Step |
Hyp |
Ref |
Expression |
1 |
|
dprdff.w |
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. } |
2 |
|
dprdff.1 |
|- ( ph -> G dom DProd S ) |
3 |
|
dprdff.2 |
|- ( ph -> dom S = I ) |
4 |
|
dprdff.3 |
|- ( ph -> F e. W ) |
5 |
|
dprdff.b |
|- B = ( Base ` G ) |
6 |
1 2 3
|
dprdw |
|- ( ph -> ( F e. W <-> ( F Fn I /\ A. x e. I ( F ` x ) e. ( S ` x ) /\ F finSupp .0. ) ) ) |
7 |
4 6
|
mpbid |
|- ( ph -> ( F Fn I /\ A. x e. I ( F ` x ) e. ( S ` x ) /\ F finSupp .0. ) ) |
8 |
7
|
simp1d |
|- ( ph -> F Fn I ) |
9 |
7
|
simp2d |
|- ( ph -> A. x e. I ( F ` x ) e. ( S ` x ) ) |
10 |
2 3
|
dprdf2 |
|- ( ph -> S : I --> ( SubGrp ` G ) ) |
11 |
10
|
ffvelrnda |
|- ( ( ph /\ x e. I ) -> ( S ` x ) e. ( SubGrp ` G ) ) |
12 |
5
|
subgss |
|- ( ( S ` x ) e. ( SubGrp ` G ) -> ( S ` x ) C_ B ) |
13 |
11 12
|
syl |
|- ( ( ph /\ x e. I ) -> ( S ` x ) C_ B ) |
14 |
13
|
sseld |
|- ( ( ph /\ x e. I ) -> ( ( F ` x ) e. ( S ` x ) -> ( F ` x ) e. B ) ) |
15 |
14
|
ralimdva |
|- ( ph -> ( A. x e. I ( F ` x ) e. ( S ` x ) -> A. x e. I ( F ` x ) e. B ) ) |
16 |
9 15
|
mpd |
|- ( ph -> A. x e. I ( F ` x ) e. B ) |
17 |
|
ffnfv |
|- ( F : I --> B <-> ( F Fn I /\ A. x e. I ( F ` x ) e. B ) ) |
18 |
8 16 17
|
sylanbrc |
|- ( ph -> F : I --> B ) |