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
|- Y = ( R ^s I )
pwspjmhm.b
|- B = ( Base ` Y )
Assertion pwspjmhm
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( x e. B |-> ( x ` A ) ) e. ( Y MndHom R ) )

Proof

Step Hyp Ref Expression
1 pwspjmhm.y
 |-  Y = ( R ^s I )
2 pwspjmhm.b
 |-  B = ( Base ` Y )
3 eqid
 |-  ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) )
4 eqid
 |-  ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
5 simp2
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> I e. V )
6 fvexd
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( Scalar ` R ) e. _V )
7 fconst6g
 |-  ( R e. Mnd -> ( I X. { R } ) : I --> Mnd )
8 7 3ad2ant1
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( I X. { R } ) : I --> Mnd )
9 simp3
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> A e. I )
10 3 4 5 6 8 9 prdspjmhm
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( x e. ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) |-> ( x ` A ) ) e. ( ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) MndHom ( ( I X. { R } ) ` A ) ) )
11 eqid
 |-  ( Scalar ` R ) = ( Scalar ` R )
12 1 11 pwsval
 |-  ( ( R e. Mnd /\ I e. V ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
13 12 3adant3
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
14 13 fveq2d
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( Base ` Y ) = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
15 2 14 syl5eq
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> B = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
16 15 mpteq1d
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( x e. B |-> ( x ` A ) ) = ( x e. ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) |-> ( x ` A ) ) )
17 fvconst2g
 |-  ( ( R e. Mnd /\ A e. I ) -> ( ( I X. { R } ) ` A ) = R )
18 17 3adant2
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( ( I X. { R } ) ` A ) = R )
19 18 eqcomd
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> R = ( ( I X. { R } ) ` A ) )
20 13 19 oveq12d
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( Y MndHom R ) = ( ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) MndHom ( ( I X. { R } ) ` A ) ) )
21 10 16 20 3eltr4d
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( x e. B |-> ( x ` A ) ) e. ( Y MndHom R ) )