MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mplcoe5 Structured version   Visualization version   GIF version

Theorem mplcoe5 19408
Description: Decompose a monomial into a finite product of powers of variables. Instead of assuming that 𝑅 is a commutative ring (as in mplcoe2 19409), it is sufficient that 𝑅 is a ring and all the variables of the multivariate polynomial commute. (Contributed by AV, 7-Oct-2019.)
Hypotheses
Ref Expression
mplcoe1.p 𝑃 = (𝐼 mPoly 𝑅)
mplcoe1.d 𝐷 = {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
mplcoe1.z 0 = (0g𝑅)
mplcoe1.o 1 = (1r𝑅)
mplcoe1.i (𝜑𝐼𝑊)
mplcoe2.g 𝐺 = (mulGrp‘𝑃)
mplcoe2.m = (.g𝐺)
mplcoe2.v 𝑉 = (𝐼 mVar 𝑅)
mplcoe5.r (𝜑𝑅 ∈ Ring)
mplcoe5.y (𝜑𝑌𝐷)
mplcoe5.c (𝜑 → ∀𝑥𝐼𝑦𝐼 ((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑥)(+g𝐺)(𝑉𝑦)))
Assertion
Ref Expression
mplcoe5 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) = (𝐺 Σg (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
Distinct variable groups:   𝑥,𝑘, ,𝑦   1 ,𝑘   𝑥,𝑦, 1   𝑘,𝐺,𝑥   𝑓,𝑘,𝑥,𝑦,𝐼   𝜑,𝑘,𝑥,𝑦   𝑅,𝑓,𝑦   𝐷,𝑘,𝑥,𝑦   𝑃,𝑘,𝑥   𝑘,𝑉,𝑥   0 ,𝑓,𝑘,𝑥,𝑦   𝑓,𝑌,𝑘,𝑥,𝑦   𝑘,𝑊,𝑦   𝑦,𝐺   𝑦,𝑉   𝑦,
Allowed substitution hints:   𝜑(𝑓)   𝐷(𝑓)   𝑃(𝑦,𝑓)   𝑅(𝑥,𝑘)   1 (𝑓)   (𝑓)   𝐺(𝑓)   𝑉(𝑓)   𝑊(𝑥,𝑓)

Proof of Theorem mplcoe5
Dummy variables 𝑖 𝑤 𝑧 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplcoe5.y . . . . . . . . 9 (𝜑𝑌𝐷)
2 mplcoe1.i . . . . . . . . . 10 (𝜑𝐼𝑊)
3 mplcoe1.d . . . . . . . . . . 11 𝐷 = {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
43psrbag 19304 . . . . . . . . . 10 (𝐼𝑊 → (𝑌𝐷 ↔ (𝑌:𝐼⟶ℕ0 ∧ (𝑌 “ ℕ) ∈ Fin)))
52, 4syl 17 . . . . . . . . 9 (𝜑 → (𝑌𝐷 ↔ (𝑌:𝐼⟶ℕ0 ∧ (𝑌 “ ℕ) ∈ Fin)))
61, 5mpbid 222 . . . . . . . 8 (𝜑 → (𝑌:𝐼⟶ℕ0 ∧ (𝑌 “ ℕ) ∈ Fin))
76simpld 475 . . . . . . 7 (𝜑𝑌:𝐼⟶ℕ0)
87feqmptd 6216 . . . . . 6 (𝜑𝑌 = (𝑖𝐼 ↦ (𝑌𝑖)))
9 iftrue 4070 . . . . . . . . 9 (𝑖 ∈ (𝑌 “ ℕ) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
109adantl 482 . . . . . . . 8 (((𝜑𝑖𝐼) ∧ 𝑖 ∈ (𝑌 “ ℕ)) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
11 eldif 3570 . . . . . . . . . 10 (𝑖 ∈ (𝐼 ∖ (𝑌 “ ℕ)) ↔ (𝑖𝐼 ∧ ¬ 𝑖 ∈ (𝑌 “ ℕ)))
12 ifid 4103 . . . . . . . . . . 11 if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), (𝑌𝑖)) = (𝑌𝑖)
13 frnnn0supp 11309 . . . . . . . . . . . . . . 15 ((𝐼𝑊𝑌:𝐼⟶ℕ0) → (𝑌 supp 0) = (𝑌 “ ℕ))
142, 7, 13syl2anc 692 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 supp 0) = (𝑌 “ ℕ))
15 eqimss 3642 . . . . . . . . . . . . . 14 ((𝑌 supp 0) = (𝑌 “ ℕ) → (𝑌 supp 0) ⊆ (𝑌 “ ℕ))
1614, 15syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑌 supp 0) ⊆ (𝑌 “ ℕ))
17 c0ex 9994 . . . . . . . . . . . . . 14 0 ∈ V
1817a1i 11 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ V)
197, 16, 2, 18suppssr 7286 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → (𝑌𝑖) = 0)
2019ifeq2d 4083 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), (𝑌𝑖)) = if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0))
2112, 20syl5reqr 2670 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
2211, 21sylan2br 493 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝐼 ∧ ¬ 𝑖 ∈ (𝑌 “ ℕ))) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
2322anassrs 679 . . . . . . . 8 (((𝜑𝑖𝐼) ∧ ¬ 𝑖 ∈ (𝑌 “ ℕ)) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
2410, 23pm2.61dan 831 . . . . . . 7 ((𝜑𝑖𝐼) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
2524mpteq2dva 4714 . . . . . 6 (𝜑 → (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)) = (𝑖𝐼 ↦ (𝑌𝑖)))
268, 25eqtr4d 2658 . . . . 5 (𝜑𝑌 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)))
2726eqeq2d 2631 . . . 4 (𝜑 → (𝑦 = 𝑌𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0))))
2827ifbid 4086 . . 3 (𝜑 → if(𝑦 = 𝑌, 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 ))
2928mpteq2dv 4715 . 2 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )))
30 cnvimass 5454 . . . . 5 (𝑌 “ ℕ) ⊆ dom 𝑌
31 fdm 6018 . . . . . 6 (𝑌:𝐼⟶ℕ0 → dom 𝑌 = 𝐼)
327, 31syl 17 . . . . 5 (𝜑 → dom 𝑌 = 𝐼)
3330, 32syl5sseq 3638 . . . 4 (𝜑 → (𝑌 “ ℕ) ⊆ 𝐼)
346simprd 479 . . . . 5 (𝜑 → (𝑌 “ ℕ) ∈ Fin)
35 sseq1 3611 . . . . . . . 8 (𝑤 = ∅ → (𝑤𝐼 ↔ ∅ ⊆ 𝐼))
36 noel 3901 . . . . . . . . . . . . . . . 16 ¬ 𝑖 ∈ ∅
37 eleq2 2687 . . . . . . . . . . . . . . . 16 (𝑤 = ∅ → (𝑖𝑤𝑖 ∈ ∅))
3836, 37mtbiri 317 . . . . . . . . . . . . . . 15 (𝑤 = ∅ → ¬ 𝑖𝑤)
3938iffalsed 4075 . . . . . . . . . . . . . 14 (𝑤 = ∅ → if(𝑖𝑤, (𝑌𝑖), 0) = 0)
4039mpteq2dv 4715 . . . . . . . . . . . . 13 (𝑤 = ∅ → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ 0))
41 fconstmpt 5133 . . . . . . . . . . . . 13 (𝐼 × {0}) = (𝑖𝐼 ↦ 0)
4240, 41syl6eqr 2673 . . . . . . . . . . . 12 (𝑤 = ∅ → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝐼 × {0}))
4342eqeq2d 2631 . . . . . . . . . . 11 (𝑤 = ∅ → (𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) ↔ 𝑦 = (𝐼 × {0})))
4443ifbid 4086 . . . . . . . . . 10 (𝑤 = ∅ → if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 ) = if(𝑦 = (𝐼 × {0}), 1 , 0 ))
4544mpteq2dv 4715 . . . . . . . . 9 (𝑤 = ∅ → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )))
46 mpteq1 4707 . . . . . . . . . . . 12 (𝑤 = ∅ → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘 ∈ ∅ ↦ ((𝑌𝑘) (𝑉𝑘))))
47 mpt0 5988 . . . . . . . . . . . 12 (𝑘 ∈ ∅ ↦ ((𝑌𝑘) (𝑉𝑘))) = ∅
4846, 47syl6eq 2671 . . . . . . . . . . 11 (𝑤 = ∅ → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = ∅)
4948oveq2d 6631 . . . . . . . . . 10 (𝑤 = ∅ → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (𝐺 Σg ∅))
50 mplcoe2.g . . . . . . . . . . . 12 𝐺 = (mulGrp‘𝑃)
51 eqid 2621 . . . . . . . . . . . 12 (1r𝑃) = (1r𝑃)
5250, 51ringidval 18443 . . . . . . . . . . 11 (1r𝑃) = (0g𝐺)
5352gsum0 17218 . . . . . . . . . 10 (𝐺 Σg ∅) = (1r𝑃)
5449, 53syl6eq 2671 . . . . . . . . 9 (𝑤 = ∅ → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (1r𝑃))
5545, 54eqeq12d 2636 . . . . . . . 8 (𝑤 = ∅ → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) ↔ (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )) = (1r𝑃)))
5635, 55imbi12d 334 . . . . . . 7 (𝑤 = ∅ → ((𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))))) ↔ (∅ ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )) = (1r𝑃))))
5756imbi2d 330 . . . . . 6 (𝑤 = ∅ → ((𝜑 → (𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))))) ↔ (𝜑 → (∅ ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )) = (1r𝑃)))))
58 sseq1 3611 . . . . . . . 8 (𝑤 = 𝑥 → (𝑤𝐼𝑥𝐼))
59 eleq2 2687 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝑖𝑤𝑖𝑥))
6059ifbid 4086 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → if(𝑖𝑤, (𝑌𝑖), 0) = if(𝑖𝑥, (𝑌𝑖), 0))
6160mpteq2dv 4715 . . . . . . . . . . . 12 (𝑤 = 𝑥 → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)))
6261eqeq2d 2631 . . . . . . . . . . 11 (𝑤 = 𝑥 → (𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) ↔ 𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0))))
6362ifbid 4086 . . . . . . . . . 10 (𝑤 = 𝑥 → if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))
6463mpteq2dv 4715 . . . . . . . . 9 (𝑤 = 𝑥 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )))
65 mpteq1 4707 . . . . . . . . . 10 (𝑤 = 𝑥 → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))
6665oveq2d 6631 . . . . . . . . 9 (𝑤 = 𝑥 → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))))
6764, 66eqeq12d 2636 . . . . . . . 8 (𝑤 = 𝑥 → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) ↔ (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))))
6858, 67imbi12d 334 . . . . . . 7 (𝑤 = 𝑥 → ((𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))))) ↔ (𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))))))
6968imbi2d 330 . . . . . 6 (𝑤 = 𝑥 → ((𝜑 → (𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))))) ↔ (𝜑 → (𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))))))
70 sseq1 3611 . . . . . . . 8 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑤𝐼 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐼))
71 eleq2 2687 . . . . . . . . . . . . . 14 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑖𝑤𝑖 ∈ (𝑥 ∪ {𝑧})))
7271ifbid 4086 . . . . . . . . . . . . 13 (𝑤 = (𝑥 ∪ {𝑧}) → if(𝑖𝑤, (𝑌𝑖), 0) = if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))
7372mpteq2dv 4715 . . . . . . . . . . . 12 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)))
7473eqeq2d 2631 . . . . . . . . . . 11 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) ↔ 𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))))
7574ifbid 4086 . . . . . . . . . 10 (𝑤 = (𝑥 ∪ {𝑧}) → if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 ))
7675mpteq2dv 4715 . . . . . . . . 9 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )))
77 mpteq1 4707 . . . . . . . . . 10 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))
7877oveq2d 6631 . . . . . . . . 9 (𝑤 = (𝑥 ∪ {𝑧}) → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))
7976, 78eqeq12d 2636 . . . . . . . 8 (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) ↔ (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))
8070, 79imbi12d 334 . . . . . . 7 (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))))) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
8180imbi2d 330 . . . . . 6 (𝑤 = (𝑥 ∪ {𝑧}) → ((𝜑 → (𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))))) ↔ (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))))
82 sseq1 3611 . . . . . . . 8 (𝑤 = (𝑌 “ ℕ) → (𝑤𝐼 ↔ (𝑌 “ ℕ) ⊆ 𝐼))
83 eleq2 2687 . . . . . . . . . . . . . 14 (𝑤 = (𝑌 “ ℕ) → (𝑖𝑤𝑖 ∈ (𝑌 “ ℕ)))
8483ifbid 4086 . . . . . . . . . . . . 13 (𝑤 = (𝑌 “ ℕ) → if(𝑖𝑤, (𝑌𝑖), 0) = if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0))
8584mpteq2dv 4715 . . . . . . . . . . . 12 (𝑤 = (𝑌 “ ℕ) → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)))
8685eqeq2d 2631 . . . . . . . . . . 11 (𝑤 = (𝑌 “ ℕ) → (𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) ↔ 𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0))))
8786ifbid 4086 . . . . . . . . . 10 (𝑤 = (𝑌 “ ℕ) → if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 ))
8887mpteq2dv 4715 . . . . . . . . 9 (𝑤 = (𝑌 “ ℕ) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )))
89 mpteq1 4707 . . . . . . . . . 10 (𝑤 = (𝑌 “ ℕ) → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))
9089oveq2d 6631 . . . . . . . . 9 (𝑤 = (𝑌 “ ℕ) → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))
9188, 90eqeq12d 2636 . . . . . . . 8 (𝑤 = (𝑌 “ ℕ) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) ↔ (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))))
9282, 91imbi12d 334 . . . . . . 7 (𝑤 = (𝑌 “ ℕ) → ((𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))))) ↔ ((𝑌 “ ℕ) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
9392imbi2d 330 . . . . . 6 (𝑤 = (𝑌 “ ℕ) → ((𝜑 → (𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))))) ↔ (𝜑 → ((𝑌 “ ℕ) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))))))
94 mplcoe1.p . . . . . . . . 9 𝑃 = (𝐼 mPoly 𝑅)
95 mplcoe1.z . . . . . . . . 9 0 = (0g𝑅)
96 mplcoe1.o . . . . . . . . 9 1 = (1r𝑅)
97 mplcoe5.r . . . . . . . . 9 (𝜑𝑅 ∈ Ring)
9894, 3, 95, 96, 51, 2, 97mpl1 19384 . . . . . . . 8 (𝜑 → (1r𝑃) = (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )))
9998eqcomd 2627 . . . . . . 7 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )) = (1r𝑃))
10099a1d 25 . . . . . 6 (𝜑 → (∅ ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )) = (1r𝑃)))
101 ssun1 3760 . . . . . . . . . . 11 𝑥 ⊆ (𝑥 ∪ {𝑧})
102 sstr2 3595 . . . . . . . . . . 11 (𝑥 ⊆ (𝑥 ∪ {𝑧}) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼𝑥𝐼))
103101, 102ax-mp 5 . . . . . . . . . 10 ((𝑥 ∪ {𝑧}) ⊆ 𝐼𝑥𝐼)
104103imim1i 63 . . . . . . . . 9 ((𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))))
105 oveq1 6622 . . . . . . . . . . . 12 ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)((𝑌𝑧) (𝑉𝑧))) = ((𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))(.r𝑃)((𝑌𝑧) (𝑉𝑧))))
106 eqid 2621 . . . . . . . . . . . . . . 15 (Base‘𝑃) = (Base‘𝑃)
1072adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝐼𝑊)
10897adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑅 ∈ Ring)
1097adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑌:𝐼⟶ℕ0)
110109ffvelrnda 6325 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → (𝑌𝑖) ∈ ℕ0)
111 0nn0 11267 . . . . . . . . . . . . . . . . . 18 0 ∈ ℕ0
112 ifcl 4108 . . . . . . . . . . . . . . . . . 18 (((𝑌𝑖) ∈ ℕ0 ∧ 0 ∈ ℕ0) → if(𝑖𝑥, (𝑌𝑖), 0) ∈ ℕ0)
113110, 111, 112sylancl 693 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → if(𝑖𝑥, (𝑌𝑖), 0) ∈ ℕ0)
114 eqid 2621 . . . . . . . . . . . . . . . . 17 (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0))
115113, 114fmptd 6351 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)):𝐼⟶ℕ0)
116 frnnn0supp 11309 . . . . . . . . . . . . . . . . . 18 ((𝐼𝑊 ∧ (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)):𝐼⟶ℕ0) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ))
117107, 115, 116syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ))
118 simprll 801 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑥 ∈ Fin)
119 eldifn 3717 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝐼𝑥) → ¬ 𝑖𝑥)
120119adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖 ∈ (𝐼𝑥)) → ¬ 𝑖𝑥)
121120iffalsed 4075 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖 ∈ (𝐼𝑥)) → if(𝑖𝑥, (𝑌𝑖), 0) = 0)
122121, 107suppss2 7289 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) ⊆ 𝑥)
123 ssfi 8140 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ Fin ∧ ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) ⊆ 𝑥) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) ∈ Fin)
124118, 122, 123syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) ∈ Fin)
125117, 124eqeltrrd 2699 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ) ∈ Fin)
1263psrbag 19304 . . . . . . . . . . . . . . . . 17 (𝐼𝑊 → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∈ 𝐷 ↔ ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)):𝐼⟶ℕ0 ∧ ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ) ∈ Fin)))
127107, 126syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∈ 𝐷 ↔ ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)):𝐼⟶ℕ0 ∧ ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ) ∈ Fin)))
128115, 125, 127mpbir2and 956 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∈ 𝐷)
129 eqid 2621 . . . . . . . . . . . . . . 15 (.r𝑃) = (.r𝑃)
130 ssun2 3761 . . . . . . . . . . . . . . . . . . 19 {𝑧} ⊆ (𝑥 ∪ {𝑧})
131 simprr 795 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑥 ∪ {𝑧}) ⊆ 𝐼)
132130, 131syl5ss 3599 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → {𝑧} ⊆ 𝐼)
133 vex 3193 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ V
134133snss 4293 . . . . . . . . . . . . . . . . . 18 (𝑧𝐼 ↔ {𝑧} ⊆ 𝐼)
135132, 134sylibr 224 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑧𝐼)
136109, 135ffvelrnd 6326 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑌𝑧) ∈ ℕ0)
1373snifpsrbag 19306 . . . . . . . . . . . . . . . 16 ((𝐼𝑊 ∧ (𝑌𝑧) ∈ ℕ0) → (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)) ∈ 𝐷)
138107, 136, 137syl2anc 692 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)) ∈ 𝐷)
13994, 106, 95, 96, 3, 107, 108, 128, 129, 138mplmonmul 19404 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)(𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)), 1 , 0 ))) = (𝑦𝐷 ↦ if(𝑦 = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘𝑓 + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))), 1 , 0 )))
140 mplcoe2.m . . . . . . . . . . . . . . . 16 = (.g𝐺)
141 mplcoe2.v . . . . . . . . . . . . . . . 16 𝑉 = (𝐼 mVar 𝑅)
14294, 3, 95, 96, 107, 50, 140, 141, 108, 135, 136mplcoe3 19406 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)), 1 , 0 )) = ((𝑌𝑧) (𝑉𝑧)))
143142oveq2d 6631 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)(𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)), 1 , 0 ))) = ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)((𝑌𝑧) (𝑉𝑧))))
144136adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → (𝑌𝑧) ∈ ℕ0)
145 ifcl 4108 . . . . . . . . . . . . . . . . . . . 20 (((𝑌𝑧) ∈ ℕ0 ∧ 0 ∈ ℕ0) → if(𝑖 = 𝑧, (𝑌𝑧), 0) ∈ ℕ0)
146144, 111, 145sylancl 693 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → if(𝑖 = 𝑧, (𝑌𝑧), 0) ∈ ℕ0)
147 eqidd 2622 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)))
148 eqidd 2622 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)) = (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)))
149107, 113, 146, 147, 148offval2 6879 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘𝑓 + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))) = (𝑖𝐼 ↦ (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0))))
150110adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (𝑌𝑖) ∈ ℕ0)
151150nn0cnd 11313 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (𝑌𝑖) ∈ ℂ)
152151addid2d 10197 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (0 + (𝑌𝑖)) = (𝑌𝑖))
153 elsni 4172 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ {𝑧} → 𝑖 = 𝑧)
154153adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → 𝑖 = 𝑧)
155 simprlr 802 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ¬ 𝑧𝑥)
156155ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → ¬ 𝑧𝑥)
157154, 156eqneltrd 2717 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → ¬ 𝑖𝑥)
158157iffalsed 4075 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → if(𝑖𝑥, (𝑌𝑖), 0) = 0)
159154iftrued 4072 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → if(𝑖 = 𝑧, (𝑌𝑧), 0) = (𝑌𝑧))
160154fveq2d 6162 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (𝑌𝑖) = (𝑌𝑧))
161159, 160eqtr4d 2658 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → if(𝑖 = 𝑧, (𝑌𝑧), 0) = (𝑌𝑖))
162158, 161oveq12d 6633 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = (0 + (𝑌𝑖)))
163 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → 𝑖 ∈ {𝑧})
164130, 163sseldi 3586 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → 𝑖 ∈ (𝑥 ∪ {𝑧}))
165164iftrued 4072 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0) = (𝑌𝑖))
166152, 162, 1653eqtr4d 2665 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))
167113adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → if(𝑖𝑥, (𝑌𝑖), 0) ∈ ℕ0)
168167nn0cnd 11313 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → if(𝑖𝑥, (𝑌𝑖), 0) ∈ ℂ)
169168addid1d 10196 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + 0) = if(𝑖𝑥, (𝑌𝑖), 0))
170 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → ¬ 𝑖 ∈ {𝑧})
171 velsn 4171 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ {𝑧} ↔ 𝑖 = 𝑧)
172170, 171sylnib 318 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → ¬ 𝑖 = 𝑧)
173172iffalsed 4075 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → if(𝑖 = 𝑧, (𝑌𝑧), 0) = 0)
174173oveq2d 6631 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = (if(𝑖𝑥, (𝑌𝑖), 0) + 0))
175 biorf 420 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑖 ∈ {𝑧} → (𝑖𝑥 ↔ (𝑖 ∈ {𝑧} ∨ 𝑖𝑥)))
176 elun 3737 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑖𝑥𝑖 ∈ {𝑧}))
177 orcom 402 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖𝑥𝑖 ∈ {𝑧}) ↔ (𝑖 ∈ {𝑧} ∨ 𝑖𝑥))
178176, 177bitri 264 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑖 ∈ {𝑧} ∨ 𝑖𝑥))
179175, 178syl6rbbr 279 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖 ∈ {𝑧} → (𝑖 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑖𝑥))
180179adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → (𝑖 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑖𝑥))
181180ifbid 4086 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0) = if(𝑖𝑥, (𝑌𝑖), 0))
182169, 174, 1813eqtr4d 2665 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))
183166, 182pm2.61dan 831 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))
184183mpteq2dva 4714 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0))) = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)))
185149, 184eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘𝑓 + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))) = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)))
186185eqeq2d 2631 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑦 = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘𝑓 + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))) ↔ 𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))))
187186ifbid 4086 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → if(𝑦 = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘𝑓 + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))), 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 ))
188187mpteq2dv 4715 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑦𝐷 ↦ if(𝑦 = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘𝑓 + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )))
189139, 143, 1883eqtr3rd 2664 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)((𝑌𝑧) (𝑉𝑧))))
19050, 106mgpbas 18435 . . . . . . . . . . . . . 14 (Base‘𝑃) = (Base‘𝐺)
19150, 129mgpplusg 18433 . . . . . . . . . . . . . 14 (.r𝑃) = (+g𝐺)
192 eqid 2621 . . . . . . . . . . . . . 14 (Cntz‘𝐺) = (Cntz‘𝐺)
193 eqid 2621 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))
19494mplring 19392 . . . . . . . . . . . . . . . . 17 ((𝐼𝑊𝑅 ∈ Ring) → 𝑃 ∈ Ring)
1952, 97, 194syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ Ring)
19650ringmgp 18493 . . . . . . . . . . . . . . . 16 (𝑃 ∈ Ring → 𝐺 ∈ Mnd)
197195, 196syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ Mnd)
198197adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝐺 ∈ Mnd)
1991adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑌𝐷)
200 mplcoe5.c . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑥𝐼𝑦𝐼 ((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑥)(+g𝐺)(𝑉𝑦)))
201 fveq2 6158 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑎 → (𝑉𝑥) = (𝑉𝑎))
202201oveq2d 6631 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → ((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑦)(+g𝐺)(𝑉𝑎)))
203201oveq1d 6630 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → ((𝑉𝑥)(+g𝐺)(𝑉𝑦)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑦)))
204202, 203eqeq12d 2636 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → (((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑥)(+g𝐺)(𝑉𝑦)) ↔ ((𝑉𝑦)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑦))))
205 fveq2 6158 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑏 → (𝑉𝑦) = (𝑉𝑏))
206205oveq1d 6630 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 → ((𝑉𝑦)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑏)(+g𝐺)(𝑉𝑎)))
207205oveq2d 6631 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 → ((𝑉𝑎)(+g𝐺)(𝑉𝑦)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏)))
208206, 207eqeq12d 2636 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 → (((𝑉𝑦)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑦)) ↔ ((𝑉𝑏)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏))))
209204, 208cbvral2v 3171 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐼𝑦𝐼 ((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑥)(+g𝐺)(𝑉𝑦)) ↔ ∀𝑎𝐼𝑏𝐼 ((𝑉𝑏)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏)))
210200, 209sylib 208 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑎𝐼𝑏𝐼 ((𝑉𝑏)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏)))
211210adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ∀𝑎𝐼𝑏𝐼 ((𝑉𝑏)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏)))
21294, 3, 95, 96, 107, 50, 140, 141, 108, 199, 211, 131mplcoe5lem 19407 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ran (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))) ⊆ ((Cntz‘𝐺)‘ran (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))
213101, 131syl5ss 3599 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑥𝐼)
214213sselda 3588 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑘𝑥) → 𝑘𝐼)
215197adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → 𝐺 ∈ Mnd)
2167ffvelrnda 6325 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → (𝑌𝑘) ∈ ℕ0)
2172adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → 𝐼𝑊)
21897adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → 𝑅 ∈ Ring)
219 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → 𝑘𝐼)
22094, 141, 106, 217, 218, 219mvrcl 19389 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → (𝑉𝑘) ∈ (Base‘𝑃))
221190, 140mulgnn0cl 17498 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Mnd ∧ (𝑌𝑘) ∈ ℕ0 ∧ (𝑉𝑘) ∈ (Base‘𝑃)) → ((𝑌𝑘) (𝑉𝑘)) ∈ (Base‘𝑃))
222215, 216, 220, 221syl3anc 1323 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐼) → ((𝑌𝑘) (𝑉𝑘)) ∈ (Base‘𝑃))
223222adantlr 750 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑘𝐼) → ((𝑌𝑘) (𝑉𝑘)) ∈ (Base‘𝑃))
224214, 223syldan 487 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑘𝑥) → ((𝑌𝑘) (𝑉𝑘)) ∈ (Base‘𝑃))
22594, 141, 106, 107, 108, 135mvrcl 19389 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑉𝑧) ∈ (Base‘𝑃))
226190, 140mulgnn0cl 17498 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Mnd ∧ (𝑌𝑧) ∈ ℕ0 ∧ (𝑉𝑧) ∈ (Base‘𝑃)) → ((𝑌𝑧) (𝑉𝑧)) ∈ (Base‘𝑃))
227198, 136, 225, 226syl3anc 1323 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑌𝑧) (𝑉𝑧)) ∈ (Base‘𝑃))
228 fveq2 6158 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑧 → (𝑌𝑘) = (𝑌𝑧))
229 fveq2 6158 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑧 → (𝑉𝑘) = (𝑉𝑧))
230228, 229oveq12d 6633 . . . . . . . . . . . . . . 15 (𝑘 = 𝑧 → ((𝑌𝑘) (𝑉𝑘)) = ((𝑌𝑧) (𝑉𝑧)))
231230adantl 482 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑘 = 𝑧) → ((𝑌𝑘) (𝑉𝑘)) = ((𝑌𝑧) (𝑉𝑧)))
232190, 191, 192, 193, 198, 118, 212, 224, 135, 155, 227, 231gsumzunsnd 18295 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))) = ((𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))(.r𝑃)((𝑌𝑧) (𝑉𝑧))))
233189, 232eqeq12d 2636 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))) ↔ ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)((𝑌𝑧) (𝑉𝑧))) = ((𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))(.r𝑃)((𝑌𝑧) (𝑉𝑧)))))
234105, 233syl5ibr 236 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))
235234expr 642 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧𝑥)) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
236235a2d 29 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧𝑥)) → (((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
237104, 236syl5 34 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧𝑥)) → ((𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
238237expcom 451 . . . . . . 7 ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) → (𝜑 → ((𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))))
239238a2d 29 . . . . . 6 ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) → ((𝜑 → (𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))))) → (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))))
24057, 69, 81, 93, 100, 239findcard2s 8161 . . . . 5 ((𝑌 “ ℕ) ∈ Fin → (𝜑 → ((𝑌 “ ℕ) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
24134, 240mpcom 38 . . . 4 (𝜑 → ((𝑌 “ ℕ) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))))
24233, 241mpd 15 . . 3 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))
24333resmptd 5421 . . . 4 (𝜑 → ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ↾ (𝑌 “ ℕ)) = (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))
244243oveq2d 6631 . . 3 (𝜑 → (𝐺 Σg ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ↾ (𝑌 “ ℕ))) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))
245 eqid 2621 . . . . 5 (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))
246222, 245fmptd 6351 . . . 4 (𝜑 → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))):𝐼⟶(Base‘𝑃))
247 ssid 3609 . . . . . 6 𝐼𝐼
248247a1i 11 . . . . 5 (𝜑𝐼𝐼)
24994, 3, 95, 96, 2, 50, 140, 141, 97, 1, 200, 248mplcoe5lem 19407 . . . 4 (𝜑 → ran (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ⊆ ((Cntz‘𝐺)‘ran (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
2507, 16, 2, 18suppssr 7286 . . . . . . 7 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → (𝑌𝑘) = 0)
251250oveq1d 6630 . . . . . 6 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → ((𝑌𝑘) (𝑉𝑘)) = (0 (𝑉𝑘)))
252 eldifi 3716 . . . . . . . 8 (𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ)) → 𝑘𝐼)
253252, 220sylan2 491 . . . . . . 7 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → (𝑉𝑘) ∈ (Base‘𝑃))
254190, 52, 140mulg0 17486 . . . . . . 7 ((𝑉𝑘) ∈ (Base‘𝑃) → (0 (𝑉𝑘)) = (1r𝑃))
255253, 254syl 17 . . . . . 6 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → (0 (𝑉𝑘)) = (1r𝑃))
256251, 255eqtrd 2655 . . . . 5 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → ((𝑌𝑘) (𝑉𝑘)) = (1r𝑃))
257256, 2suppss2 7289 . . . 4 (𝜑 → ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) supp (1r𝑃)) ⊆ (𝑌 “ ℕ))
258 mptexg 6449 . . . . . 6 (𝐼𝑊 → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ∈ V)
2592, 258syl 17 . . . . 5 (𝜑 → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ∈ V)
260 funmpt 5894 . . . . . 6 Fun (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))
261260a1i 11 . . . . 5 (𝜑 → Fun (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))))
262 fvexd 6170 . . . . 5 (𝜑 → (1r𝑃) ∈ V)
263 suppssfifsupp 8250 . . . . 5 ((((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ∈ V ∧ Fun (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ∧ (1r𝑃) ∈ V) ∧ ((𝑌 “ ℕ) ∈ Fin ∧ ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) supp (1r𝑃)) ⊆ (𝑌 “ ℕ))) → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) finSupp (1r𝑃))
264259, 261, 262, 34, 257, 263syl32anc 1331 . . . 4 (𝜑 → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) finSupp (1r𝑃))
265190, 52, 192, 197, 2, 246, 249, 257, 264gsumzres 18250 . . 3 (𝜑 → (𝐺 Σg ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ↾ (𝑌 “ ℕ))) = (𝐺 Σg (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
266242, 244, 2653eqtr2d 2661 . 2 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
26729, 266eqtrd 2655 1 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) = (𝐺 Σg (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1987  wral 2908  {crab 2912  Vcvv 3190  cdif 3557  cun 3558  wss 3560  c0 3897  ifcif 4064  {csn 4155   class class class wbr 4623  cmpt 4683   × cxp 5082  ccnv 5083  dom cdm 5084  cres 5086  cima 5087  Fun wfun 5851  wf 5853  cfv 5857  (class class class)co 6615  𝑓 cof 6860   supp csupp 7255  𝑚 cmap 7817  Fincfn 7915   finSupp cfsupp 8235  0cc0 9896   + caddc 9899  cn 10980  0cn0 11252  Basecbs 15800  +gcplusg 15881  .rcmulr 15882  0gc0g 16040   Σg cgsu 16041  Mndcmnd 17234  .gcmg 17480  Cntzccntz 17688  mulGrpcmgp 18429  1rcur 18441  Ringcrg 18487   mVar cmvr 19292   mPoly cmpl 19293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-ofr 6863  df-om 7028  df-1st 7128  df-2nd 7129  df-supp 7256  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-ixp 7869  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fsupp 8236  df-oi 8375  df-card 8725  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-z 11338  df-uz 11648  df-fz 12285  df-fzo 12423  df-seq 12758  df-hash 13074  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-mulr 15895  df-sca 15897  df-vsca 15898  df-tset 15900  df-0g 16042  df-gsum 16043  df-mre 16186  df-mrc 16187  df-acs 16189  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-mhm 17275  df-submnd 17276  df-grp 17365  df-minusg 17366  df-mulg 17481  df-subg 17531  df-ghm 17598  df-cntz 17690  df-cmn 18135  df-abl 18136  df-mgp 18430  df-ur 18442  df-srg 18446  df-ring 18489  df-subrg 18718  df-psr 19296  df-mvr 19297  df-mpl 19298
This theorem is referenced by:  mplcoe2  19409  ply1coe  19606
  Copyright terms: Public domain W3C validator