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