Theorem subrgascl

Description: The scalar injection function in a subring algebra is the same up to a restriction to 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)$$
	subrgascl.c	$$⊢C=\mathrm{algSc}\left(U\right)$$
Assertion	subrgascl	$$⊢\phi \to C={A\upharpoonright }_T$$

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		subrgascl.c	$$⊢C=\mathrm{algSc}\left(U\right)$$
8		eqid	$$⊢\mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(U\right)$$
9		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
10	7 8 9	asclfn	$$⊢CFn{\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
11	3	subrgbas	$$⊢T\in \mathrm{SubRing}\left(R\right)\to T={\mathrm{Base}}_H$$
12	6 11	syl	$$⊢\phi \to T={\mathrm{Base}}_H$$
13	3	ovexi	$$⊢H\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to H\in \mathrm{V}$$
15	4 5 14	mplsca	$$⊢\phi \to H=\mathrm{Scalar}\left(U\right)$$
16	15	fveq2d	$$⊢\phi \to {\mathrm{Base}}_H={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
17	12 16	eqtrd	$$⊢\phi \to T={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
18	17	fneq2d	$$⊢\phi \to \left(CFnT\leftrightarrow CFn{\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}\right)$$
19	10 18	mpbiri	$$⊢\phi \to CFnT$$
20		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
21		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
22	2 20 21	asclfn	$$⊢AFn{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
23		subrgrcl	$$⊢T\in \mathrm{SubRing}\left(R\right)\to R\in \mathrm{Ring}$$
24	6 23	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
25	1 5 24	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
26	25	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
27	26	fneq2d	$$⊢\phi \to \left(AFn{\mathrm{Base}}_R\leftrightarrow AFn{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\right)$$
28	22 27	mpbiri	$$⊢\phi \to AFn{\mathrm{Base}}_R$$
29		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
30	29	subrgss	$$⊢T\in \mathrm{SubRing}\left(R\right)\to T\subseteq {\mathrm{Base}}_R$$
31	6 30	syl	$$⊢\phi \to T\subseteq {\mathrm{Base}}_R$$
32		fnssres	$$⊢\left(AFn{\mathrm{Base}}_R\wedge T\subseteq {\mathrm{Base}}_R\right)\to \left({A\upharpoonright }_T\right)FnT$$
33	28 31 32	syl2anc	$$⊢\phi \to \left({A\upharpoonright }_T\right)FnT$$
34		fvres	$$⊢x\in T\to \left({A\upharpoonright }_T\right)\left(x\right)=A\left(x\right)$$
35	34	adantl	$$⊢\left(\phi \wedge x\in T\right)\to \left({A\upharpoonright }_T\right)\left(x\right)=A\left(x\right)$$
36		eqid	$$⊢0_R=0_R$$
37	3 36	subrg0	$$⊢T\in \mathrm{SubRing}\left(R\right)\to 0_R=0_H$$
38	6 37	syl	$$⊢\phi \to 0_R=0_H$$
39	38	ifeq2d	$$⊢\phi \to if\left(y=I\times \left\{0\right\},x,0_R\right)=if\left(y=I\times \left\{0\right\},x,0_H\right)$$
40	39	adantr	$$⊢\left(\phi \wedge x\in T\right)\to if\left(y=I\times \left\{0\right\},x,0_R\right)=if\left(y=I\times \left\{0\right\},x,0_H\right)$$
41	40	mpteq2dv	$$⊢\left(\phi \wedge x\in T\right)\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=I\times \left\{0\right\},x,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=I\times \left\{0\right\},x,0_H\right)\right)$$
42		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\}$$
43	5	adantr	$$⊢\left(\phi \wedge x\in T\right)\to I\in W$$
44	24	adantr	$$⊢\left(\phi \wedge x\in T\right)\to R\in \mathrm{Ring}$$
45	31	sselda	$$⊢\left(\phi \wedge x\in T\right)\to x\in {\mathrm{Base}}_R$$
46	1 42 36 29 2 43 44 45	mplascl	$$⊢\left(\phi \wedge x\in T\right)\to A\left(x\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=I\times \left\{0\right\},x,0_R\right)\right)$$
47		eqid	$$⊢0_H=0_H$$
48		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
49	3	subrgring	$$⊢T\in \mathrm{SubRing}\left(R\right)\to H\in \mathrm{Ring}$$
50	6 49	syl	$$⊢\phi \to H\in \mathrm{Ring}$$
51	50	adantr	$$⊢\left(\phi \wedge x\in T\right)\to H\in \mathrm{Ring}$$
52	12	eleq2d	$$⊢\phi \to \left(x\in T\leftrightarrow x\in {\mathrm{Base}}_H\right)$$
53	52	biimpa	$$⊢\left(\phi \wedge x\in T\right)\to x\in {\mathrm{Base}}_H$$
54	4 42 47 48 7 43 51 53	mplascl	$$⊢\left(\phi \wedge x\in T\right)\to C\left(x\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=I\times \left\{0\right\},x,0_H\right)\right)$$
55	41 46 54	3eqtr4d	$$⊢\left(\phi \wedge x\in T\right)\to A\left(x\right)=C\left(x\right)$$
56	35 55	eqtr2d	$$⊢\left(\phi \wedge x\in T\right)\to C\left(x\right)=\left({A\upharpoonright }_T\right)\left(x\right)$$
57	19 33 56	eqfnfvd	$$⊢\phi \to C={A\upharpoonright }_T$$