Theorem prdsmgp

Description: The multiplicative monoid of a product is the product of the multiplicative monoids of the factors. (Contributed by Mario Carneiro, 11-Mar-2015)

	Ref	Expression
Hypotheses	prdsmgp.y	$$⊢Y=S{⨉}_{𝑠}R$$
	prdsmgp.m	$$⊢M={\mathrm{mulGrp}}_Y$$
	prdsmgp.z	$$⊢Z=S{⨉}_{𝑠}\left(\mathrm{mulGrp}\circ R\right)$$
	prdsmgp.i	$$⊢\phi \to I\in V$$
	prdsmgp.s	$$⊢\phi \to S\in W$$
	prdsmgp.r	$$⊢\phi \to RFnI$$
Assertion	prdsmgp	$$⊢\phi \to \left({\mathrm{Base}}_M={\mathrm{Base}}_Z\wedge {+}_M={+}_Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		prdsmgp.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsmgp.m	$$⊢M={\mathrm{mulGrp}}_Y$$
3		prdsmgp.z	$$⊢Z=S{⨉}_{𝑠}\left(\mathrm{mulGrp}\circ R\right)$$
4		prdsmgp.i	$$⊢\phi \to I\in V$$
5		prdsmgp.s	$$⊢\phi \to S\in W$$
6		prdsmgp.r	$$⊢\phi \to RFnI$$
7		eqid	$$⊢{\mathrm{mulGrp}}_{R\left(x\right)}={\mathrm{mulGrp}}_{R\left(x\right)}$$
8		eqid	$$⊢{\mathrm{Base}}_{R\left(x\right)}={\mathrm{Base}}_{R\left(x\right)}$$
9	7 8	mgpbas	$$⊢{\mathrm{Base}}_{R\left(x\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{R\left(x\right)}}$$
10		fvco2	$$⊢\left(RFnI\wedge x\in I\right)\to \left(\mathrm{mulGrp}\circ R\right)\left(x\right)={\mathrm{mulGrp}}_{R\left(x\right)}$$
11	6 10	sylan	$$⊢\left(\phi \wedge x\in I\right)\to \left(\mathrm{mulGrp}\circ R\right)\left(x\right)={\mathrm{mulGrp}}_{R\left(x\right)}$$
12	11	eqcomd	$$⊢\left(\phi \wedge x\in I\right)\to {\mathrm{mulGrp}}_{R\left(x\right)}=\left(\mathrm{mulGrp}\circ R\right)\left(x\right)$$
13	12	fveq2d	$$⊢\left(\phi \wedge x\in I\right)\to {\mathrm{Base}}_{{\mathrm{mulGrp}}_{R\left(x\right)}}={\mathrm{Base}}_{\left(\mathrm{mulGrp}\circ R\right)\left(x\right)}$$
14	9 13	syl5eq	$$⊢\left(\phi \wedge x\in I\right)\to {\mathrm{Base}}_{R\left(x\right)}={\mathrm{Base}}_{\left(\mathrm{mulGrp}\circ R\right)\left(x\right)}$$
15	14	ixpeq2dva	$$⊢\phi \to \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}=\underset{x\in I}{⨉}{\mathrm{Base}}_{\left(\mathrm{mulGrp}\circ R\right)\left(x\right)}$$
16		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
17	2 16	mgpbas	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_M$$
18	17	eqcomi	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_Y$$
19	1 18 5 4 6	prdsbas2	$$⊢\phi \to {\mathrm{Base}}_M=\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}$$
20		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
21		fnmgp	$$⊢\mathrm{mulGrp}Fn\mathrm{V}$$
22		ssv	$$⊢\mathrm{ran}R\subseteq \mathrm{V}$$
23	22	a1i	$$⊢\phi \to \mathrm{ran}R\subseteq \mathrm{V}$$
24		fnco	$$⊢\left(\mathrm{mulGrp}Fn\mathrm{V}\wedge RFnI\wedge \mathrm{ran}R\subseteq \mathrm{V}\right)\to \left(\mathrm{mulGrp}\circ R\right)FnI$$
25	21 6 23 24	mp3an2i	$$⊢\phi \to \left(\mathrm{mulGrp}\circ R\right)FnI$$
26	3 20 5 4 25	prdsbas2	$$⊢\phi \to {\mathrm{Base}}_Z=\underset{x\in I}{⨉}{\mathrm{Base}}_{\left(\mathrm{mulGrp}\circ R\right)\left(x\right)}$$
27	15 19 26	3eqtr4d	$$⊢\phi \to {\mathrm{Base}}_M={\mathrm{Base}}_Z$$
28		eqid	$$⊢{\cdot }_Y={\cdot }_Y$$
29	2 28	mgpplusg	$$⊢{\cdot }_Y={+}_M$$
30		eqid	$$⊢{\mathrm{mulGrp}}_{R\left(z\right)}={\mathrm{mulGrp}}_{R\left(z\right)}$$
31		eqid	$$⊢{\cdot }_{R\left(z\right)}={\cdot }_{R\left(z\right)}$$
32	30 31	mgpplusg	$$⊢{\cdot }_{R\left(z\right)}={+}_{{\mathrm{mulGrp}}_{R\left(z\right)}}$$
33		fvco2	$$⊢\left(RFnI\wedge z\in I\right)\to \left(\mathrm{mulGrp}\circ R\right)\left(z\right)={\mathrm{mulGrp}}_{R\left(z\right)}$$
34	6 33	sylan	$$⊢\left(\phi \wedge z\in I\right)\to \left(\mathrm{mulGrp}\circ R\right)\left(z\right)={\mathrm{mulGrp}}_{R\left(z\right)}$$
35	34	eqcomd	$$⊢\left(\phi \wedge z\in I\right)\to {\mathrm{mulGrp}}_{R\left(z\right)}=\left(\mathrm{mulGrp}\circ R\right)\left(z\right)$$
36	35	fveq2d	$$⊢\left(\phi \wedge z\in I\right)\to {+}_{{\mathrm{mulGrp}}_{R\left(z\right)}}={+}_{\left(\mathrm{mulGrp}\circ R\right)\left(z\right)}$$
37	32 36	syl5eq	$$⊢\left(\phi \wedge z\in I\right)\to {\cdot }_{R\left(z\right)}={+}_{\left(\mathrm{mulGrp}\circ R\right)\left(z\right)}$$
38	37	oveqd	$$⊢\left(\phi \wedge z\in I\right)\to x\left(z\right){\cdot }_{R\left(z\right)}y\left(z\right)=x\left(z\right){+}_{\left(\mathrm{mulGrp}\circ R\right)\left(z\right)}y\left(z\right)$$
39	38	mpteq2dva	$$⊢\phi \to \left(z\in I⟼x\left(z\right){\cdot }_{R\left(z\right)}y\left(z\right)\right)=\left(z\in I⟼x\left(z\right){+}_{\left(\mathrm{mulGrp}\circ R\right)\left(z\right)}y\left(z\right)\right)$$
40	27 27 39	mpoeq123dv	$$⊢\phi \to \left(x\in {\mathrm{Base}}_M,y\in {\mathrm{Base}}_M⟼\left(z\in I⟼x\left(z\right){\cdot }_{R\left(z\right)}y\left(z\right)\right)\right)=\left(x\in {\mathrm{Base}}_Z,y\in {\mathrm{Base}}_Z⟼\left(z\in I⟼x\left(z\right){+}_{\left(\mathrm{mulGrp}\circ R\right)\left(z\right)}y\left(z\right)\right)\right)$$
41		fnex	$$⊢\left(RFnI\wedge I\in V\right)\to R\in \mathrm{V}$$
42	6 4 41	syl2anc	$$⊢\phi \to R\in \mathrm{V}$$
43	6	fndmd	$$⊢\phi \to \mathrm{dom}R=I$$
44	1 5 42 18 43 28	prdsmulr	$$⊢\phi \to {\cdot }_Y=\left(x\in {\mathrm{Base}}_M,y\in {\mathrm{Base}}_M⟼\left(z\in I⟼x\left(z\right){\cdot }_{R\left(z\right)}y\left(z\right)\right)\right)$$
45		fnex	$$⊢\left(\left(\mathrm{mulGrp}\circ R\right)FnI\wedge I\in V\right)\to \mathrm{mulGrp}\circ R\in \mathrm{V}$$
46	25 4 45	syl2anc	$$⊢\phi \to \mathrm{mulGrp}\circ R\in \mathrm{V}$$
47	25	fndmd	$$⊢\phi \to \mathrm{dom}\left(\mathrm{mulGrp}\circ R\right)=I$$
48		eqid	$$⊢{+}_Z={+}_Z$$
49	3 5 46 20 47 48	prdsplusg	$$⊢\phi \to {+}_Z=\left(x\in {\mathrm{Base}}_Z,y\in {\mathrm{Base}}_Z⟼\left(z\in I⟼x\left(z\right){+}_{\left(\mathrm{mulGrp}\circ R\right)\left(z\right)}y\left(z\right)\right)\right)$$
50	40 44 49	3eqtr4d	$$⊢\phi \to {\cdot }_Y={+}_Z$$
51	29 50	syl5eqr	$$⊢\phi \to {+}_M={+}_Z$$
52	27 51	jca	$$⊢\phi \to \left({\mathrm{Base}}_M={\mathrm{Base}}_Z\wedge {+}_M={+}_Z\right)$$