Theorem asclply1subcl

Description: Closure of the algebra scalar injection function in a polynomial on a subring. (Contributed by Thierry Arnoux, 5-Feb-2025)

	Ref	Expression
Hypotheses	asclply1subcl.1	$$⊢A=\mathrm{algSc}\left(V\right)$$
	asclply1subcl.2	$$⊢U=R{\upharpoonright }_{𝑠}S$$
	asclply1subcl.3	$$⊢V={\mathrm{Poly}}_1\left(R\right)$$
	asclply1subcl.4	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
	asclply1subcl.5	$$⊢P={\mathrm{Base}}_W$$
	asclply1subcl.6	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
	asclply1subcl.7	$$⊢\phi \to Z\in S$$
Assertion	asclply1subcl	$$⊢\phi \to A\left(Z\right)\in P$$

Proof

Step	Hyp	Ref	Expression
1		asclply1subcl.1	$$⊢A=\mathrm{algSc}\left(V\right)$$
2		asclply1subcl.2	$$⊢U=R{\upharpoonright }_{𝑠}S$$
3		asclply1subcl.3	$$⊢V={\mathrm{Poly}}_1\left(R\right)$$
4		asclply1subcl.4	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
5		asclply1subcl.5	$$⊢P={\mathrm{Base}}_W$$
6		asclply1subcl.6	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
7		asclply1subcl.7	$$⊢\phi \to Z\in S$$
8		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
9	8	subrgss	$$⊢S\in \mathrm{SubRing}\left(R\right)\to S\subseteq {\mathrm{Base}}_R$$
10	6 9	syl	$$⊢\phi \to S\subseteq {\mathrm{Base}}_R$$
11	10 7	sseldd	$$⊢\phi \to Z\in {\mathrm{Base}}_R$$
12		subrgrcl	$$⊢S\in \mathrm{SubRing}\left(R\right)\to R\in \mathrm{Ring}$$
13	3	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(V\right)$$
14	6 12 13	3syl	$$⊢\phi \to R=\mathrm{Scalar}\left(V\right)$$
15	14	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(V\right)}$$
16	11 15	eleqtrd	$$⊢\phi \to Z\in {\mathrm{Base}}_{\mathrm{Scalar}\left(V\right)}$$
17		eqid	$$⊢\mathrm{Scalar}\left(V\right)=\mathrm{Scalar}\left(V\right)$$
18		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(V\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(V\right)}$$
19		eqid	$$⊢{\cdot }_V={\cdot }_V$$
20		eqid	$$⊢1_V=1_V$$
21	1 17 18 19 20	asclval	$$⊢Z\in {\mathrm{Base}}_{\mathrm{Scalar}\left(V\right)}\to A\left(Z\right)=Z{\cdot }_V{1}_V$$
22	16 21	syl	$$⊢\phi \to A\left(Z\right)=Z{\cdot }_V{1}_V$$
23	3 2 4 5	subrgply1	$$⊢S\in \mathrm{SubRing}\left(R\right)\to P\in \mathrm{SubRing}\left(V\right)$$
24		eqid	$$⊢V{\upharpoonright }_{𝑠}P=V{\upharpoonright }_{𝑠}P$$
25	24 19	ressvsca	$$⊢P\in \mathrm{SubRing}\left(V\right)\to {\cdot }_V={\cdot }_{\left(V{\upharpoonright }_{𝑠}P\right)}$$
26	6 23 25	3syl	$$⊢\phi \to {\cdot }_V={\cdot }_{\left(V{\upharpoonright }_{𝑠}P\right)}$$
27	26	oveqd	$$⊢\phi \to Z{\cdot }_V{1}_V=Z{\cdot }_{\left(V{\upharpoonright }_{𝑠}P\right)}{1}_V$$
28		id	$$⊢\phi \to \phi$$
29	20	subrg1cl	$$⊢P\in \mathrm{SubRing}\left(V\right)\to 1_V\in P$$
30	6 23 29	3syl	$$⊢\phi \to 1_V\in P$$
31	3 2 4 5 6 24	ressply1vsca	$$⊢\left(\phi \wedge \left(Z\in S\wedge 1_V\in P\right)\right)\to Z{\cdot }_W{1}_V=Z{\cdot }_{\left(V{\upharpoonright }_{𝑠}P\right)}{1}_V$$
32	28 7 30 31	syl12anc	$$⊢\phi \to Z{\cdot }_W{1}_V=Z{\cdot }_{\left(V{\upharpoonright }_{𝑠}P\right)}{1}_V$$
33	27 32	eqtr4d	$$⊢\phi \to Z{\cdot }_V{1}_V=Z{\cdot }_W{1}_V$$
34	2	subrgring	$$⊢S\in \mathrm{SubRing}\left(R\right)\to U\in \mathrm{Ring}$$
35	4	ply1lmod	$$⊢U\in \mathrm{Ring}\to W\in \mathrm{LMod}$$
36	6 34 35	3syl	$$⊢\phi \to W\in \mathrm{LMod}$$
37	2 8	ressbas2	$$⊢S\subseteq {\mathrm{Base}}_R\to S={\mathrm{Base}}_U$$
38	6 9 37	3syl	$$⊢\phi \to S={\mathrm{Base}}_U$$
39	7 38	eleqtrd	$$⊢\phi \to Z\in {\mathrm{Base}}_U$$
40	2	ovexi	$$⊢U\in \mathrm{V}$$
41	4	ply1sca	$$⊢U\in \mathrm{V}\to U=\mathrm{Scalar}\left(W\right)$$
42	40 41	ax-mp	$$⊢U=\mathrm{Scalar}\left(W\right)$$
43		eqid	$$⊢{\cdot }_W={\cdot }_W$$
44		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
45	5 42 43 44	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge Z\in {\mathrm{Base}}_U\wedge 1_V\in P\right)\to Z{\cdot }_W{1}_V\in P$$
46	36 39 30 45	syl3anc	$$⊢\phi \to Z{\cdot }_W{1}_V\in P$$
47	33 46	eqeltrd	$$⊢\phi \to Z{\cdot }_V{1}_V\in P$$
48	22 47	eqeltrd	$$⊢\phi \to A\left(Z\right)\in P$$