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 |
|
dpjlid.3 |
|- ( ph -> X e. I ) |
5 |
1 2 3 4
|
dpjghm |
|- ( ph -> ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom G ) ) |
6 |
1 2
|
dprdf2 |
|- ( ph -> S : I --> ( SubGrp ` G ) ) |
7 |
6 4
|
ffvelrnd |
|- ( ph -> ( S ` X ) e. ( SubGrp ` G ) ) |
8 |
1 2 3 4
|
dpjf |
|- ( ph -> ( P ` X ) : ( G DProd S ) --> ( S ` X ) ) |
9 |
8
|
frnd |
|- ( ph -> ran ( P ` X ) C_ ( S ` X ) ) |
10 |
|
eqid |
|- ( G |`s ( S ` X ) ) = ( G |`s ( S ` X ) ) |
11 |
10
|
resghm2b |
|- ( ( ( S ` X ) e. ( SubGrp ` G ) /\ ran ( P ` X ) C_ ( S ` X ) ) -> ( ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom G ) <-> ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom ( G |`s ( S ` X ) ) ) ) ) |
12 |
7 9 11
|
syl2anc |
|- ( ph -> ( ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom G ) <-> ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom ( G |`s ( S ` X ) ) ) ) ) |
13 |
5 12
|
mpbid |
|- ( ph -> ( P ` X ) e. ( ( G |`s ( G DProd S ) ) GrpHom ( G |`s ( S ` X ) ) ) ) |