Step |
Hyp |
Ref |
Expression |
1 |
|
dpjfval.1 |
⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 ) |
2 |
|
dpjfval.2 |
⊢ ( 𝜑 → dom 𝑆 = 𝐼 ) |
3 |
|
dpjfval.p |
⊢ 𝑃 = ( 𝐺 dProj 𝑆 ) |
4 |
|
dpjlid.3 |
⊢ ( 𝜑 → 𝑋 ∈ 𝐼 ) |
5 |
1 2 3 4
|
dpjghm |
⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom 𝐺 ) ) |
6 |
1 2
|
dprdf2 |
⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ) |
7 |
6 4
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐺 ) ) |
8 |
1 2 3 4
|
dpjf |
⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) : ( 𝐺 DProd 𝑆 ) ⟶ ( 𝑆 ‘ 𝑋 ) ) |
9 |
8
|
frnd |
⊢ ( 𝜑 → ran ( 𝑃 ‘ 𝑋 ) ⊆ ( 𝑆 ‘ 𝑋 ) ) |
10 |
|
eqid |
⊢ ( 𝐺 ↾s ( 𝑆 ‘ 𝑋 ) ) = ( 𝐺 ↾s ( 𝑆 ‘ 𝑋 ) ) |
11 |
10
|
resghm2b |
⊢ ( ( ( 𝑆 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ran ( 𝑃 ‘ 𝑋 ) ⊆ ( 𝑆 ‘ 𝑋 ) ) → ( ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom 𝐺 ) ↔ ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom ( 𝐺 ↾s ( 𝑆 ‘ 𝑋 ) ) ) ) ) |
12 |
7 9 11
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom 𝐺 ) ↔ ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom ( 𝐺 ↾s ( 𝑆 ‘ 𝑋 ) ) ) ) ) |
13 |
5 12
|
mpbid |
⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) ∈ ( ( 𝐺 ↾s ( 𝐺 DProd 𝑆 ) ) GrpHom ( 𝐺 ↾s ( 𝑆 ‘ 𝑋 ) ) ) ) |