Theorem pwsco2rhm

Description: Left composition with a ring homomorphism yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	pwsco2rhm.y	|- Y = ( R ^s A )
	pwsco2rhm.z	|- Z = ( S ^s A )
	pwsco2rhm.b	|- B = ( Base ` Y )
	pwsco2rhm.a	|- ( ph -> A e. V )
	pwsco2rhm.f	|- ( ph -> F e. ( R RingHom S ) )
Assertion	pwsco2rhm	|- ( ph -> ( g e. B |-> ( F o. g ) ) e. ( Y RingHom Z ) )

Proof

Step	Hyp	Ref	Expression
1		pwsco2rhm.y	|- Y = ( R ^s A )
2		pwsco2rhm.z	|- Z = ( S ^s A )
3		pwsco2rhm.b	|- B = ( Base ` Y )
4		pwsco2rhm.a	|- ( ph -> A e. V )
5		pwsco2rhm.f	|- ( ph -> F e. ( R RingHom S ) )
6		rhmrcl1	|- ( F e. ( R RingHom S ) -> R e. Ring )
7	5 6	syl	|- ( ph -> R e. Ring )
8	1	pwsring	|- ( ( R e. Ring /\ A e. V ) -> Y e. Ring )
9	7 4 8	syl2anc	|- ( ph -> Y e. Ring )
10		rhmrcl2	|- ( F e. ( R RingHom S ) -> S e. Ring )
11	5 10	syl	|- ( ph -> S e. Ring )
12	2	pwsring	|- ( ( S e. Ring /\ A e. V ) -> Z e. Ring )
13	11 4 12	syl2anc	|- ( ph -> Z e. Ring )
14		rhmghm	|- ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
15	5 14	syl	|- ( ph -> F e. ( R GrpHom S ) )
16		ghmmhm	|- ( F e. ( R GrpHom S ) -> F e. ( R MndHom S ) )
17	15 16	syl	|- ( ph -> F e. ( R MndHom S ) )
18	1 2 3 4 17	pwsco2mhm	|- ( ph -> ( g e. B |-> ( F o. g ) ) e. ( Y MndHom Z ) )
19		ringgrp	|- ( Y e. Ring -> Y e. Grp )
20	9 19	syl	|- ( ph -> Y e. Grp )
21		ringgrp	|- ( Z e. Ring -> Z e. Grp )
22	13 21	syl	|- ( ph -> Z e. Grp )
23		ghmmhmb	|- ( ( Y e. Grp /\ Z e. Grp ) -> ( Y GrpHom Z ) = ( Y MndHom Z ) )
24	20 22 23	syl2anc	|- ( ph -> ( Y GrpHom Z ) = ( Y MndHom Z ) )
25	18 24	eleqtrrd	|- ( ph -> ( g e. B |-> ( F o. g ) ) e. ( Y GrpHom Z ) )
26		eqid	|- ( ( mulGrp ` R ) ^s A ) = ( ( mulGrp ` R ) ^s A )
27		eqid	|- ( ( mulGrp ` S ) ^s A ) = ( ( mulGrp ` S ) ^s A )
28		eqid	|- ( Base ` ( ( mulGrp ` R ) ^s A ) ) = ( Base ` ( ( mulGrp ` R ) ^s A ) )
29		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
30		eqid	|- ( mulGrp ` S ) = ( mulGrp ` S )
31	29 30	rhmmhm	|- ( F e. ( R RingHom S ) -> F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) )
32	5 31	syl	|- ( ph -> F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) )
33	26 27 28 4 32	pwsco2mhm	|- ( ph -> ( g e. ( Base ` ( ( mulGrp ` R ) ^s A ) ) |-> ( F o. g ) ) e. ( ( ( mulGrp ` R ) ^s A ) MndHom ( ( mulGrp ` S ) ^s A ) ) )
34		eqid	|- ( Base ` R ) = ( Base ` R )
35	1 34	pwsbas	|- ( ( R e. Ring /\ A e. V ) -> ( ( Base ` R ) ^m A ) = ( Base ` Y ) )
36	7 4 35	syl2anc	|- ( ph -> ( ( Base ` R ) ^m A ) = ( Base ` Y ) )
37	36 3	eqtr4di	|- ( ph -> ( ( Base ` R ) ^m A ) = B )
38	29	ringmgp	|- ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
39	7 38	syl	|- ( ph -> ( mulGrp ` R ) e. Mnd )
40	29 34	mgpbas	|- ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
41	26 40	pwsbas	|- ( ( ( mulGrp ` R ) e. Mnd /\ A e. V ) -> ( ( Base ` R ) ^m A ) = ( Base ` ( ( mulGrp ` R ) ^s A ) ) )
42	39 4 41	syl2anc	|- ( ph -> ( ( Base ` R ) ^m A ) = ( Base ` ( ( mulGrp ` R ) ^s A ) ) )
43	37 42	eqtr3d	|- ( ph -> B = ( Base ` ( ( mulGrp ` R ) ^s A ) ) )
44	43	mpteq1d	|- ( ph -> ( g e. B |-> ( F o. g ) ) = ( g e. ( Base ` ( ( mulGrp ` R ) ^s A ) ) |-> ( F o. g ) ) )
45		eqidd	|- ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( mulGrp ` Y ) ) )
46		eqidd	|- ( ph -> ( Base ` ( mulGrp ` Z ) ) = ( Base ` ( mulGrp ` Z ) ) )
47		eqid	|- ( mulGrp ` Y ) = ( mulGrp ` Y )
48		eqid	|- ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( mulGrp ` Y ) )
49		eqid	|- ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( mulGrp ` Y ) )
50		eqid	|- ( +g ` ( ( mulGrp ` R ) ^s A ) ) = ( +g ` ( ( mulGrp ` R ) ^s A ) )
51	1 29 26 47 48 28 49 50	pwsmgp	|- ( ( R e. Ring /\ A e. V ) -> ( ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( ( mulGrp ` R ) ^s A ) ) /\ ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( ( mulGrp ` R ) ^s A ) ) ) )
52	7 4 51	syl2anc	|- ( ph -> ( ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( ( mulGrp ` R ) ^s A ) ) /\ ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( ( mulGrp ` R ) ^s A ) ) ) )
53	52	simpld	|- ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( ( mulGrp ` R ) ^s A ) ) )
54		eqid	|- ( mulGrp ` Z ) = ( mulGrp ` Z )
55		eqid	|- ( Base ` ( mulGrp ` Z ) ) = ( Base ` ( mulGrp ` Z ) )
56		eqid	|- ( Base ` ( ( mulGrp ` S ) ^s A ) ) = ( Base ` ( ( mulGrp ` S ) ^s A ) )
57		eqid	|- ( +g ` ( mulGrp ` Z ) ) = ( +g ` ( mulGrp ` Z ) )
58		eqid	|- ( +g ` ( ( mulGrp ` S ) ^s A ) ) = ( +g ` ( ( mulGrp ` S ) ^s A ) )
59	2 30 27 54 55 56 57 58	pwsmgp	|- ( ( S e. Ring /\ A e. V ) -> ( ( Base ` ( mulGrp ` Z ) ) = ( Base ` ( ( mulGrp ` S ) ^s A ) ) /\ ( +g ` ( mulGrp ` Z ) ) = ( +g ` ( ( mulGrp ` S ) ^s A ) ) ) )
60	11 4 59	syl2anc	|- ( ph -> ( ( Base ` ( mulGrp ` Z ) ) = ( Base ` ( ( mulGrp ` S ) ^s A ) ) /\ ( +g ` ( mulGrp ` Z ) ) = ( +g ` ( ( mulGrp ` S ) ^s A ) ) ) )
61	60	simpld	|- ( ph -> ( Base ` ( mulGrp ` Z ) ) = ( Base ` ( ( mulGrp ` S ) ^s A ) ) )
62	52	simprd	|- ( ph -> ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( ( mulGrp ` R ) ^s A ) ) )
63	62	oveqdr	|- ( ( ph /\ ( x e. ( Base ` ( mulGrp ` Y ) ) /\ y e. ( Base ` ( mulGrp ` Y ) ) ) ) -> ( x ( +g ` ( mulGrp ` Y ) ) y ) = ( x ( +g ` ( ( mulGrp ` R ) ^s A ) ) y ) )
64	60	simprd	|- ( ph -> ( +g ` ( mulGrp ` Z ) ) = ( +g ` ( ( mulGrp ` S ) ^s A ) ) )
65	64	oveqdr	|- ( ( ph /\ ( x e. ( Base ` ( mulGrp ` Z ) ) /\ y e. ( Base ` ( mulGrp ` Z ) ) ) ) -> ( x ( +g ` ( mulGrp ` Z ) ) y ) = ( x ( +g ` ( ( mulGrp ` S ) ^s A ) ) y ) )
66	45 46 53 61 63 65	mhmpropd	|- ( ph -> ( ( mulGrp ` Y ) MndHom ( mulGrp ` Z ) ) = ( ( ( mulGrp ` R ) ^s A ) MndHom ( ( mulGrp ` S ) ^s A ) ) )
67	33 44 66	3eltr4d	|- ( ph -> ( g e. B |-> ( F o. g ) ) e. ( ( mulGrp ` Y ) MndHom ( mulGrp ` Z ) ) )
68	25 67	jca	|- ( ph -> ( ( g e. B |-> ( F o. g ) ) e. ( Y GrpHom Z ) /\ ( g e. B |-> ( F o. g ) ) e. ( ( mulGrp ` Y ) MndHom ( mulGrp ` Z ) ) ) )
69	47 54	isrhm	|- ( ( g e. B |-> ( F o. g ) ) e. ( Y RingHom Z ) <-> ( ( Y e. Ring /\ Z e. Ring ) /\ ( ( g e. B |-> ( F o. g ) ) e. ( Y GrpHom Z ) /\ ( g e. B |-> ( F o. g ) ) e. ( ( mulGrp ` Y ) MndHom ( mulGrp ` Z ) ) ) ) )
70	9 13 68 69	syl21anbrc	|- ( ph -> ( g e. B |-> ( F o. g ) ) e. ( Y RingHom Z ) )