cply1mul

Description: The product of two constant polynomials is a constant polynomial. (Contributed by AV, 18-Nov-2019)

	Ref	Expression
Hypotheses	cply1mul.p	$⊢ P = {Poly}_{1} (R)$
	cply1mul.b	$⊢ B = {Base}_{P}$
	cply1mul.0	$⊢ \underset{˙}{0} = 0_{R}$
	cply1mul.m	$⊢ \underset{˙}{\times} = \cdot_{P}$
Assertion	cply1mul	$⊢ (R \in Ring \land (F \in B \land G \in B)) \to (\forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0}) \to \forall c \in ℕ {coe}_{1} (F \underset{˙}{\times} G) (c) = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		cply1mul.p	$⊢ P = {Poly}_{1} (R)$
2		cply1mul.b	$⊢ B = {Base}_{P}$
3		cply1mul.0	$⊢ \underset{˙}{0} = 0_{R}$
4		cply1mul.m	$⊢ \underset{˙}{\times} = \cdot_{P}$
5		eqid	$⊢ \cdot_{R} = \cdot_{R}$
6	1 4 5 2	coe1mul	$⊢ (R \in Ring \land F \in B \land G \in B) \to {coe}_{1} (F \underset{˙}{\times} G) = (s \in ℕ_{0} ⟼ {\sum_{R}}_{k = 0}^{s} ({coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (s - k)))$
7	6	3expb	$⊢ (R \in Ring \land (F \in B \land G \in B)) \to {coe}_{1} (F \underset{˙}{\times} G) = (s \in ℕ_{0} ⟼ {\sum_{R}}_{k = 0}^{s} ({coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (s - k)))$
8	7	adantr	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \to {coe}_{1} (F \underset{˙}{\times} G) = (s \in ℕ_{0} ⟼ {\sum_{R}}_{k = 0}^{s} ({coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (s - k)))$
9	8	adantr	$⊢ (((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \land n \in ℕ) \to {coe}_{1} (F \underset{˙}{\times} G) = (s \in ℕ_{0} ⟼ {\sum_{R}}_{k = 0}^{s} ({coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (s - k)))$
10		oveq2	$⊢ s = n \to (0 \dots s) = (0 \dots n)$
11		fvoveq1	$⊢ s = n \to {coe}_{1} (G) (s - k) = {coe}_{1} (G) (n - k)$
12	11	oveq2d	$⊢ s = n \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (s - k) = {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k)$
13	10 12	mpteq12dv	$⊢ s = n \to (k \in (0 \dots s) ⟼ {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (s - k)) = (k \in (0 \dots n) ⟼ {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k))$
14	13	oveq2d	$⊢ s = n \to {\sum_{R}}_{k = 0}^{s} ({coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (s - k)) = {\sum_{R}}_{k = 0}^{n} ({coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k))$
15	14	adantl	$⊢ ((((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \land n \in ℕ) \land s = n) \to {\sum_{R}}_{k = 0}^{s} ({coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (s - k)) = {\sum_{R}}_{k = 0}^{n} ({coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k))$
16		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
17	16	adantl	$⊢ (((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \land n \in ℕ) \to n \in ℕ_{0}$
18		ovexd	$⊢ (((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \land n \in ℕ) \to {\sum_{R}}_{k = 0}^{n} ({coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k)) \in V$
19	9 15 17 18	fvmptd	$⊢ (((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \land n \in ℕ) \to {coe}_{1} (F \underset{˙}{\times} G) (n) = {\sum_{R}}_{k = 0}^{n} ({coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k))$
20		r19.26	$⊢ \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0}) \leftrightarrow (\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \land \forall c \in ℕ {coe}_{1} (G) (c) = \underset{˙}{0})$
21		oveq2	$⊢ k = 0 \to n - k = n - 0$
22		nncn	$⊢ n \in ℕ \to n \in ℂ$
23	22	subid1d	$⊢ n \in ℕ \to n - 0 = n$
24	23	adantr	$⊢ (n \in ℕ \land k \in (0 \dots n)) \to n - 0 = n$
25	21 24	sylan9eqr	$⊢ ((n \in ℕ \land k \in (0 \dots n)) \land k = 0) \to n - k = n$
26		simpll	$⊢ ((n \in ℕ \land k \in (0 \dots n)) \land k = 0) \to n \in ℕ$
27	25 26	eqeltrd	$⊢ ((n \in ℕ \land k \in (0 \dots n)) \land k = 0) \to n - k \in ℕ$
28		fveqeq2	$⊢ c = n - k \to ({coe}_{1} (G) (c) = \underset{˙}{0} \leftrightarrow {coe}_{1} (G) (n - k) = \underset{˙}{0})$
29	28	rspcv	$⊢ n - k \in ℕ \to (\forall c \in ℕ {coe}_{1} (G) (c) = \underset{˙}{0} \to {coe}_{1} (G) (n - k) = \underset{˙}{0})$
30	27 29	syl	$⊢ ((n \in ℕ \land k \in (0 \dots n)) \land k = 0) \to (\forall c \in ℕ {coe}_{1} (G) (c) = \underset{˙}{0} \to {coe}_{1} (G) (n - k) = \underset{˙}{0})$
31		oveq2	$⊢ {coe}_{1} (G) (n - k) = \underset{˙}{0} \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = {coe}_{1} (F) (k) \cdot_{R} \underset{˙}{0}$
32		simpll	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land ((n \in ℕ \land k \in (0 \dots n)) \land k = 0)) \to R \in Ring$
33		simprl	$⊢ (R \in Ring \land (F \in B \land G \in B)) \to F \in B$
34		elfznn0	$⊢ k \in (0 \dots n) \to k \in ℕ_{0}$
35	34	adantl	$⊢ (n \in ℕ \land k \in (0 \dots n)) \to k \in ℕ_{0}$
36	35	adantr	$⊢ ((n \in ℕ \land k \in (0 \dots n)) \land k = 0) \to k \in ℕ_{0}$
37		eqid	$⊢ {coe}_{1} (F) = {coe}_{1} (F)$
38		eqid	$⊢ {Base}_{R} = {Base}_{R}$
39	37 2 1 38	coe1fvalcl	$⊢ (F \in B \land k \in ℕ_{0}) \to {coe}_{1} (F) (k) \in {Base}_{R}$
40	33 36 39	syl2an	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land ((n \in ℕ \land k \in (0 \dots n)) \land k = 0)) \to {coe}_{1} (F) (k) \in {Base}_{R}$
41	38 5 3	ringrz	$⊢ (R \in Ring \land {coe}_{1} (F) (k) \in {Base}_{R}) \to {coe}_{1} (F) (k) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
42	32 40 41	syl2anc	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land ((n \in ℕ \land k \in (0 \dots n)) \land k = 0)) \to {coe}_{1} (F) (k) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
43	31 42	sylan9eqr	$⊢ (((R \in Ring \land (F \in B \land G \in B)) \land ((n \in ℕ \land k \in (0 \dots n)) \land k = 0)) \land {coe}_{1} (G) (n - k) = \underset{˙}{0}) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}$
44	43	ex	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land ((n \in ℕ \land k \in (0 \dots n)) \land k = 0)) \to ({coe}_{1} (G) (n - k) = \underset{˙}{0} \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})$
45	44	expcom	$⊢ ((n \in ℕ \land k \in (0 \dots n)) \land k = 0) \to ((R \in Ring \land (F \in B \land G \in B)) \to ({coe}_{1} (G) (n - k) = \underset{˙}{0} \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}))$
46	45	com23	$⊢ ((n \in ℕ \land k \in (0 \dots n)) \land k = 0) \to ({coe}_{1} (G) (n - k) = \underset{˙}{0} \to ((R \in Ring \land (F \in B \land G \in B)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}))$
47	30 46	syldc	$⊢ \forall c \in ℕ {coe}_{1} (G) (c) = \underset{˙}{0} \to (((n \in ℕ \land k \in (0 \dots n)) \land k = 0) \to ((R \in Ring \land (F \in B \land G \in B)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}))$
48	47	expd	$⊢ \forall c \in ℕ {coe}_{1} (G) (c) = \underset{˙}{0} \to ((n \in ℕ \land k \in (0 \dots n)) \to (k = 0 \to ((R \in Ring \land (F \in B \land G \in B)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
49	48	com24	$⊢ \forall c \in ℕ {coe}_{1} (G) (c) = \underset{˙}{0} \to ((R \in Ring \land (F \in B \land G \in B)) \to (k = 0 \to ((n \in ℕ \land k \in (0 \dots n)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
50	49	adantl	$⊢ (\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \land \forall c \in ℕ {coe}_{1} (G) (c) = \underset{˙}{0}) \to ((R \in Ring \land (F \in B \land G \in B)) \to (k = 0 \to ((n \in ℕ \land k \in (0 \dots n)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
51	50	com13	$⊢ k = 0 \to ((R \in Ring \land (F \in B \land G \in B)) \to ((\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \land \forall c \in ℕ {coe}_{1} (G) (c) = \underset{˙}{0}) \to ((n \in ℕ \land k \in (0 \dots n)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
52		neqne	$⊢ \neg k = 0 \to k \neq 0$
53	52 34	anim12ci	$⊢ (\neg k = 0 \land k \in (0 \dots n)) \to (k \in ℕ_{0} \land k \neq 0)$
54		elnnne0	$⊢ k \in ℕ \leftrightarrow (k \in ℕ_{0} \land k \neq 0)$
55	53 54	sylibr	$⊢ (\neg k = 0 \land k \in (0 \dots n)) \to k \in ℕ$
56		fveqeq2	$⊢ c = k \to ({coe}_{1} (F) (c) = \underset{˙}{0} \leftrightarrow {coe}_{1} (F) (k) = \underset{˙}{0})$
57	56	rspcv	$⊢ k \in ℕ \to (\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \to {coe}_{1} (F) (k) = \underset{˙}{0})$
58	55 57	syl	$⊢ (\neg k = 0 \land k \in (0 \dots n)) \to (\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \to {coe}_{1} (F) (k) = \underset{˙}{0})$
59		oveq1	$⊢ {coe}_{1} (F) (k) = \underset{˙}{0} \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0} \cdot_{R} {coe}_{1} (G) (n - k)$
60		simpll	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land k \in (0 \dots n)) \to R \in Ring$
61	2	eleq2i	$⊢ G \in B \leftrightarrow G \in {Base}_{P}$
62	61	biimpi	$⊢ G \in B \to G \in {Base}_{P}$
63	62	adantl	$⊢ (F \in B \land G \in B) \to G \in {Base}_{P}$
64	63	adantl	$⊢ (R \in Ring \land (F \in B \land G \in B)) \to G \in {Base}_{P}$
65		fznn0sub	$⊢ k \in (0 \dots n) \to n - k \in ℕ_{0}$
66		eqid	$⊢ {coe}_{1} (G) = {coe}_{1} (G)$
67		eqid	$⊢ {Base}_{P} = {Base}_{P}$
68	66 67 1 38	coe1fvalcl	$⊢ (G \in {Base}_{P} \land n - k \in ℕ_{0}) \to {coe}_{1} (G) (n - k) \in {Base}_{R}$
69	64 65 68	syl2an	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land k \in (0 \dots n)) \to {coe}_{1} (G) (n - k) \in {Base}_{R}$
70	38 5 3	ringlz	$⊢ (R \in Ring \land {coe}_{1} (G) (n - k) \in {Base}_{R}) \to \underset{˙}{0} \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}$
71	60 69 70	syl2anc	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land k \in (0 \dots n)) \to \underset{˙}{0} \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}$
72	59 71	sylan9eqr	$⊢ (((R \in Ring \land (F \in B \land G \in B)) \land k \in (0 \dots n)) \land {coe}_{1} (F) (k) = \underset{˙}{0}) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}$
73	72	ex	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land k \in (0 \dots n)) \to ({coe}_{1} (F) (k) = \underset{˙}{0} \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})$
74	73	ex	$⊢ (R \in Ring \land (F \in B \land G \in B)) \to (k \in (0 \dots n) \to ({coe}_{1} (F) (k) = \underset{˙}{0} \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}))$
75	74	com23	$⊢ (R \in Ring \land (F \in B \land G \in B)) \to ({coe}_{1} (F) (k) = \underset{˙}{0} \to (k \in (0 \dots n) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}))$
76	75	a1dd	$⊢ (R \in Ring \land (F \in B \land G \in B)) \to ({coe}_{1} (F) (k) = \underset{˙}{0} \to (n \in ℕ \to (k \in (0 \dots n) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
77	76	com14	$⊢ k \in (0 \dots n) \to ({coe}_{1} (F) (k) = \underset{˙}{0} \to (n \in ℕ \to ((R \in Ring \land (F \in B \land G \in B)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
78	77	adantl	$⊢ (\neg k = 0 \land k \in (0 \dots n)) \to ({coe}_{1} (F) (k) = \underset{˙}{0} \to (n \in ℕ \to ((R \in Ring \land (F \in B \land G \in B)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
79	58 78	syld	$⊢ (\neg k = 0 \land k \in (0 \dots n)) \to (\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \to (n \in ℕ \to ((R \in Ring \land (F \in B \land G \in B)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
80	79	com24	$⊢ (\neg k = 0 \land k \in (0 \dots n)) \to ((R \in Ring \land (F \in B \land G \in B)) \to (n \in ℕ \to (\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
81	80	ex	$⊢ \neg k = 0 \to (k \in (0 \dots n) \to ((R \in Ring \land (F \in B \land G \in B)) \to (n \in ℕ \to (\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}))))$
82	81	com14	$⊢ n \in ℕ \to (k \in (0 \dots n) \to ((R \in Ring \land (F \in B \land G \in B)) \to (\neg k = 0 \to (\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}))))$
83	82	imp	$⊢ (n \in ℕ \land k \in (0 \dots n)) \to ((R \in Ring \land (F \in B \land G \in B)) \to (\neg k = 0 \to (\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
84	83	com14	$⊢ \forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \to ((R \in Ring \land (F \in B \land G \in B)) \to (\neg k = 0 \to ((n \in ℕ \land k \in (0 \dots n)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
85	84	adantr	$⊢ (\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \land \forall c \in ℕ {coe}_{1} (G) (c) = \underset{˙}{0}) \to ((R \in Ring \land (F \in B \land G \in B)) \to (\neg k = 0 \to ((n \in ℕ \land k \in (0 \dots n)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
86	85	com13	$⊢ \neg k = 0 \to ((R \in Ring \land (F \in B \land G \in B)) \to ((\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \land \forall c \in ℕ {coe}_{1} (G) (c) = \underset{˙}{0}) \to ((n \in ℕ \land k \in (0 \dots n)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})))$
87	51 86	pm2.61i	$⊢ (R \in Ring \land (F \in B \land G \in B)) \to ((\forall c \in ℕ {coe}_{1} (F) (c) = \underset{˙}{0} \land \forall c \in ℕ {coe}_{1} (G) (c) = \underset{˙}{0}) \to ((n \in ℕ \land k \in (0 \dots n)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}))$
88	20 87	syl5bi	$⊢ (R \in Ring \land (F \in B \land G \in B)) \to (\forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0}) \to ((n \in ℕ \land k \in (0 \dots n)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}))$
89	88	imp	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \to ((n \in ℕ \land k \in (0 \dots n)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0})$
90	89	impl	$⊢ ((((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \land n \in ℕ) \land k \in (0 \dots n)) \to {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k) = \underset{˙}{0}$
91	90	mpteq2dva	$⊢ (((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \land n \in ℕ) \to (k \in (0 \dots n) ⟼ {coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k)) = (k \in (0 \dots n) ⟼ \underset{˙}{0})$
92	91	oveq2d	$⊢ (((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \land n \in ℕ) \to {\sum_{R}}_{k = 0}^{n} ({coe}_{1} (F) (k) \cdot_{R} {coe}_{1} (G) (n - k)) = {\sum_{R}}_{k = 0}^{n} \underset{˙}{0}$
93		ringmnd	$⊢ R \in Ring \to R \in Mnd$
94		ovexd	$⊢ R \in Ring \to (0 \dots n) \in V$
95	3	gsumz	$⊢ (R \in Mnd \land (0 \dots n) \in V) \to {\sum_{R}}_{k = 0}^{n} \underset{˙}{0} = \underset{˙}{0}$
96	93 94 95	syl2anc	$⊢ R \in Ring \to {\sum_{R}}_{k = 0}^{n} \underset{˙}{0} = \underset{˙}{0}$
97	96	adantr	$⊢ (R \in Ring \land (F \in B \land G \in B)) \to {\sum_{R}}_{k = 0}^{n} \underset{˙}{0} = \underset{˙}{0}$
98	97	adantr	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \to {\sum_{R}}_{k = 0}^{n} \underset{˙}{0} = \underset{˙}{0}$
99	98	adantr	$⊢ (((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \land n \in ℕ) \to {\sum_{R}}_{k = 0}^{n} \underset{˙}{0} = \underset{˙}{0}$
100	19 92 99	3eqtrd	$⊢ (((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \land n \in ℕ) \to {coe}_{1} (F \underset{˙}{\times} G) (n) = \underset{˙}{0}$
101	100	ralrimiva	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \to \forall n \in ℕ {coe}_{1} (F \underset{˙}{\times} G) (n) = \underset{˙}{0}$
102		fveqeq2	$⊢ c = n \to ({coe}_{1} (F \underset{˙}{\times} G) (c) = \underset{˙}{0} \leftrightarrow {coe}_{1} (F \underset{˙}{\times} G) (n) = \underset{˙}{0})$
103	102	cbvralvw	$⊢ \forall c \in ℕ {coe}_{1} (F \underset{˙}{\times} G) (c) = \underset{˙}{0} \leftrightarrow \forall n \in ℕ {coe}_{1} (F \underset{˙}{\times} G) (n) = \underset{˙}{0}$
104	101 103	sylibr	$⊢ ((R \in Ring \land (F \in B \land G \in B)) \land \forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0})) \to \forall c \in ℕ {coe}_{1} (F \underset{˙}{\times} G) (c) = \underset{˙}{0}$
105	104	ex	$⊢ (R \in Ring \land (F \in B \land G \in B)) \to (\forall c \in ℕ ({coe}_{1} (F) (c) = \underset{˙}{0} \land {coe}_{1} (G) (c) = \underset{˙}{0}) \to \forall c \in ℕ {coe}_{1} (F \underset{˙}{\times} G) (c) = \underset{˙}{0})$

Metamath Proof Explorer

Theorem cply1mul

Proof