This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑌 ) )