Metamath Proof Explorer

Theorem deg1prod

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

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

Proof

Step Hyp Ref Expression
1 deg1prod.1 ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2 deg1prod.2 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 deg1prod.3 ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 deg1prod.4 ⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
5 deg1prod.5 ⊢ 0 = ( 0g ‘ 𝑃 )
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 ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
35 4 34 ringidval ⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝑀 )
36 35 gsum0 ⊢ ( 𝑀 Σg ∅ ) = ( 1r ‘ 𝑃 )
37 33 36 eqtri ⊢ ( 𝑀 Σg ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 1r ‘ 𝑃 )
38 37 a1i ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 1r ‘ 𝑃 ) )
39 38 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 Σg ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐷 ‘ ( 1r ‘ 𝑃 ) ) )
40 7 idomdomd ⊢ ( 𝜑 → 𝑅 ∈ Domn )
41 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
42 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
43 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
44 2 42 43 34 ply1scl1 ⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
45 40 41 44 3syl ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
46 45 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝐷 ‘ ( 1r ‘ 𝑃 ) ) )
47 7 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
48 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
49 48 43 47 ringidcld ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
50 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
51 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
52 43 51 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
53 40 50 52 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
54 1 2 48 42 51 deg1scl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐷 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = 0 )
55 47 49 53 54 syl3anc ⊢ ( 𝜑 → ( 𝐷 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = 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 ) → ( 𝐷 ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℕ0 )
134 127 131 132 133 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝐷 ‘ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) = Σ 𝑘 ∈ 𝑏 ( 𝐷 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑏 ) → ( 𝐷 ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℕ0 )
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 ) → ( 𝐷 ‘ ( 𝐹 ‘ 𝑙 ) ) ∈ ℕ0 )
144 137 141 142 143 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝐷 ‘ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) = Σ 𝑘 ∈ 𝑏 ( 𝐷 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝐷 ‘ ( 𝐹 ‘ 𝑙 ) ) ∈ ℕ0 )
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 𝐹 ) ) = Σ 𝑘 ∈ 𝐴 ( 𝐷 ‘ ( 𝐹 ‘ 𝑘 ) ) )