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 eqtrid ( ( 𝑅 ∈ 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 𝑅 ) )