evls1pw

Description: Univariate 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	evls1pw.q	$⊢ Q = S {evalSub}_{1} R$
	evls1pw.u	$⊢ U = S ↾_{𝑠} R$
	evls1pw.w	$⊢ W = {Poly}_{1} (U)$
	evls1pw.g	$⊢ G = {mulGrp}_{W}$
	evls1pw.k	$⊢ K = {Base}_{S}$
	evls1pw.b	$⊢ B = {Base}_{W}$
	evls1pw.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
	evls1pw.s	$⊢ φ \to S \in CRing$
	evls1pw.r	$⊢ φ \to R \in SubRing (S)$
	evls1pw.n	$⊢ φ \to N \in ℕ_{0}$
	evls1pw.x	$⊢ φ \to X \in B$
Assertion	evls1pw	$⊢ φ \to Q (N \underset{˙}{\times} X) = N \cdot_{{mulGrp}_{(S ↑_{𝑠} K)}} Q (X)$

Proof

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

Metamath Proof Explorer

Theorem evls1pw

Proof