deg1prod

Description: Degree of a product of polynomials. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	deg1prod.1	$⊢ D = \deg_{1} (R)$
	deg1prod.2	$⊢ P = {Poly}_{1} (R)$
	deg1prod.3	$⊢ B = {Base}_{P}$
	deg1prod.4	$⊢ M = {mulGrp}_{P}$
	deg1prod.5	$⊢ \underset{˙}{0} = 0_{P}$
	deg1prod.6	$⊢ φ \to A \in Fin$
	deg1prod.7	$⊢ φ \to R \in IDomn$
	deg1prod.8	$⊢ φ \to F : A ⟶ B ∖ \{\underset{˙}{0}\}$
Assertion	deg1prod	$⊢ φ \to D (\sum_{M} F) = \sum_{k \in A} D (F (k))$

Proof

Step	Hyp	Ref	Expression
1		deg1prod.1	$⊢ D = \deg_{1} (R)$
2		deg1prod.2	$⊢ P = {Poly}_{1} (R)$
3		deg1prod.3	$⊢ B = {Base}_{P}$
4		deg1prod.4	$⊢ M = {mulGrp}_{P}$
5		deg1prod.5	$⊢ \underset{˙}{0} = 0_{P}$
6		deg1prod.6	$⊢ φ \to A \in Fin$
7		deg1prod.7	$⊢ φ \to R \in IDomn$
8		deg1prod.8	$⊢ φ \to F : A ⟶ B ∖ \{\underset{˙}{0}\}$
9	8	feqmptd	$⊢ φ \to F = (k \in A ⟼ F (k))$
10	9	oveq2d	$⊢ φ \to \sum_{M} F = \underset{k \in A}{\sum_{M}} F (k)$
11	10	fveq2d	$⊢ φ \to D (\sum_{M} F) = D (\underset{k \in A}{\sum_{M}} F (k))$
12		mpteq1	$⊢ a = \emptyset \to (k \in a ⟼ F (k)) = (k \in \emptyset ⟼ F (k))$
13	12	oveq2d	$⊢ a = \emptyset \to \underset{k \in a}{\sum_{M}} F (k) = \underset{k \in \emptyset}{\sum_{M}} F (k)$
14	13	fveq2d	$⊢ a = \emptyset \to D (\underset{k \in a}{\sum_{M}} F (k)) = D (\underset{k \in \emptyset}{\sum_{M}} F (k))$
15		sumeq1	$⊢ a = \emptyset \to \sum_{k \in a} D (F (k)) = \sum_{k \in \emptyset} D (F (k))$
16	14 15	eqeq12d	$⊢ a = \emptyset \to (D (\underset{k \in a}{\sum_{M}} F (k)) = \sum_{k \in a} D (F (k)) \leftrightarrow D (\underset{k \in \emptyset}{\sum_{M}} F (k)) = \sum_{k \in \emptyset} D (F (k)))$
17		mpteq1	$⊢ a = b \to (k \in a ⟼ F (k)) = (k \in b ⟼ F (k))$
18	17	oveq2d	$⊢ a = b \to \underset{k \in a}{\sum_{M}} F (k) = \underset{k \in b}{\sum_{M}} F (k)$
19	18	fveq2d	$⊢ a = b \to D (\underset{k \in a}{\sum_{M}} F (k)) = D (\underset{k \in b}{\sum_{M}} F (k))$
20		sumeq1	$⊢ a = b \to \sum_{k \in a} D (F (k)) = \sum_{k \in b} D (F (k))$
21	19 20	eqeq12d	$⊢ a = b \to (D (\underset{k \in a}{\sum_{M}} F (k)) = \sum_{k \in a} D (F (k)) \leftrightarrow D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k)))$
22		mpteq1	$⊢ a = b \cup \{l\} \to (k \in a ⟼ F (k)) = (k \in (b \cup \{l\}) ⟼ F (k))$
23	22	oveq2d	$⊢ a = b \cup \{l\} \to \underset{k \in a}{\sum_{M}} F (k) = \underset{k \in b \cup \{l\}}{\sum_{M}} F (k)$
24	23	fveq2d	$⊢ a = b \cup \{l\} \to D (\underset{k \in a}{\sum_{M}} F (k)) = D (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k))$
25		sumeq1	$⊢ a = b \cup \{l\} \to \sum_{k \in a} D (F (k)) = \sum_{k \in b \cup \{l\}} D (F (k))$
26	24 25	eqeq12d	$⊢ a = b \cup \{l\} \to (D (\underset{k \in a}{\sum_{M}} F (k)) = \sum_{k \in a} D (F (k)) \leftrightarrow D (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k)) = \sum_{k \in b \cup \{l\}} D (F (k)))$
27		mpteq1	$⊢ a = A \to (k \in a ⟼ F (k)) = (k \in A ⟼ F (k))$
28	27	oveq2d	$⊢ a = A \to \underset{k \in a}{\sum_{M}} F (k) = \underset{k \in A}{\sum_{M}} F (k)$
29	28	fveq2d	$⊢ a = A \to D (\underset{k \in a}{\sum_{M}} F (k)) = D (\underset{k \in A}{\sum_{M}} F (k))$
30		sumeq1	$⊢ a = A \to \sum_{k \in a} D (F (k)) = \sum_{k \in A} D (F (k))$
31	29 30	eqeq12d	$⊢ a = A \to (D (\underset{k \in a}{\sum_{M}} F (k)) = \sum_{k \in a} D (F (k)) \leftrightarrow D (\underset{k \in A}{\sum_{M}} F (k)) = \sum_{k \in A} D (F (k)))$
32		mpt0	$⊢ (k \in \emptyset ⟼ F (k)) = \emptyset$
33	32	oveq2i	$⊢ \underset{k \in \emptyset}{\sum_{M}} F (k) = \sum_{M} \emptyset$
34		eqid	$⊢ 1_{P} = 1_{P}$
35	4 34	ringidval	$⊢ 1_{P} = 0_{M}$
36	35	gsum0	$⊢ \sum_{M} \emptyset = 1_{P}$
37	33 36	eqtri	$⊢ \underset{k \in \emptyset}{\sum_{M}} F (k) = 1_{P}$
38	37	a1i	$⊢ φ \to \underset{k \in \emptyset}{\sum_{M}} F (k) = 1_{P}$
39	38	fveq2d	$⊢ φ \to D (\underset{k \in \emptyset}{\sum_{M}} F (k)) = D (1_{P})$
40	7	idomdomd	$⊢ φ \to R \in Domn$
41		domnring	$⊢ R \in Domn \to R \in Ring$
42		eqid	$⊢ algSc (P) = algSc (P)$
43		eqid	$⊢ 1_{R} = 1_{R}$
44	2 42 43 34	ply1scl1	$⊢ R \in Ring \to algSc (P) (1_{R}) = 1_{P}$
45	40 41 44	3syl	$⊢ φ \to algSc (P) (1_{R}) = 1_{P}$
46	45	fveq2d	$⊢ φ \to D (algSc (P) (1_{R})) = D (1_{P})$
47	7	idomringd	$⊢ φ \to R \in Ring$
48		eqid	$⊢ {Base}_{R} = {Base}_{R}$
49	48 43 47	ringidcld	$⊢ φ \to 1_{R} \in {Base}_{R}$
50		domnnzr	$⊢ R \in Domn \to R \in NzRing$
51		eqid	$⊢ 0_{R} = 0_{R}$
52	43 51	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
53	40 50 52	3syl	$⊢ φ \to 1_{R} \neq 0_{R}$
54	1 2 48 42 51	deg1scl	$⊢ (R \in Ring \land 1_{R} \in {Base}_{R} \land 1_{R} \neq 0_{R}) \to D (algSc (P) (1_{R})) = 0$
55	47 49 53 54	syl3anc	$⊢ φ \to D (algSc (P) (1_{R})) = 0$
56	39 46 55	3eqtr2d	$⊢ φ \to D (\underset{k \in \emptyset}{\sum_{M}} F (k)) = 0$
57		sum0	$⊢ \sum_{k \in \emptyset} D (F (k)) = 0$
58	56 57	eqtr4di	$⊢ φ \to D (\underset{k \in \emptyset}{\sum_{M}} F (k)) = \sum_{k \in \emptyset} D (F (k))$
59		eqid	$⊢ \cdot_{P} = \cdot_{P}$
60	40	ad2antrr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to R \in Domn$
61	4 3	mgpbas	$⊢ B = {Base}_{M}$
62	2	ply1idom	$⊢ R \in IDomn \to P \in IDomn$
63	7 62	syl	$⊢ φ \to P \in IDomn$
64	63	idomcringd	$⊢ φ \to P \in CRing$
65	4	crngmgp	$⊢ P \in CRing \to M \in CMnd$
66	64 65	syl	$⊢ φ \to M \in CMnd$
67	66	ad2antrr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to M \in CMnd$
68	6	ad2antrr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to A \in Fin$
69		simplr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to b \subseteq A$
70	68 69	ssfid	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to b \in Fin$
71	8	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land k \in b) \to F : A ⟶ B ∖ \{\underset{˙}{0}\}$
72	69	sselda	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land k \in b) \to k \in A$
73	71 72	ffvelcdmd	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land k \in b) \to F (k) \in (B ∖ \{\underset{˙}{0}\})$
74	73	eldifad	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land k \in b) \to F (k) \in B$
75	74	ralrimiva	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to \forall k \in b F (k) \in B$
76	61 67 70 75	gsummptcl	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to \underset{k \in b}{\sum_{M}} F (k) \in B$
77		nfv	$⊢ Ⅎ k (φ \land b \subseteq A)$
78		eqid	$⊢ (k \in b ⟼ F (k)) = (k \in b ⟼ F (k))$
79	5	fvexi	$⊢ \underset{˙}{0} \in V$
80	79	a1i	$⊢ (φ \land b \subseteq A) \to \underset{˙}{0} \in V$
81	8	ad2antrr	$⊢ ((φ \land b \subseteq A) \land k \in b) \to F : A ⟶ B ∖ \{\underset{˙}{0}\}$
82		simpr	$⊢ (φ \land b \subseteq A) \to b \subseteq A$
83	82	sselda	$⊢ ((φ \land b \subseteq A) \land k \in b) \to k \in A$
84	81 83	ffvelcdmd	$⊢ ((φ \land b \subseteq A) \land k \in b) \to F (k) \in (B ∖ \{\underset{˙}{0}\})$
85		eldifsni	$⊢ F (k) \in (B ∖ \{\underset{˙}{0}\}) \to F (k) \neq \underset{˙}{0}$
86	84 85	syl	$⊢ ((φ \land b \subseteq A) \land k \in b) \to F (k) \neq \underset{˙}{0}$
87	86	necomd	$⊢ ((φ \land b \subseteq A) \land k \in b) \to \underset{˙}{0} \neq F (k)$
88	77 78 80 87	nelrnmpt	$⊢ (φ \land b \subseteq A) \to \neg \underset{˙}{0} \in ran (k \in b ⟼ F (k))$
89	63	adantr	$⊢ (φ \land b \subseteq A) \to P \in IDomn$
90	6	adantr	$⊢ (φ \land b \subseteq A) \to A \in Fin$
91	90 82	ssfid	$⊢ (φ \land b \subseteq A) \to b \in Fin$
92	84	eldifad	$⊢ ((φ \land b \subseteq A) \land k \in b) \to F (k) \in B$
93	92	fmpttd	$⊢ (φ \land b \subseteq A) \to (k \in b ⟼ F (k)) : b ⟶ B$
94	4 3 5 89 91 93	domnprodeq0	$⊢ (φ \land b \subseteq A) \to (\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in b ⟼ F (k)))$
95	94	necon3abid	$⊢ (φ \land b \subseteq A) \to (\underset{k \in b}{\sum_{M}} F (k) \neq \underset{˙}{0} \leftrightarrow \neg \underset{˙}{0} \in ran (k \in b ⟼ F (k)))$
96	88 95	mpbird	$⊢ (φ \land b \subseteq A) \to \underset{k \in b}{\sum_{M}} F (k) \neq \underset{˙}{0}$
97	96	adantr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to \underset{k \in b}{\sum_{M}} F (k) \neq \underset{˙}{0}$
98	8	ad2antrr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to F : A ⟶ B ∖ \{\underset{˙}{0}\}$
99		simpr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to l \in (A ∖ b)$
100	99	eldifad	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to l \in A$
101	98 100	ffvelcdmd	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to F (l) \in (B ∖ \{\underset{˙}{0}\})$
102	101	eldifad	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to F (l) \in B$
103		eldifsni	$⊢ F (l) \in (B ∖ \{\underset{˙}{0}\}) \to F (l) \neq \underset{˙}{0}$
104	101 103	syl	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to F (l) \neq \underset{˙}{0}$
105	1 2 3 59 5 60 76 97 102 104	deg1mul	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to D ((\underset{k \in b}{\sum_{M}}, F (k)) \cdot_{P} F (l)) = D (\underset{k \in b}{\sum_{M}} F (k)) + D (F (l))$
106	105	adantr	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to D ((\underset{k \in b}{\sum_{M}}, F (k)) \cdot_{P} F (l)) = D (\underset{k \in b}{\sum_{M}} F (k)) + D (F (l))$
107		simpr	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))$
108	107	oveq1d	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to D (\underset{k \in b}{\sum_{M}} F (k)) + D (F (l)) = \sum_{k \in b} D (F (k)) + D (F (l))$
109	106 108	eqtr2d	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to \sum_{k \in b} D (F (k)) + D (F (l)) = D ((\underset{k \in b}{\sum_{M}}, F (k)) \cdot_{P} F (l))$
110		nfv	$⊢ Ⅎ k ((φ \land b \subseteq A) \land l \in (A ∖ b))$
111		nfcv	$⊢ \underline{Ⅎ} k D$
112		nfcv	$⊢ \underline{Ⅎ} k M$
113		nfcv	$⊢ \underline{Ⅎ} k Σ_{𝑔}$
114		nfmpt1	$⊢ \underline{Ⅎ} k (k \in b ⟼ F (k))$
115	112 113 114	nfov	$⊢ \underline{Ⅎ} k (\underset{k \in b}{\sum_{M}}, F (k))$
116	111 115	nffv	$⊢ \underline{Ⅎ} k D (\underset{k \in b}{\sum_{M}} F (k))$
117		nfcv	$⊢ \underline{Ⅎ} k b$
118	117	nfsum1	$⊢ \underline{Ⅎ} k \sum_{k \in b} D (F (k))$
119	116 118	nfeq	$⊢ Ⅎ k D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))$
120	110 119	nfan	$⊢ Ⅎ k (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k)))$
121		nfcv	$⊢ \underline{Ⅎ} k D (F (l))$
122	6	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to A \in Fin$
123		simpllr	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to b \subseteq A$
124	122 123	ssfid	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to b \in Fin$
125		simplr	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to l \in (A ∖ b)$
126	125	eldifbd	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to \neg l \in b$
127	47	ad4antr	$⊢ ((((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \land k \in b) \to R \in Ring$
128	8	ad4antr	$⊢ ((((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \land k \in b) \to F : A ⟶ B ∖ \{\underset{˙}{0}\}$
129	123	sselda	$⊢ ((((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \land k \in b) \to k \in A$
130	128 129	ffvelcdmd	$⊢ ((((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \land k \in b) \to F (k) \in (B ∖ \{\underset{˙}{0}\})$
131	130	eldifad	$⊢ ((((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \land k \in b) \to F (k) \in B$
132	130 85	syl	$⊢ ((((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \land k \in b) \to F (k) \neq \underset{˙}{0}$
133	1 2 5 3	deg1nn0cl	$⊢ (R \in Ring \land F (k) \in B \land F (k) \neq \underset{˙}{0}) \to D (F (k)) \in ℕ_{0}$
134	127 131 132 133	syl3anc	$⊢ ((((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \land k \in b) \to D (F (k)) \in ℕ_{0}$
135	134	nn0cnd	$⊢ ((((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \land k \in b) \to D (F (k)) \in ℂ$
136		2fveq3	$⊢ k = l \to D (F (k)) = D (F (l))$
137	47	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to R \in Ring$
138	8	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to F : A ⟶ B ∖ \{\underset{˙}{0}\}$
139	125	eldifad	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to l \in A$
140	138 139	ffvelcdmd	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to F (l) \in (B ∖ \{\underset{˙}{0}\})$
141	140	eldifad	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to F (l) \in B$
142	140 103	syl	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to F (l) \neq \underset{˙}{0}$
143	1 2 5 3	deg1nn0cl	$⊢ (R \in Ring \land F (l) \in B \land F (l) \neq \underset{˙}{0}) \to D (F (l)) \in ℕ_{0}$
144	137 141 142 143	syl3anc	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to D (F (l)) \in ℕ_{0}$
145	144	nn0cnd	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to D (F (l)) \in ℂ$
146	120 121 124 125 126 135 136 145	fsumsplitsn	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to \sum_{k \in b \cup \{l\}} D (F (k)) = \sum_{k \in b} D (F (k)) + D (F (l))$
147	4 59	mgpplusg	$⊢ \cdot_{P} = +_{M}$
148	99	eldifbd	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to \neg l \in b$
149		fveq2	$⊢ k = l \to F (k) = F (l)$
150	61 147 67 70 74 99 148 102 149	gsumunsn	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to \underset{k \in b \cup \{l\}}{\sum_{M}} F (k) = (\underset{k \in b}{\sum_{M}}, F (k)) \cdot_{P} F (l)$
151	150	fveq2d	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to D (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k)) = D ((\underset{k \in b}{\sum_{M}}, F (k)) \cdot_{P} F (l))$
152	151	adantr	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to D (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k)) = D ((\underset{k \in b}{\sum_{M}}, F (k)) \cdot_{P} F (l))$
153	109 146 152	3eqtr4rd	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k))) \to D (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k)) = \sum_{k \in b \cup \{l\}} D (F (k))$
154	153	ex	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to (D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k)) \to D (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k)) = \sum_{k \in b \cup \{l\}} D (F (k)))$
155	154	anasss	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to (D (\underset{k \in b}{\sum_{M}} F (k)) = \sum_{k \in b} D (F (k)) \to D (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k)) = \sum_{k \in b \cup \{l\}} D (F (k)))$
156	16 21 26 31 58 155 6	findcard2d	$⊢ φ \to D (\underset{k \in A}{\sum_{M}} F (k)) = \sum_{k \in A} D (F (k))$
157	11 156	eqtrd	$⊢ φ \to D (\sum_{M} F) = \sum_{k \in A} D (F (k))$

Metamath Proof Explorer

Theorem deg1prod

Proof