Theorem evls1monply1

Description: Subring evaluation of a scaled monomial. (Contributed by Thierry Arnoux, 10-Jan-2026)

	Ref	Expression
Hypotheses	evls1monply1.1	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
	evls1monply1.2	$$⊢K={\mathrm{Base}}_S$$
	evls1monply1.3	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
	evls1monply1.4	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evls1monply1.5	$$⊢X={\mathrm{var}}_1\left(U\right)$$
	evls1monply1.6	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_W}$$
	evls1monply1.7	$$⊢\underset{\dot{}}{\wedge }={\cdot }_{{\mathrm{mulGrp}}_S}$$
	evls1monply1.8	$$⊢\underset{\dot{}}{\ast }={\cdot }_W$$
	evls1monply1.9	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	evls1monply1.10	$$⊢\phi \to S\in \mathrm{CRing}$$
	evls1monply1.11	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evls1monply1.12	$$⊢\phi \to A\in R$$
	evls1monply1.13	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	evls1monply1.14	$$⊢\phi \to Y\in K$$
Assertion	evls1monply1	$$⊢\phi \to Q\left(A\underset{\dot{}}{\ast }\left(N\underset{\dot{}}{\times }X\right)\right)\left(Y\right)=A\underset{\dot{}}{·}\left(N\underset{\dot{}}{\wedge }Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		evls1monply1.1	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		evls1monply1.2	$$⊢K={\mathrm{Base}}_S$$
3		evls1monply1.3	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
4		evls1monply1.4	$$⊢U=S{\upharpoonright }_{𝑠}R$$
5		evls1monply1.5	$$⊢X={\mathrm{var}}_1\left(U\right)$$
6		evls1monply1.6	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_W}$$
7		evls1monply1.7	$$⊢\underset{\dot{}}{\wedge }={\cdot }_{{\mathrm{mulGrp}}_S}$$
8		evls1monply1.8	$$⊢\underset{\dot{}}{\ast }={\cdot }_W$$
9		evls1monply1.9	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
10		evls1monply1.10	$$⊢\phi \to S\in \mathrm{CRing}$$
11		evls1monply1.11	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
12		evls1monply1.12	$$⊢\phi \to A\in R$$
13		evls1monply1.13	$$⊢\phi \to N\in {\mathbb{N}}_0$$
14		evls1monply1.14	$$⊢\phi \to Y\in K$$
15		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
16		eqid	$$⊢{\mathrm{mulGrp}}_W={\mathrm{mulGrp}}_W$$
17	16 15	mgpbas	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_{{\mathrm{mulGrp}}_W}$$
18	4	subrgring	$$⊢R\in \mathrm{SubRing}\left(S\right)\to U\in \mathrm{Ring}$$
19	11 18	syl	$$⊢\phi \to U\in \mathrm{Ring}$$
20	3	ply1ring	$$⊢U\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
21	16	ringmgp	$$⊢W\in \mathrm{Ring}\to {\mathrm{mulGrp}}_W\in \mathrm{Mnd}$$
22	19 20 21	3syl	$$⊢\phi \to {\mathrm{mulGrp}}_W\in \mathrm{Mnd}$$
23	5 3 15	vr1cl	$$⊢U\in \mathrm{Ring}\to X\in {\mathrm{Base}}_W$$
24	19 23	syl	$$⊢\phi \to X\in {\mathrm{Base}}_W$$
25	17 6 22 13 24	mulgnn0cld	$$⊢\phi \to N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_W$$
26	1 2 3 4 15 8 9 10 11 12 25 14	evls1vsca	$$⊢\phi \to Q\left(A\underset{\dot{}}{\ast }\left(N\underset{\dot{}}{\times }X\right)\right)\left(Y\right)=A\underset{\dot{}}{·}Q\left(N\underset{\dot{}}{\times }X\right)\left(Y\right)$$
27	1 4 3 5 2 6 7 10 11 13 14	evls1varpwval	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)\left(Y\right)=N\underset{\dot{}}{\wedge }Y$$
28	27	oveq2d	$$⊢\phi \to A\underset{\dot{}}{·}Q\left(N\underset{\dot{}}{\times }X\right)\left(Y\right)=A\underset{\dot{}}{·}\left(N\underset{\dot{}}{\wedge }Y\right)$$
29	26 28	eqtrd	$$⊢\phi \to Q\left(A\underset{\dot{}}{\ast }\left(N\underset{\dot{}}{\times }X\right)\right)\left(Y\right)=A\underset{\dot{}}{·}\left(N\underset{\dot{}}{\wedge }Y\right)$$