Theorem pwsdiagghm

Description: Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	pwsdiagghm.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
	pwsdiagghm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	pwsdiagghm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐼 × { 𝑥 } ) )
Assertion	pwsdiagghm	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		pwsdiagghm.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2		pwsdiagghm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		pwsdiagghm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐼 × { 𝑥 } ) )
4		grpmnd	⊢ ( 𝑅 ∈ Grp → 𝑅 ∈ Mnd )
5	1 2 3	pwsdiagmhm	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 MndHom 𝑌 ) )
6	4 5	sylan	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 MndHom 𝑌 ) )
7	1	pwsgrp	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑊 ) → 𝑌 ∈ Grp )
8		ghmmhmb	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑌 ∈ Grp ) → ( 𝑅 GrpHom 𝑌 ) = ( 𝑅 MndHom 𝑌 ) )
9	7 8	syldan	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑊 ) → ( 𝑅 GrpHom 𝑌 ) = ( 𝑅 MndHom 𝑌 ) )
10	6 9	eleqtrrd	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑌 ) )