Metamath Proof Explorer

Theorem pwspjmhm

Description: A projection from a structure power of a monoid to the monoid itself is a monoid homomorphism. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses pwspjmhm.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwspjmhm.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
Assertion pwspjmhm ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ∈ ( 𝑌 MndHom 𝑅 ) )

Proof

Step Hyp Ref Expression
1 pwspjmhm.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwspjmhm.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
4 eqid ⊢ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
5 simp2 ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → 𝐼 ∈ 𝑉 )
6 fvexd ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( Scalar ‘ 𝑅 ) ∈ V )
7 fconst6g ⊢ ( 𝑅 ∈ Mnd → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ Mnd )
8 7 3ad2ant1 ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ Mnd )
9 simp3 ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → 𝐴 ∈ 𝐼 )
10 3 4 5 6 8 9 prdspjmhm ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑥 ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ↦ ( 𝑥 ‘ 𝐴 ) ) ∈ ( ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) MndHom ( ( 𝐼 × { 𝑅 } ) ‘ 𝐴 ) ) )
11 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
12 1 11 pwsval ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
13 12 3adant3 ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
14 13 fveq2d ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
15 2 14 syl5eq ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → 𝐵 = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
16 15 mpteq1d ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) = ( 𝑥 ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ↦ ( 𝑥 ‘ 𝐴 ) ) )
17 fvconst2g ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝐴 ) = 𝑅 )
18 17 3adant2 ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝐴 ) = 𝑅 )
19 18 eqcomd ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → 𝑅 = ( ( 𝐼 × { 𝑅 } ) ‘ 𝐴 ) )
20 13 19 oveq12d ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑌 MndHom 𝑅 ) = ( ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) MndHom ( ( 𝐼 × { 𝑅 } ) ‘ 𝐴 ) ) )
21 10 16 20 3eltr4d ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ∈ ( 𝑌 MndHom 𝑅 ) )