deg1prod

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

	Ref	Expression
Hypotheses	deg1prod.1	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
	deg1prod.2	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	deg1prod.3	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1prod.4	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
	deg1prod.5	⊢ 0 = ( 0_g ‘ 𝑃 )
	deg1prod.6	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	deg1prod.7	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
	deg1prod.8	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 𝐵 ∖ { 0 } ) )
Assertion	deg1prod	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 Σ_g 𝐹 ) ) = Σ 𝑘 ∈ 𝐴 ( 𝐷 ‘ ( 𝐹 ‘ 𝑘 ) ) )

Proof

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

Metamath Proof Explorer

Theorem deg1prod

Proof