coe1subfv

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

	Ref	Expression
Hypotheses	coe1sub.y	$⊢ Y = {Poly}_{1} (R)$
	coe1sub.b	$⊢ B = {Base}_{Y}$
	coe1sub.p	$⊢ \underset{˙}{-} = -_{Y}$
	coe1sub.q	$⊢ N = -_{R}$
Assertion	coe1subfv	$⊢ ((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) N {coe}_{1} (G) (X)$

Proof

Step	Hyp	Ref	Expression
1		coe1sub.y	$⊢ Y = {Poly}_{1} (R)$
2		coe1sub.b	$⊢ B = {Base}_{Y}$
3		coe1sub.p	$⊢ \underset{˙}{-} = -_{Y}$
4		coe1sub.q	$⊢ N = -_{R}$
5		simpl1	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to R \in Ring$
6	1	ply1ring	$⊢ R \in Ring \to Y \in Ring$
7		ringgrp	$⊢ Y \in Ring \to Y \in Grp$
8	6 7	syl	$⊢ R \in Ring \to Y \in Grp$
9	2 3	grpsubcl	$⊢ (Y \in Grp \land F \in B \land G \in B) \to F \underset{˙}{-} G \in B$
10	8 9	syl3an1	$⊢ (R \in Ring \land F \in B \land G \in B) \to F \underset{˙}{-} G \in B$
11	10	adantr	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to F \underset{˙}{-} G \in B$
12		simpl3	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to G \in B$
13		simpr	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to X \in ℕ_{0}$
14		eqid	$⊢ +_{Y} = +_{Y}$
15		eqid	$⊢ +_{R} = +_{R}$
16	1 2 14 15	coe1addfv	$⊢ ((R \in Ring \land F \underset{˙}{-} G \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} ((F \underset{˙}{-} G) +_{Y} G) (X) = {coe}_{1} (F \underset{˙}{-} G) (X) +_{R} {coe}_{1} (G) (X)$
17	5 11 12 13 16	syl31anc	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} ((F \underset{˙}{-} G) +_{Y} G) (X) = {coe}_{1} (F \underset{˙}{-} G) (X) +_{R} {coe}_{1} (G) (X)$
18	8	3ad2ant1	$⊢ (R \in Ring \land F \in B \land G \in B) \to Y \in Grp$
19	18	adantr	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to Y \in Grp$
20		simpl2	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to F \in B$
21	2 14 3	grpnpcan	$⊢ (Y \in Grp \land F \in B \land G \in B) \to (F \underset{˙}{-} G) +_{Y} G = F$
22	19 20 12 21	syl3anc	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to (F \underset{˙}{-} G) +_{Y} G = F$
23	22	fveq2d	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} ((F \underset{˙}{-} G) +_{Y} G) = {coe}_{1} (F)$
24	23	fveq1d	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} ((F \underset{˙}{-} G) +_{Y} G) (X) = {coe}_{1} (F) (X)$
25	17 24	eqtr3d	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} (F \underset{˙}{-} G) (X) +_{R} {coe}_{1} (G) (X) = {coe}_{1} (F) (X)$
26		ringgrp	$⊢ R \in Ring \to R \in Grp$
27	26	3ad2ant1	$⊢ (R \in Ring \land F \in B \land G \in B) \to R \in Grp$
28	27	adantr	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to R \in Grp$
29		eqid	$⊢ {coe}_{1} (F) = {coe}_{1} (F)$
30		eqid	$⊢ {Base}_{R} = {Base}_{R}$
31	29 2 1 30	coe1f	$⊢ F \in B \to {coe}_{1} (F) : ℕ_{0} ⟶ {Base}_{R}$
32	31	3ad2ant2	$⊢ (R \in Ring \land F \in B \land G \in B) \to {coe}_{1} (F) : ℕ_{0} ⟶ {Base}_{R}$
33	32	ffvelcdmda	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} (F) (X) \in {Base}_{R}$
34		eqid	$⊢ {coe}_{1} (G) = {coe}_{1} (G)$
35	34 2 1 30	coe1f	$⊢ G \in B \to {coe}_{1} (G) : ℕ_{0} ⟶ {Base}_{R}$
36	35	3ad2ant3	$⊢ (R \in Ring \land F \in B \land G \in B) \to {coe}_{1} (G) : ℕ_{0} ⟶ {Base}_{R}$
37	36	ffvelcdmda	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} (G) (X) \in {Base}_{R}$
38		eqid	$⊢ {coe}_{1} (F \underset{˙}{-} G) = {coe}_{1} (F \underset{˙}{-} G)$
39	38 2 1 30	coe1f	$⊢ F \underset{˙}{-} G \in B \to {coe}_{1} (F \underset{˙}{-} G) : ℕ_{0} ⟶ {Base}_{R}$
40	10 39	syl	$⊢ (R \in Ring \land F \in B \land G \in B) \to {coe}_{1} (F \underset{˙}{-} G) : ℕ_{0} ⟶ {Base}_{R}$
41	40	ffvelcdmda	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} (F \underset{˙}{-} G) (X) \in {Base}_{R}$
42	30 15 4	grpsubadd	$⊢ (R \in Grp \land ({coe}_{1} (F) (X) \in {Base}_{R} \land {coe}_{1} (G) (X) \in {Base}_{R} \land {coe}_{1} (F \underset{˙}{-} G) (X) \in {Base}_{R})) \to ({coe}_{1} (F) (X) N {coe}_{1} (G) (X) = {coe}_{1} (F \underset{˙}{-} G) (X) \leftrightarrow {coe}_{1} (F \underset{˙}{-} G) (X) +_{R} {coe}_{1} (G) (X) = {coe}_{1} (F) (X))$
43	28 33 37 41 42	syl13anc	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to ({coe}_{1} (F) (X) N {coe}_{1} (G) (X) = {coe}_{1} (F \underset{˙}{-} G) (X) \leftrightarrow {coe}_{1} (F \underset{˙}{-} G) (X) +_{R} {coe}_{1} (G) (X) = {coe}_{1} (F) (X))$
44	25 43	mpbird	$⊢ ((R \in Ring \land F \in B \land G \in B) \land X \in ℕ_{0}) \to {coe}_{1} (F) (X) N {coe}_{1} (G) (X) = {coe}_{1} (F \underset{˙}{-} G) (X)$
45	44	eqcomd	$⊢ ((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) N {coe}_{1} (G) (X)$

Metamath Proof Explorer

Theorem coe1subfv

Proof