Theorem subrgasclcl

Description: The scalars in a polynomial algebra are in the subring algebra iff the scalar value is in the subring. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	subrgascl.p	$$⊢P=I\mathrm{mPoly}R$$
	subrgascl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	subrgascl.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
	subrgascl.u	$$⊢U=I\mathrm{mPoly}H$$
	subrgascl.i	$$⊢\phi \to I\in W$$
	subrgascl.r	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
	subrgasclcl.b	$$⊢B={\mathrm{Base}}_U$$
	subrgasclcl.k	$$⊢K={\mathrm{Base}}_R$$
	subrgasclcl.x	$$⊢\phi \to X\in K$$
Assertion	subrgasclcl	$$⊢\phi \to \left(A\left(X\right)\in B\leftrightarrow X\in T\right)$$

Proof

Step	Hyp	Ref	Expression
1		subrgascl.p	$$⊢P=I\mathrm{mPoly}R$$
2		subrgascl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
3		subrgascl.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
4		subrgascl.u	$$⊢U=I\mathrm{mPoly}H$$
5		subrgascl.i	$$⊢\phi \to I\in W$$
6		subrgascl.r	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
7		subrgasclcl.b	$$⊢B={\mathrm{Base}}_U$$
8		subrgasclcl.k	$$⊢K={\mathrm{Base}}_R$$
9		subrgasclcl.x	$$⊢\phi \to X\in K$$
10		iftrue	$$⊢x=I\times \left\{0\right\}\to if\left(x=I\times \left\{0\right\},X,0_R\right)=X$$
11	10	eleq1d	$$⊢x=I\times \left\{0\right\}\to \left(if\left(x=I\times \left\{0\right\},X,0_R\right)\in {\mathrm{Base}}_H\leftrightarrow X\in {\mathrm{Base}}_H\right)$$
12		eqid	$$⊢I\mathrm{mPwSer}H=I\mathrm{mPwSer}H$$
13		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
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		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}$$
16		eqid	$$⊢0_R=0_R$$
17		subrgrcl	$$⊢T\in \mathrm{SubRing}\left(R\right)\to R\in \mathrm{Ring}$$
18	6 17	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
19	1 14 16 8 2 5 18 9	mplascl	$$⊢\phi \to A\left(X\right)=\left(x\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(x=I\times \left\{0\right\},X,0_R\right)\right)$$
20	19	adantr	$$⊢\left(\phi \wedge A\left(X\right)\in B\right)\to A\left(X\right)=\left(x\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(x=I\times \left\{0\right\},X,0_R\right)\right)$$
21	3	subrgring	$$⊢T\in \mathrm{SubRing}\left(R\right)\to H\in \mathrm{Ring}$$
22	6 21	syl	$$⊢\phi \to H\in \mathrm{Ring}$$
23	12 4 7 5 22	mplsubrg	$$⊢\phi \to B\in \mathrm{SubRing}\left(I\mathrm{mPwSer}H\right)$$
24	15	subrgss	$$⊢B\in \mathrm{SubRing}\left(I\mathrm{mPwSer}H\right)\to B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}$$
25	23 24	syl	$$⊢\phi \to B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}$$
26	25	sselda	$$⊢\left(\phi \wedge A\left(X\right)\in B\right)\to A\left(X\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}$$
27	20 26	eqeltrrd	$$⊢\left(\phi \wedge A\left(X\right)\in B\right)\to \left(x\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(x=I\times \left\{0\right\},X,0_R\right)\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}H\right)}$$
28	12 13 14 15 27	psrelbas	$$⊢\left(\phi \wedge A\left(X\right)\in B\right)\to \left(x\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(x=I\times \left\{0\right\},X,0_R\right)\right):\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_H$$
29		eqid	$$⊢\left(x\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(x=I\times \left\{0\right\},X,0_R\right)\right)=\left(x\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(x=I\times \left\{0\right\},X,0_R\right)\right)$$
30	29	fmpt	$$⊢\forall x\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}if\left(x=I\times \left\{0\right\},X,0_R\right)\in {\mathrm{Base}}_H\leftrightarrow \left(x\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(x=I\times \left\{0\right\},X,0_R\right)\right):\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_H$$
31	28 30	sylibr	$$⊢\left(\phi \wedge A\left(X\right)\in B\right)\to \forall x\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}if\left(x=I\times \left\{0\right\},X,0_R\right)\in {\mathrm{Base}}_H$$
32	5	adantr	$$⊢\left(\phi \wedge A\left(X\right)\in B\right)\to I\in W$$
33	14	psrbag0	$$⊢I\in W\to I\times \left\{0\right\}\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
34	32 33	syl	$$⊢\left(\phi \wedge A\left(X\right)\in B\right)\to I\times \left\{0\right\}\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
35	11 31 34	rspcdva	$$⊢\left(\phi \wedge A\left(X\right)\in B\right)\to X\in {\mathrm{Base}}_H$$
36	3	subrgbas	$$⊢T\in \mathrm{SubRing}\left(R\right)\to T={\mathrm{Base}}_H$$
37	6 36	syl	$$⊢\phi \to T={\mathrm{Base}}_H$$
38	37	adantr	$$⊢\left(\phi \wedge A\left(X\right)\in B\right)\to T={\mathrm{Base}}_H$$
39	35 38	eleqtrrd	$$⊢\left(\phi \wedge A\left(X\right)\in B\right)\to X\in T$$
40		eqid	$$⊢\mathrm{algSc}\left(U\right)=\mathrm{algSc}\left(U\right)$$
41	1 2 3 4 5 6 40	subrgascl	$$⊢\phi \to \mathrm{algSc}\left(U\right)={A\upharpoonright }_T$$
42	41	fveq1d	$$⊢\phi \to \mathrm{algSc}\left(U\right)\left(X\right)=\left({A\upharpoonright }_T\right)\left(X\right)$$
43		fvres	$$⊢X\in T\to \left({A\upharpoonright }_T\right)\left(X\right)=A\left(X\right)$$
44	42 43	sylan9eq	$$⊢\left(\phi \wedge X\in T\right)\to \mathrm{algSc}\left(U\right)\left(X\right)=A\left(X\right)$$
45		eqid	$$⊢\mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(U\right)$$
46	4	mplring	$$⊢\left(I\in W\wedge H\in \mathrm{Ring}\right)\to U\in \mathrm{Ring}$$
47	4	mpllmod	$$⊢\left(I\in W\wedge H\in \mathrm{Ring}\right)\to U\in \mathrm{LMod}$$
48		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
49	40 45 46 47 48 7	asclf	$$⊢\left(I\in W\wedge H\in \mathrm{Ring}\right)\to \mathrm{algSc}\left(U\right):{\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}⟶B$$
50	5 22 49	syl2anc	$$⊢\phi \to \mathrm{algSc}\left(U\right):{\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}⟶B$$
51	50	adantr	$$⊢\left(\phi \wedge X\in T\right)\to \mathrm{algSc}\left(U\right):{\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}⟶B$$
52	4 5 22	mplsca	$$⊢\phi \to H=\mathrm{Scalar}\left(U\right)$$
53	52	fveq2d	$$⊢\phi \to {\mathrm{Base}}_H={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
54	37 53	eqtrd	$$⊢\phi \to T={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
55	54	eleq2d	$$⊢\phi \to \left(X\in T\leftrightarrow X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}\right)$$
56	55	biimpa	$$⊢\left(\phi \wedge X\in T\right)\to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
57	51 56	ffvelrnd	$$⊢\left(\phi \wedge X\in T\right)\to \mathrm{algSc}\left(U\right)\left(X\right)\in B$$
58	44 57	eqeltrrd	$$⊢\left(\phi \wedge X\in T\right)\to A\left(X\right)\in B$$
59	39 58	impbida	$$⊢\phi \to \left(A\left(X\right)\in B\leftrightarrow X\in T\right)$$