Theorem subrgmvr

Description: The variables in a subring polynomial algebra are the same as the original ring. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	subrgmvr.v	$$⊢V=I\mathrm{mVar}R$$
	subrgmvr.i	$$⊢\phi \to I\in W$$
	subrgmvr.r	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
	subrgmvr.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
Assertion	subrgmvr	$$⊢\phi \to V=I\mathrm{mVar}H$$

Proof

Step	Hyp	Ref	Expression
1		subrgmvr.v	$$⊢V=I\mathrm{mVar}R$$
2		subrgmvr.i	$$⊢\phi \to I\in W$$
3		subrgmvr.r	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
4		subrgmvr.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
5		eqid	$$⊢1_R=1_R$$
6	4 5	subrg1	$$⊢T\in \mathrm{SubRing}\left(R\right)\to 1_R=1_H$$
7	3 6	syl	$$⊢\phi \to 1_R=1_H$$
8		eqid	$$⊢0_R=0_R$$
9	4 8	subrg0	$$⊢T\in \mathrm{SubRing}\left(R\right)\to 0_R=0_H$$
10	3 9	syl	$$⊢\phi \to 0_R=0_H$$
11	7 10	ifeq12d	$$⊢\phi \to if\left(y=\left(z\in I⟼if\left(z=x,1,0\right)\right),1_R,0_R\right)=if\left(y=\left(z\in I⟼if\left(z=x,1,0\right)\right),1_H,0_H\right)$$
12	11	mpteq2dv	$$⊢\phi \to \left(y\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(y=\left(z\in I⟼if\left(z=x,1,0\right)\right),1_R,0_R\right)\right)=\left(y\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(y=\left(z\in I⟼if\left(z=x,1,0\right)\right),1_H,0_H\right)\right)$$
13	12	mpteq2dv	$$⊢\phi \to \left(x\in I⟼\left(y\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(y=\left(z\in I⟼if\left(z=x,1,0\right)\right),1_R,0_R\right)\right)\right)=\left(x\in I⟼\left(y\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(y=\left(z\in I⟼if\left(z=x,1,0\right)\right),1_H,0_H\right)\right)\right)$$
14		eqid	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
15		subrgrcl	$$⊢T\in \mathrm{SubRing}\left(R\right)\to R\in \mathrm{Ring}$$
16	3 15	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
17	1 14 8 5 2 16	mvrfval	$$⊢\phi \to V=\left(x\in I⟼\left(y\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(y=\left(z\in I⟼if\left(z=x,1,0\right)\right),1_R,0_R\right)\right)\right)$$
18		eqid	$$⊢I\mathrm{mVar}H=I\mathrm{mVar}H$$
19		eqid	$$⊢0_H=0_H$$
20		eqid	$$⊢1_H=1_H$$
21	4	ovexi	$$⊢H\in \mathrm{V}$$
22	21	a1i	$$⊢\phi \to H\in \mathrm{V}$$
23	18 14 19 20 2 22	mvrfval	$$⊢\phi \to I\mathrm{mVar}H=\left(x\in I⟼\left(y\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(y=\left(z\in I⟼if\left(z=x,1,0\right)\right),1_H,0_H\right)\right)\right)$$
24	13 17 23	3eqtr4d	$$⊢\phi \to V=I\mathrm{mVar}H$$