evls1monply1

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

	Ref	Expression
Hypotheses	evls1monply1.1	$⊢ Q = S {evalSub}_{1} R$
	evls1monply1.2	$⊢ K = {Base}_{S}$
	evls1monply1.3	$⊢ W = {Poly}_{1} (U)$
	evls1monply1.4	$⊢ U = S ↾_{𝑠} R$
	evls1monply1.5	$⊢ X = {var}_{1} (U)$
	evls1monply1.6	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{W}}$
	evls1monply1.7	$⊢ \underset{˙}{\land} = \cdot_{{mulGrp}_{S}}$
	evls1monply1.8	$⊢ \underset{˙}{*} = \cdot_{W}$
	evls1monply1.9	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	evls1monply1.10	$⊢ φ \to S \in CRing$
	evls1monply1.11	$⊢ φ \to R \in SubRing (S)$
	evls1monply1.12	$⊢ φ \to A \in R$
	evls1monply1.13	$⊢ φ \to N \in ℕ_{0}$
	evls1monply1.14	$⊢ φ \to Y \in K$
Assertion	evls1monply1	$⊢ φ \to Q (A \underset{˙}{*} (N \underset{˙}{\times} X)) (Y) = A \underset{˙}{\cdot} (N \underset{˙}{\land} Y)$

Proof

Step	Hyp	Ref	Expression
1		evls1monply1.1	$⊢ Q = S {evalSub}_{1} R$
2		evls1monply1.2	$⊢ K = {Base}_{S}$
3		evls1monply1.3	$⊢ W = {Poly}_{1} (U)$
4		evls1monply1.4	$⊢ U = S ↾_{𝑠} R$
5		evls1monply1.5	$⊢ X = {var}_{1} (U)$
6		evls1monply1.6	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{W}}$
7		evls1monply1.7	$⊢ \underset{˙}{\land} = \cdot_{{mulGrp}_{S}}$
8		evls1monply1.8	$⊢ \underset{˙}{*} = \cdot_{W}$
9		evls1monply1.9	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
10		evls1monply1.10	$⊢ φ \to S \in CRing$
11		evls1monply1.11	$⊢ φ \to R \in SubRing (S)$
12		evls1monply1.12	$⊢ φ \to A \in R$
13		evls1monply1.13	$⊢ φ \to N \in ℕ_{0}$
14		evls1monply1.14	$⊢ φ \to Y \in K$
15		eqid	$⊢ {Base}_{W} = {Base}_{W}$
16		eqid	$⊢ {mulGrp}_{W} = {mulGrp}_{W}$
17	16 15	mgpbas	$⊢ {Base}_{W} = {Base}_{{mulGrp}_{W}}$
18	4	subrgring	$⊢ R \in SubRing (S) \to U \in Ring$
19	11 18	syl	$⊢ φ \to U \in Ring$
20	3	ply1ring	$⊢ U \in Ring \to W \in Ring$
21	16	ringmgp	$⊢ W \in Ring \to {mulGrp}_{W} \in Mnd$
22	19 20 21	3syl	$⊢ φ \to {mulGrp}_{W} \in Mnd$
23	5 3 15	vr1cl	$⊢ U \in Ring \to X \in {Base}_{W}$
24	19 23	syl	$⊢ φ \to X \in {Base}_{W}$
25	17 6 22 13 24	mulgnn0cld	$⊢ φ \to N \underset{˙}{\times} X \in {Base}_{W}$
26	1 2 3 4 15 8 9 10 11 12 25 14	evls1vsca	$⊢ φ \to Q (A \underset{˙}{*} (N \underset{˙}{\times} X)) (Y) = A \underset{˙}{\cdot} Q (N \underset{˙}{\times} X) (Y)$
27	1 4 3 5 2 6 7 10 11 13 14	evls1varpwval	$⊢ φ \to Q (N \underset{˙}{\times} X) (Y) = N \underset{˙}{\land} Y$
28	27	oveq2d	$⊢ φ \to A \underset{˙}{\cdot} Q (N \underset{˙}{\times} X) (Y) = A \underset{˙}{\cdot} (N \underset{˙}{\land} Y)$
29	26 28	eqtrd	$⊢ φ \to Q (A \underset{˙}{*} (N \underset{˙}{\times} X)) (Y) = A \underset{˙}{\cdot} (N \underset{˙}{\land} Y)$

Metamath Proof Explorer

Theorem evls1monply1

Proof