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{\uparrow }_{𝑠}A$$
	pwsco2rhm.z	$$⊢Z=S{\uparrow }_{𝑠}A$$
	pwsco2rhm.b	$$⊢B={\mathrm{Base}}_Y$$
	pwsco2rhm.a	$$⊢\phi \to A\in V$$
	pwsco2rhm.f	$$⊢\phi \to F\in \left(R\mathrm{RingHom}S\right)$$
Assertion	pwsco2rhm	$$⊢\phi \to \left(g\in B⟼F\circ g\right)\in \left(Y\mathrm{RingHom}Z\right)$$

Proof

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