Theorem pwsco1rhm

Description: Right composition with a function on the index sets yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	pwsco1rhm.y	$$⊢Y=R{\uparrow }_{𝑠}A$$
	pwsco1rhm.z	$$⊢Z=R{\uparrow }_{𝑠}B$$
	pwsco1rhm.c	$$⊢C={\mathrm{Base}}_Z$$
	pwsco1rhm.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	pwsco1rhm.a	$$⊢\phi \to A\in V$$
	pwsco1rhm.b	$$⊢\phi \to B\in W$$
	pwsco1rhm.f	$$⊢\phi \to F:A⟶B$$
Assertion	pwsco1rhm	$$⊢\phi \to \left(g\in C⟼g\circ F\right)\in \left(Z\mathrm{RingHom}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		pwsco1rhm.y	$$⊢Y=R{\uparrow }_{𝑠}A$$
2		pwsco1rhm.z	$$⊢Z=R{\uparrow }_{𝑠}B$$
3		pwsco1rhm.c	$$⊢C={\mathrm{Base}}_Z$$
4		pwsco1rhm.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		pwsco1rhm.a	$$⊢\phi \to A\in V$$
6		pwsco1rhm.b	$$⊢\phi \to B\in W$$
7		pwsco1rhm.f	$$⊢\phi \to F:A⟶B$$
8	2	pwsring	$$⊢\left(R\in \mathrm{Ring}\wedge B\in W\right)\to Z\in \mathrm{Ring}$$
9	4 6 8	syl2anc	$$⊢\phi \to Z\in \mathrm{Ring}$$
10	1	pwsring	$$⊢\left(R\in \mathrm{Ring}\wedge A\in V\right)\to Y\in \mathrm{Ring}$$
11	4 5 10	syl2anc	$$⊢\phi \to Y\in \mathrm{Ring}$$
12		ringmnd	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Mnd}$$
13	4 12	syl	$$⊢\phi \to R\in \mathrm{Mnd}$$
14	1 2 3 13 5 6 7	pwsco1mhm	$$⊢\phi \to \left(g\in C⟼g\circ F\right)\in \left(Z\mathrm{MndHom}Y\right)$$
15		ringgrp	$$⊢Z\in \mathrm{Ring}\to Z\in \mathrm{Grp}$$
16	9 15	syl	$$⊢\phi \to Z\in \mathrm{Grp}$$
17		ringgrp	$$⊢Y\in \mathrm{Ring}\to Y\in \mathrm{Grp}$$
18	11 17	syl	$$⊢\phi \to Y\in \mathrm{Grp}$$
19		ghmmhmb	$$⊢\left(Z\in \mathrm{Grp}\wedge Y\in \mathrm{Grp}\right)\to Z\mathrm{GrpHom}Y=Z\mathrm{MndHom}Y$$
20	16 18 19	syl2anc	$$⊢\phi \to Z\mathrm{GrpHom}Y=Z\mathrm{MndHom}Y$$
21	14 20	eleqtrrd	$$⊢\phi \to \left(g\in C⟼g\circ F\right)\in \left(Z\mathrm{GrpHom}Y\right)$$
22		eqid	$$⊢{\mathrm{mulGrp}}_R{\uparrow }_{𝑠}A={\mathrm{mulGrp}}_R{\uparrow }_{𝑠}A$$
23		eqid	$$⊢{\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B={\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B$$
24		eqid	$$⊢{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}$$
25		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
26	25	ringmgp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
27	4 26	syl	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
28	22 23 24 27 5 6 7	pwsco1mhm	$$⊢\phi \to \left(g\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}⟼g\circ F\right)\in \left(\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)\mathrm{MndHom}\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}A\right)\right)$$
29		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
30	2 29	pwsbas	$$⊢\left(R\in \mathrm{Mnd}\wedge B\in W\right)\to {{\mathrm{Base}}_R}^B={\mathrm{Base}}_Z$$
31	13 6 30	syl2anc	$$⊢\phi \to {{\mathrm{Base}}_R}^B={\mathrm{Base}}_Z$$
32	31 3	syl6eqr	$$⊢\phi \to {{\mathrm{Base}}_R}^B=C$$
33	25 29	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
34	23 33	pwsbas	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge B\in W\right)\to {{\mathrm{Base}}_R}^B={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}$$
35	27 6 34	syl2anc	$$⊢\phi \to {{\mathrm{Base}}_R}^B={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}$$
36	32 35	eqtr3d	$$⊢\phi \to C={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}$$
37	36	mpteq1d	$$⊢\phi \to \left(g\in C⟼g\circ F\right)=\left(g\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}⟼g\circ F\right)$$
38		eqidd	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{mulGrp}}_Z}={\mathrm{Base}}_{{\mathrm{mulGrp}}_Z}$$
39		eqidd	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{mulGrp}}_Y}={\mathrm{Base}}_{{\mathrm{mulGrp}}_Y}$$
40		eqid	$$⊢{\mathrm{mulGrp}}_Z={\mathrm{mulGrp}}_Z$$
41		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_Z}={\mathrm{Base}}_{{\mathrm{mulGrp}}_Z}$$
42		eqid	$$⊢{+}_{{\mathrm{mulGrp}}_Z}={+}_{{\mathrm{mulGrp}}_Z}$$
43		eqid	$$⊢{+}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}={+}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}$$
44	2 25 23 40 41 24 42 43	pwsmgp	$$⊢\left(R\in \mathrm{Ring}\wedge B\in W\right)\to \left({\mathrm{Base}}_{{\mathrm{mulGrp}}_Z}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}\wedge {+}_{{\mathrm{mulGrp}}_Z}={+}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}\right)$$
45	4 6 44	syl2anc	$$⊢\phi \to \left({\mathrm{Base}}_{{\mathrm{mulGrp}}_Z}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}\wedge {+}_{{\mathrm{mulGrp}}_Z}={+}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}\right)$$
46	45	simpld	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{mulGrp}}_Z}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}$$
47		eqid	$$⊢{\mathrm{mulGrp}}_Y={\mathrm{mulGrp}}_Y$$
48		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_Y}={\mathrm{Base}}_{{\mathrm{mulGrp}}_Y}$$
49		eqid	$$⊢{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}A\right)}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}A\right)}$$
50		eqid	$$⊢{+}_{{\mathrm{mulGrp}}_Y}={+}_{{\mathrm{mulGrp}}_Y}$$
51		eqid	$$⊢{+}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}A\right)}={+}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}A\right)}$$
52	1 25 22 47 48 49 50 51	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)$$
53	4 5 52	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)$$
54	53	simpld	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{mulGrp}}_Y}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}A\right)}$$
55	45	simprd	$$⊢\phi \to {+}_{{\mathrm{mulGrp}}_Z}={+}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)}$$
56	55	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}}_R{\uparrow }_{𝑠}B\right)}y$$
57	53	simprd	$$⊢\phi \to {+}_{{\mathrm{mulGrp}}_Y}={+}_{\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}A\right)}$$
58	57	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$$
59	38 39 46 54 56 58	mhmpropd	$$⊢\phi \to {\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_Y=\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}B\right)\mathrm{MndHom}\left({\mathrm{mulGrp}}_R{\uparrow }_{𝑠}A\right)$$
60	28 37 59	3eltr4d	$$⊢\phi \to \left(g\in C⟼g\circ F\right)\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_Y\right)$$
61	21 60	jca	$$⊢\phi \to \left(\left(g\in C⟼g\circ F\right)\in \left(Z\mathrm{GrpHom}Y\right)\wedge \left(g\in C⟼g\circ F\right)\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_Y\right)\right)$$
62	40 47	isrhm	$$⊢\left(g\in C⟼g\circ F\right)\in \left(Z\mathrm{RingHom}Y\right)\leftrightarrow \left(\left(Z\in \mathrm{Ring}\wedge Y\in \mathrm{Ring}\right)\wedge \left(\left(g\in C⟼g\circ F\right)\in \left(Z\mathrm{GrpHom}Y\right)\wedge \left(g\in C⟼g\circ F\right)\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_Y\right)\right)\right)$$
63	9 11 61 62	syl21anbrc	$$⊢\phi \to \left(g\in C⟼g\circ F\right)\in \left(Z\mathrm{RingHom}Y\right)$$