evl1scvarpwval

Description: Value of a univariate polynomial evaluation mapping a multiple of an exponentiation of a variable to the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-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}$
	evl1scvarpw.t1	$⊢ \underset{˙}{\times} = \cdot_{W}$
	evl1scvarpw.a	$⊢ φ \to A \in B$
	evl1scvarpwval.c	$⊢ φ \to C \in B$
	evl1scvarpwval.h	$⊢ H = {mulGrp}_{R}$
	evl1scvarpwval.e	$⊢ E = \cdot_{H}$
	evl1scvarpwval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	evl1scvarpwval	$⊢ φ \to Q (A \underset{˙}{\times} (N \underset{˙}{\times} X)) (C) = A \underset{˙}{\cdot} (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		evl1scvarpw.t1	$⊢ \underset{˙}{\times} = \cdot_{W}$
10		evl1scvarpw.a	$⊢ φ \to A \in B$
11		evl1scvarpwval.c	$⊢ φ \to C \in B$
12		evl1scvarpwval.h	$⊢ H = {mulGrp}_{R}$
13		evl1scvarpwval.e	$⊢ E = \cdot_{H}$
14		evl1scvarpwval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
15		eqid	$⊢ {Base}_{W} = {Base}_{W}$
16	3 15	mgpbas	$⊢ {Base}_{W} = {Base}_{G}$
17		crngring	$⊢ R \in CRing \to R \in Ring$
18	7 17	syl	$⊢ φ \to R \in Ring$
19	2	ply1ring	$⊢ R \in Ring \to W \in Ring$
20	18 19	syl	$⊢ φ \to W \in Ring$
21	3	ringmgp	$⊢ W \in Ring \to G \in Mnd$
22	20 21	syl	$⊢ φ \to G \in Mnd$
23	4 2 15	vr1cl	$⊢ R \in Ring \to X \in {Base}_{W}$
24	18 23	syl	$⊢ φ \to X \in {Base}_{W}$
25	16 6 22 8 24	mulgnn0cld	$⊢ φ \to N \underset{˙}{\times} X \in {Base}_{W}$
26	1 2 3 4 5 6 7 8 11 12 13	evl1varpwval	$⊢ φ \to Q (N \underset{˙}{\times} X) (C) = N E C$
27	25 26	jca	$⊢ φ \to (N \underset{˙}{\times} X \in {Base}_{W} \land Q (N \underset{˙}{\times} X) (C) = N E C)$
28	1 2 5 15 7 11 27 10 9 14	evl1vsd	$⊢ φ \to (A \underset{˙}{\times} (N \underset{˙}{\times} X) \in {Base}_{W} \land Q (A \underset{˙}{\times} (N \underset{˙}{\times} X)) (C) = A \underset{˙}{\cdot} (N E C))$
29	28	simprd	$⊢ φ \to Q (A \underset{˙}{\times} (N \underset{˙}{\times} X)) (C) = A \underset{˙}{\cdot} (N E C)$

Metamath Proof Explorer

Theorem evl1scvarpwval

Proof