evlspw

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

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

Proof

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

Metamath Proof Explorer

Theorem evlspw

Proof