coe1sclmul2

Description: Coefficient vector of a polynomial multiplied on the right by a scalar. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	coe1sclmul.p	$⊢ P = {Poly}_{1} (R)$
	coe1sclmul.b	$⊢ B = {Base}_{P}$
	coe1sclmul.k	$⊢ K = {Base}_{R}$
	coe1sclmul.a	$⊢ A = algSc (P)$
	coe1sclmul.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
	coe1sclmul.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	coe1sclmul2	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} (Y \underset{˙}{∙} A (X)) = {coe}_{1} (Y) {\underset{˙}{\cdot}}_{f} (ℕ_{0} \times \{X\})$

Proof

Step	Hyp	Ref	Expression
1		coe1sclmul.p	$⊢ P = {Poly}_{1} (R)$
2		coe1sclmul.b	$⊢ B = {Base}_{P}$
3		coe1sclmul.k	$⊢ K = {Base}_{R}$
4		coe1sclmul.a	$⊢ A = algSc (P)$
5		coe1sclmul.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
6		coe1sclmul.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
7		eqid	$⊢ 0_{R} = 0_{R}$
8		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
9		eqid	$⊢ \cdot_{P} = \cdot_{P}$
10		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
11		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
12		simp3	$⊢ (R \in Ring \land X \in K \land Y \in B) \to Y \in B$
13		simp1	$⊢ (R \in Ring \land X \in K \land Y \in B) \to R \in Ring$
14		simp2	$⊢ (R \in Ring \land X \in K \land Y \in B) \to X \in K$
15		0nn0	$⊢ 0 \in ℕ_{0}$
16	15	a1i	$⊢ (R \in Ring \land X \in K \land Y \in B) \to 0 \in ℕ_{0}$
17	7 3 1 8 9 10 11 2 5 6 12 13 14 16	coe1tmmul2	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} (Y \underset{˙}{∙} (X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) = (x \in ℕ_{0} ⟼ if (0 \leq x, {coe}_{1} (Y) (x - 0) \underset{˙}{\cdot} X, 0_{R}))$
18	3 1 8 9 10 11 4	ply1scltm	$⊢ (R \in Ring \land X \in K) \to A (X) = X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
19	18	3adant3	$⊢ (R \in Ring \land X \in K \land Y \in B) \to A (X) = X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
20	19	oveq2d	$⊢ (R \in Ring \land X \in K \land Y \in B) \to Y \underset{˙}{∙} A (X) = Y \underset{˙}{∙} (X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
21	20	fveq2d	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} (Y \underset{˙}{∙} A (X)) = {coe}_{1} (Y \underset{˙}{∙} (X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))))$
22		nn0ex	$⊢ ℕ_{0} \in V$
23	22	a1i	$⊢ (R \in Ring \land X \in K \land Y \in B) \to ℕ_{0} \in V$
24		fvexd	$⊢ ((R \in Ring \land X \in K \land Y \in B) \land x \in ℕ_{0}) \to {coe}_{1} (Y) (x) \in V$
25		simpl2	$⊢ ((R \in Ring \land X \in K \land Y \in B) \land x \in ℕ_{0}) \to X \in K$
26		eqid	$⊢ {coe}_{1} (Y) = {coe}_{1} (Y)$
27	26 2 1 3	coe1f	$⊢ Y \in B \to {coe}_{1} (Y) : ℕ_{0} ⟶ K$
28	27	feqmptd	$⊢ Y \in B \to {coe}_{1} (Y) = (x \in ℕ_{0} ⟼ {coe}_{1} (Y) (x))$
29	28	3ad2ant3	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} (Y) = (x \in ℕ_{0} ⟼ {coe}_{1} (Y) (x))$
30		fconstmpt	$⊢ ℕ_{0} \times \{X\} = (x \in ℕ_{0} ⟼ X)$
31	30	a1i	$⊢ (R \in Ring \land X \in K \land Y \in B) \to ℕ_{0} \times \{X\} = (x \in ℕ_{0} ⟼ X)$
32	23 24 25 29 31	offval2	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} (Y) {\underset{˙}{\cdot}}_{f} (ℕ_{0} \times \{X\}) = (x \in ℕ_{0} ⟼ {coe}_{1} (Y) (x) \underset{˙}{\cdot} X)$
33		nn0ge0	$⊢ x \in ℕ_{0} \to 0 \leq x$
34	33	iftrued	$⊢ x \in ℕ_{0} \to if (0 \leq x, {coe}_{1} (Y) (x - 0) \underset{˙}{\cdot} X, 0_{R}) = {coe}_{1} (Y) (x - 0) \underset{˙}{\cdot} X$
35		nn0cn	$⊢ x \in ℕ_{0} \to x \in ℂ$
36	35	subid1d	$⊢ x \in ℕ_{0} \to x - 0 = x$
37	36	fveq2d	$⊢ x \in ℕ_{0} \to {coe}_{1} (Y) (x - 0) = {coe}_{1} (Y) (x)$
38	37	oveq1d	$⊢ x \in ℕ_{0} \to {coe}_{1} (Y) (x - 0) \underset{˙}{\cdot} X = {coe}_{1} (Y) (x) \underset{˙}{\cdot} X$
39	34 38	eqtrd	$⊢ x \in ℕ_{0} \to if (0 \leq x, {coe}_{1} (Y) (x - 0) \underset{˙}{\cdot} X, 0_{R}) = {coe}_{1} (Y) (x) \underset{˙}{\cdot} X$
40	39	mpteq2ia	$⊢ (x \in ℕ_{0} ⟼ if (0 \leq x, {coe}_{1} (Y) (x - 0) \underset{˙}{\cdot} X, 0_{R})) = (x \in ℕ_{0} ⟼ {coe}_{1} (Y) (x) \underset{˙}{\cdot} X)$
41	32 40	eqtr4di	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} (Y) {\underset{˙}{\cdot}}_{f} (ℕ_{0} \times \{X\}) = (x \in ℕ_{0} ⟼ if (0 \leq x, {coe}_{1} (Y) (x - 0) \underset{˙}{\cdot} X, 0_{R}))$
42	17 21 41	3eqtr4d	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} (Y \underset{˙}{∙} A (X)) = {coe}_{1} (Y) {\underset{˙}{\cdot}}_{f} (ℕ_{0} \times \{X\})$

Metamath Proof Explorer

Theorem coe1sclmul2

Proof