coe1scl

Description: Coefficient vector of a scalar. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	ply1scl.p	$⊢ P = {Poly}_{1} (R)$
	ply1scl.a	$⊢ A = algSc (P)$
	coe1scl.k	$⊢ K = {Base}_{R}$
	coe1scl.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	coe1scl	$⊢ (R \in Ring \land X \in K) \to {coe}_{1} (A (X)) = (x \in ℕ_{0} ⟼ if (x = 0, X, \underset{˙}{0}))$

Step	Hyp	Ref	Expression
1		ply1scl.p	$⊢ P = {Poly}_{1} (R)$
2		ply1scl.a	$⊢ A = algSc (P)$
3		coe1scl.k	$⊢ K = {Base}_{R}$
4		coe1scl.z	$⊢ \underset{˙}{0} = 0_{R}$
5		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
6		eqid	$⊢ \cdot_{P} = \cdot_{P}$
7		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
8		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
9	3 1 5 6 7 8 2	ply1scltm	$⊢ (R \in Ring \land X \in K) \to A (X) = X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
10	9	fveq2d	$⊢ (R \in Ring \land X \in K) \to {coe}_{1} (A (X)) = {coe}_{1} (X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R)))$
11		0nn0	$⊢ 0 \in ℕ_{0}$
12	4 3 1 5 6 7 8	coe1tm	$⊢ (R \in Ring \land X \in K \land 0 \in ℕ_{0}) \to {coe}_{1} (X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = (x \in ℕ_{0} ⟼ if (x = 0, X, \underset{˙}{0}))$
13	11 12	mp3an3	$⊢ (R \in Ring \land X \in K) \to {coe}_{1} (X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) = (x \in ℕ_{0} ⟼ if (x = 0, X, \underset{˙}{0}))$
14	10 13	eqtrd	$⊢ (R \in Ring \land X \in K) \to {coe}_{1} (A (X)) = (x \in ℕ_{0} ⟼ if (x = 0, X, \underset{˙}{0}))$

Metamath Proof Explorer