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

Metamath Proof Explorer

Theorem evl1varpwval

Description: Value of a univariate polynomial evaluation mapping the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019)

		Ref	Expression
	Hypotheses	evl1varpw.q	$⊢ Q = {eval}_{1} (R)$
		evl1varpw.w	$⊢ W = {Poly}_{1} (R)$
		evl1varpw.g	$⊢ G = {mulGrp}_{W}$
		evl1varpw.x	$⊢ X = {var}_{1} (R)$
		evl1varpw.b	$⊢ B = {Base}_{R}$
		evl1varpw.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
		evl1varpw.r	$⊢ φ \to R \in CRing$
		evl1varpw.n	$⊢ φ \to N \in ℕ_{0}$
		evl1varpwval.c	$⊢ φ \to C \in B$
		evl1varpwval.h	$⊢ H = {mulGrp}_{R}$
		evl1varpwval.e	$⊢ E = \cdot_{H}$
	Assertion	evl1varpwval	$⊢ φ \to Q (N \underset{˙}{\times} X) (C) = N E C$

Proof

Step	Hyp	Ref	Expression
1		evl1varpw.q	$⊢ Q = {eval}_{1} (R)$
2		evl1varpw.w	$⊢ W = {Poly}_{1} (R)$
3		evl1varpw.g	$⊢ G = {mulGrp}_{W}$
4		evl1varpw.x	$⊢ X = {var}_{1} (R)$
5		evl1varpw.b	$⊢ B = {Base}_{R}$
6		evl1varpw.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
7		evl1varpw.r	$⊢ φ \to R \in CRing$
8		evl1varpw.n	$⊢ φ \to N \in ℕ_{0}$
9		evl1varpwval.c	$⊢ φ \to C \in B$
10		evl1varpwval.h	$⊢ H = {mulGrp}_{R}$
11		evl1varpwval.e	$⊢ E = \cdot_{H}$
12		eqid	$⊢ {Base}_{W} = {Base}_{W}$
13	1 4 5 2 12 7 9	evl1vard	$⊢ φ \to (X \in {Base}_{W} \land Q (X) (C) = C)$
14	3	fveq2i	$⊢ \cdot_{G} = \cdot_{{mulGrp}_{W}}$
15	6 14	eqtri	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{W}}$
16	10	fveq2i	$⊢ \cdot_{H} = \cdot_{{mulGrp}_{R}}$
17	11 16	eqtri	$⊢ E = \cdot_{{mulGrp}_{R}}$
18	1 2 5 12 7 9 13 15 17 8	evl1expd	$⊢ φ \to (N \underset{˙}{\times} X \in {Base}_{W} \land Q (N \underset{˙}{\times} X) (C) = N E C)$
19	18	simprd	$⊢ φ \to Q (N \underset{˙}{\times} X) (C) = N E C$