coe1addfv

Description: A particular coefficient of an addition. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	coe1add.y	$⊢ Y = {Poly}_{1} (R)$
	coe1add.b	$⊢ B = {Base}_{Y}$
	coe1add.p	$⊢ \underset{˙}{✚} = +_{Y}$
	coe1add.q	$⊢ \underset{˙}{+} = +_{R}$
Assertion	coe1addfv	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} (F \underset{˙}{✚} G) (X) = {coe}_{1} (F) (X) \underset{˙}{+} {coe}_{1} (G) (X)$

Proof

Step	Hyp	Ref	Expression
1		coe1add.y	$⊢ Y = {Poly}_{1} (R)$
2		coe1add.b	$⊢ B = {Base}_{Y}$
3		coe1add.p	$⊢ \underset{˙}{✚} = +_{Y}$
4		coe1add.q	$⊢ \underset{˙}{+} = +_{R}$
5	1 2 3 4	coe1add	$⊢ (R \in Ring \land F \in B \land G \in B) \to {coe}_{1} (F \underset{˙}{✚} G) = {coe}_{1} (F) {\underset{˙}{+}}_{f} {coe}_{1} (G)$
6	5	adantr	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} (F \underset{˙}{✚} G) = {coe}_{1} (F) {\underset{˙}{+}}_{f} {coe}_{1} (G)$
7	6	fveq1d	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} (F \underset{˙}{✚} G) (X) = ({coe}_{1} (F) {\underset{˙}{+}}_{f} {coe}_{1} (G)) (X)$
8		eqid	$⊢ {coe}_{1} (F) = {coe}_{1} (F)$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10	8 2 1 9	coe1f	$⊢ F \in B \to {coe}_{1} (F) : ℕ_{0} ⟶ {Base}_{R}$
11	10	ffnd	$⊢ F \in B \to {coe}_{1} (F) Fn ℕ_{0}$
12	11	3ad2ant2	$⊢ (R \in Ring \land F \in B \land G \in B) \to {coe}_{1} (F) Fn ℕ_{0}$
13	12	adantr	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} (F) Fn ℕ_{0}$
14		eqid	$⊢ {coe}_{1} (G) = {coe}_{1} (G)$
15	14 2 1 9	coe1f	$⊢ G \in B \to {coe}_{1} (G) : ℕ_{0} ⟶ {Base}_{R}$
16	15	ffnd	$⊢ G \in B \to {coe}_{1} (G) Fn ℕ_{0}$
17	16	3ad2ant3	$⊢ (R \in Ring \land F \in B \land G \in B) \to {coe}_{1} (G) Fn ℕ_{0}$
18	17	adantr	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} (G) Fn ℕ_{0}$
19		nn0ex	$⊢ ℕ_{0} \in V$
20	19	a1i	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to ℕ_{0} \in V$
21		simpr	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to X \in ℕ_{0}$
22		fnfvof	$⊢ (({coe}_{1} (F) Fn ℕ_{0} \land {coe}_{1} (G) Fn ℕ_{0}) \land (ℕ_{0} \in V \land X \in ℕ_{0})) \to ({coe}_{1} (F) {\underset{˙}{+}}_{f} {coe}_{1} (G)) (X) = {coe}_{1} (F) (X) \underset{˙}{+} {coe}_{1} (G) (X)$
23	13 18 20 21 22	syl22anc	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to ({coe}_{1} (F) {\underset{˙}{+}}_{f} {coe}_{1} (G)) (X) = {coe}_{1} (F) (X) \underset{˙}{+} {coe}_{1} (G) (X)$
24	7 23	eqtrd	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} (F \underset{˙}{✚} G) (X) = {coe}_{1} (F) (X) \underset{˙}{+} {coe}_{1} (G) (X)$

Metamath Proof Explorer

Theorem coe1addfv

Proof