Theorem srapwov

Description: The "power" operation on a subring algebra. (Contributed by Thierry Arnoux, 10-Jan-2026)

	Ref	Expression
Hypotheses	srapwov.a	$$⊢A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
	srapwov.w	$$⊢\phi \to W\in \mathrm{Ring}$$
	srapwov.s	$$⊢\phi \to S\subseteq {\mathrm{Base}}_W$$
Assertion	srapwov	$$⊢\phi \to {\cdot }_{{\mathrm{mulGrp}}_W}={\cdot }_{{\mathrm{mulGrp}}_A}$$

Proof

Step	Hyp	Ref	Expression
1		srapwov.a	$$⊢A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
2		srapwov.w	$$⊢\phi \to W\in \mathrm{Ring}$$
3		srapwov.s	$$⊢\phi \to S\subseteq {\mathrm{Base}}_W$$
4		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_W}={\cdot }_{{\mathrm{mulGrp}}_W}$$
5		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_A}={\cdot }_{{\mathrm{mulGrp}}_A}$$
6		eqid	$$⊢{\mathrm{mulGrp}}_W={\mathrm{mulGrp}}_W$$
7		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
8	6 7	mgpbas	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_{{\mathrm{mulGrp}}_W}$$
9	8	a1i	$$⊢\phi \to {\mathrm{Base}}_W={\mathrm{Base}}_{{\mathrm{mulGrp}}_W}$$
10	1	a1i	$$⊢\phi \to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
11	10 3	srabase	$$⊢\phi \to {\mathrm{Base}}_W={\mathrm{Base}}_A$$
12		eqid	$$⊢{\mathrm{mulGrp}}_A={\mathrm{mulGrp}}_A$$
13		eqid	$$⊢{\mathrm{Base}}_A={\mathrm{Base}}_A$$
14	12 13	mgpbas	$$⊢{\mathrm{Base}}_A={\mathrm{Base}}_{{\mathrm{mulGrp}}_A}$$
15	11 14	eqtrdi	$$⊢\phi \to {\mathrm{Base}}_W={\mathrm{Base}}_{{\mathrm{mulGrp}}_A}$$
16		ssidd	$$⊢\phi \to {\mathrm{Base}}_W\subseteq {\mathrm{Base}}_W$$
17		eqid	$$⊢{\cdot }_W={\cdot }_W$$
18	6 17	mgpplusg	$$⊢{\cdot }_W={+}_{{\mathrm{mulGrp}}_W}$$
19	18	eqcomi	$$⊢{+}_{{\mathrm{mulGrp}}_W}={\cdot }_W$$
20	2	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_W\wedge y\in {\mathrm{Base}}_W\right)\right)\to W\in \mathrm{Ring}$$
21		simprl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_W\wedge y\in {\mathrm{Base}}_W\right)\right)\to x\in {\mathrm{Base}}_W$$
22		simprr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_W\wedge y\in {\mathrm{Base}}_W\right)\right)\to y\in {\mathrm{Base}}_W$$
23	7 19 20 21 22	ringcld	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_W\wedge y\in {\mathrm{Base}}_W\right)\right)\to x{+}_{{\mathrm{mulGrp}}_W}y\in {\mathrm{Base}}_W$$
24	10 3	sramulr	$$⊢\phi \to {\cdot }_W={\cdot }_A$$
25	1	fveq2i	$$⊢{\mathrm{mulGrp}}_A={\mathrm{mulGrp}}_{\mathrm{subringAlg}\left(W\right)\left(S\right)}$$
26	1	fveq2i	$$⊢{\cdot }_A={\cdot }_{\mathrm{subringAlg}\left(W\right)\left(S\right)}$$
27	25 26	mgpplusg	$$⊢{\cdot }_A={+}_{{\mathrm{mulGrp}}_A}$$
28	24 18 27	3eqtr3g	$$⊢\phi \to {+}_{{\mathrm{mulGrp}}_W}={+}_{{\mathrm{mulGrp}}_A}$$
29	28	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_W\wedge y\in {\mathrm{Base}}_W\right)\right)\to x{+}_{{\mathrm{mulGrp}}_W}y=x{+}_{{\mathrm{mulGrp}}_A}y$$
30	4 5 9 15 16 23 29	mulgpropd	$$⊢\phi \to {\cdot }_{{\mathrm{mulGrp}}_W}={\cdot }_{{\mathrm{mulGrp}}_A}$$