This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evls1varpw

Description: Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019)

		Ref	Expression
	Hypotheses	evls1varpw.q	$⊢ Q = S {evalSub}_{1} R$
		evls1varpw.u	$⊢ U = S ↾_{𝑠} R$
		evls1varpw.w	$⊢ W = {Poly}_{1} (U)$
		evls1varpw.g	$⊢ G = {mulGrp}_{W}$
		evls1varpw.x	$⊢ X = {var}_{1} (U)$
		evls1varpw.b	$⊢ B = {Base}_{S}$
		evls1varpw.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
		evls1varpw.s	$⊢ φ \to S \in CRing$
		evls1varpw.r	$⊢ φ \to R \in SubRing (S)$
		evls1varpw.n	$⊢ φ \to N \in ℕ_{0}$
	Assertion	evls1varpw	$⊢ φ \to Q (N \underset{˙}{\times} X) = N \cdot_{{mulGrp}_{(S ↑_{𝑠} B)}} Q (X)$

Proof

Step	Hyp	Ref	Expression
1		evls1varpw.q	$⊢ Q = S {evalSub}_{1} R$
2		evls1varpw.u	$⊢ U = S ↾_{𝑠} R$
3		evls1varpw.w	$⊢ W = {Poly}_{1} (U)$
4		evls1varpw.g	$⊢ G = {mulGrp}_{W}$
5		evls1varpw.x	$⊢ X = {var}_{1} (U)$
6		evls1varpw.b	$⊢ B = {Base}_{S}$
7		evls1varpw.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
8		evls1varpw.s	$⊢ φ \to S \in CRing$
9		evls1varpw.r	$⊢ φ \to R \in SubRing (S)$
10		evls1varpw.n	$⊢ φ \to N \in ℕ_{0}$
11		eqid	$⊢ {Base}_{W} = {Base}_{W}$
12	2	subrgring	$⊢ R \in SubRing (S) \to U \in Ring$
13	5 3 11	vr1cl	$⊢ U \in Ring \to X \in {Base}_{W}$
14	9 12 13	3syl	$⊢ φ \to X \in {Base}_{W}$
15	1 2 3 4 6 11 7 8 9 10 14	evls1pw	$⊢ φ \to Q (N \underset{˙}{\times} X) = N \cdot_{{mulGrp}_{(S ↑_{𝑠} B)}} Q (X)$