evlsvarpw

Description: Polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by SN, 21-Feb-2024)

	Ref	Expression
Hypotheses	evlsvarpw.q	$⊢ Q = (I evalSub S) (R)$
	evlsvarpw.w	$⊢ W = I mPoly U$
	evlsvarpw.g	$⊢ G = {mulGrp}_{W}$
	evlsvarpw.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
	evlsvarpw.x	$⊢ X = (I mVar U) (Y)$
	evlsvarpw.u	$⊢ U = S ↾_{𝑠} R$
	evlsvarpw.p	$⊢ P = S ↑_{𝑠} (B^{I})$
	evlsvarpw.h	$⊢ H = {mulGrp}_{P}$
	evlsvarpw.b	$⊢ B = {Base}_{S}$
	evlsvarpw.i	$⊢ φ \to I \in V$
	evlsvarpw.y	$⊢ φ \to Y \in I$
	evlsvarpw.s	$⊢ φ \to S \in CRing$
	evlsvarpw.r	$⊢ φ \to R \in SubRing (S)$
	evlsvarpw.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	evlsvarpw	$⊢ φ \to Q (N \underset{˙}{\times} X) = N \cdot_{H} Q (X)$

Proof

Step	Hyp	Ref	Expression
1		evlsvarpw.q	$⊢ Q = (I evalSub S) (R)$
2		evlsvarpw.w	$⊢ W = I mPoly U$
3		evlsvarpw.g	$⊢ G = {mulGrp}_{W}$
4		evlsvarpw.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
5		evlsvarpw.x	$⊢ X = (I mVar U) (Y)$
6		evlsvarpw.u	$⊢ U = S ↾_{𝑠} R$
7		evlsvarpw.p	$⊢ P = S ↑_{𝑠} (B^{I})$
8		evlsvarpw.h	$⊢ H = {mulGrp}_{P}$
9		evlsvarpw.b	$⊢ B = {Base}_{S}$
10		evlsvarpw.i	$⊢ φ \to I \in V$
11		evlsvarpw.y	$⊢ φ \to Y \in I$
12		evlsvarpw.s	$⊢ φ \to S \in CRing$
13		evlsvarpw.r	$⊢ φ \to R \in SubRing (S)$
14		evlsvarpw.n	$⊢ φ \to N \in ℕ_{0}$
15		eqid	$⊢ {Base}_{W} = {Base}_{W}$
16		eqid	$⊢ I mVar U = I mVar U$
17	6	subrgring	$⊢ R \in SubRing (S) \to U \in Ring$
18	13 17	syl	$⊢ φ \to U \in Ring$
19	2 16 15 10 18 11	mvrcl	$⊢ φ \to (I mVar U) (Y) \in {Base}_{W}$
20	5 19	eqeltrid	$⊢ φ \to X \in {Base}_{W}$
21	1 2 3 4 6 7 8 9 15 10 12 13 14 20	evlspw	$⊢ φ \to Q (N \underset{˙}{\times} X) = N \cdot_{H} Q (X)$

Metamath Proof Explorer

Theorem evlsvarpw

Proof