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

Theorem mplcoe5 22058
Description: Decompose a monomial into a finite product of powers of variables. Instead of assuming that 𝑅 is a commutative ring (as in mplcoe2 22059), 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 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ 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 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
43psrbag 21937 . . . . . . . . . 10 (𝐼𝑊 → (𝑌𝐷 ↔ (𝑌:𝐼⟶ℕ0 ∧ (𝑌 “ ℕ) ∈ Fin)))
52, 4syl 17 . . . . . . . . 9 (𝜑 → (𝑌𝐷 ↔ (𝑌:𝐼⟶ℕ0 ∧ (𝑌 “ ℕ) ∈ Fin)))
61, 5mpbid 232 . . . . . . . 8 (𝜑 → (𝑌:𝐼⟶ℕ0 ∧ (𝑌 “ ℕ) ∈ Fin))
76simpld 494 . . . . . . 7 (𝜑𝑌:𝐼⟶ℕ0)
87feqmptd 6977 . . . . . 6 (𝜑𝑌 = (𝑖𝐼 ↦ (𝑌𝑖)))
9 iftrue 4531 . . . . . . . . 9 (𝑖 ∈ (𝑌 “ ℕ) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
109adantl 481 . . . . . . . 8 (((𝜑𝑖𝐼) ∧ 𝑖 ∈ (𝑌 “ ℕ)) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
11 eldif 3961 . . . . . . . . . 10 (𝑖 ∈ (𝐼 ∖ (𝑌 “ ℕ)) ↔ (𝑖𝐼 ∧ ¬ 𝑖 ∈ (𝑌 “ ℕ)))
12 fcdmnn0supp 12583 . . . . . . . . . . . . . . 15 ((𝐼𝑊𝑌:𝐼⟶ℕ0) → (𝑌 supp 0) = (𝑌 “ ℕ))
132, 7, 12syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 supp 0) = (𝑌 “ ℕ))
14 eqimss 4042 . . . . . . . . . . . . . 14 ((𝑌 supp 0) = (𝑌 “ ℕ) → (𝑌 supp 0) ⊆ (𝑌 “ ℕ))
1513, 14syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑌 supp 0) ⊆ (𝑌 “ ℕ))
16 c0ex 11255 . . . . . . . . . . . . . 14 0 ∈ V
1716a1i 11 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ V)
187, 15, 2, 17suppssr 8220 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → (𝑌𝑖) = 0)
1918ifeq2d 4546 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), (𝑌𝑖)) = if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0))
20 ifid 4566 . . . . . . . . . . 11 if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), (𝑌𝑖)) = (𝑌𝑖)
2119, 20eqtr3di 2792 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
2211, 21sylan2br 595 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝐼 ∧ ¬ 𝑖 ∈ (𝑌 “ ℕ))) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
2322anassrs 467 . . . . . . . 8 (((𝜑𝑖𝐼) ∧ ¬ 𝑖 ∈ (𝑌 “ ℕ)) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
2410, 23pm2.61dan 813 . . . . . . 7 ((𝜑𝑖𝐼) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
2524mpteq2dva 5242 . . . . . 6 (𝜑 → (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)) = (𝑖𝐼 ↦ (𝑌𝑖)))
268, 25eqtr4d 2780 . . . . 5 (𝜑𝑌 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)))
2726eqeq2d 2748 . . . 4 (𝜑 → (𝑦 = 𝑌𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0))))
2827ifbid 4549 . . 3 (𝜑 → if(𝑦 = 𝑌, 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 ))
2928mpteq2dv 5244 . 2 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )))
30 cnvimass 6100 . . . . 5 (𝑌 “ ℕ) ⊆ dom 𝑌
3130, 7fssdm 6755 . . . 4 (𝜑 → (𝑌 “ ℕ) ⊆ 𝐼)
326simprd 495 . . . . 5 (𝜑 → (𝑌 “ ℕ) ∈ Fin)
33 sseq1 4009 . . . . . . . 8 (𝑤 = ∅ → (𝑤𝐼 ↔ ∅ ⊆ 𝐼))
34 noel 4338 . . . . . . . . . . . . . . . 16 ¬ 𝑖 ∈ ∅
35 eleq2 2830 . . . . . . . . . . . . . . . 16 (𝑤 = ∅ → (𝑖𝑤𝑖 ∈ ∅))
3634, 35mtbiri 327 . . . . . . . . . . . . . . 15 (𝑤 = ∅ → ¬ 𝑖𝑤)
3736iffalsed 4536 . . . . . . . . . . . . . 14 (𝑤 = ∅ → if(𝑖𝑤, (𝑌𝑖), 0) = 0)
3837mpteq2dv 5244 . . . . . . . . . . . . 13 (𝑤 = ∅ → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ 0))
39 fconstmpt 5747 . . . . . . . . . . . . 13 (𝐼 × {0}) = (𝑖𝐼 ↦ 0)
4038, 39eqtr4di 2795 . . . . . . . . . . . 12 (𝑤 = ∅ → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝐼 × {0}))
4140eqeq2d 2748 . . . . . . . . . . 11 (𝑤 = ∅ → (𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) ↔ 𝑦 = (𝐼 × {0})))
4241ifbid 4549 . . . . . . . . . 10 (𝑤 = ∅ → if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 ) = if(𝑦 = (𝐼 × {0}), 1 , 0 ))
4342mpteq2dv 5244 . . . . . . . . 9 (𝑤 = ∅ → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )))
44 mpteq1 5235 . . . . . . . . . . . 12 (𝑤 = ∅ → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘 ∈ ∅ ↦ ((𝑌𝑘) (𝑉𝑘))))
45 mpt0 6710 . . . . . . . . . . . 12 (𝑘 ∈ ∅ ↦ ((𝑌𝑘) (𝑉𝑘))) = ∅
4644, 45eqtrdi 2793 . . . . . . . . . . 11 (𝑤 = ∅ → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = ∅)
4746oveq2d 7447 . . . . . . . . . 10 (𝑤 = ∅ → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (𝐺 Σg ∅))
48 mplcoe2.g . . . . . . . . . . . 12 𝐺 = (mulGrp‘𝑃)
49 eqid 2737 . . . . . . . . . . . 12 (1r𝑃) = (1r𝑃)
5048, 49ringidval 20180 . . . . . . . . . . 11 (1r𝑃) = (0g𝐺)
5150gsum0 18697 . . . . . . . . . 10 (𝐺 Σg ∅) = (1r𝑃)
5247, 51eqtrdi 2793 . . . . . . . . 9 (𝑤 = ∅ → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (1r𝑃))
5343, 52eqeq12d 2753 . . . . . . . 8 (𝑤 = ∅ → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) ↔ (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )) = (1r𝑃)))
5433, 53imbi12d 344 . . . . . . 7 (𝑤 = ∅ → ((𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))))) ↔ (∅ ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )) = (1r𝑃))))
5554imbi2d 340 . . . . . 6 (𝑤 = ∅ → ((𝜑 → (𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))))) ↔ (𝜑 → (∅ ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )) = (1r𝑃)))))
56 sseq1 4009 . . . . . . . 8 (𝑤 = 𝑥 → (𝑤𝐼𝑥𝐼))
57 eleq2 2830 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝑖𝑤𝑖𝑥))
5857ifbid 4549 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → if(𝑖𝑤, (𝑌𝑖), 0) = if(𝑖𝑥, (𝑌𝑖), 0))
5958mpteq2dv 5244 . . . . . . . . . . . 12 (𝑤 = 𝑥 → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)))
6059eqeq2d 2748 . . . . . . . . . . 11 (𝑤 = 𝑥 → (𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) ↔ 𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0))))
6160ifbid 4549 . . . . . . . . . 10 (𝑤 = 𝑥 → if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))
6261mpteq2dv 5244 . . . . . . . . 9 (𝑤 = 𝑥 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )))
63 mpteq1 5235 . . . . . . . . . 10 (𝑤 = 𝑥 → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))
6463oveq2d 7447 . . . . . . . . 9 (𝑤 = 𝑥 → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))))
6562, 64eqeq12d 2753 . . . . . . . 8 (𝑤 = 𝑥 → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) ↔ (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))))
6656, 65imbi12d 344 . . . . . . 7 (𝑤 = 𝑥 → ((𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))))) ↔ (𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))))))
6766imbi2d 340 . . . . . 6 (𝑤 = 𝑥 → ((𝜑 → (𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))))) ↔ (𝜑 → (𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))))))
68 sseq1 4009 . . . . . . . 8 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑤𝐼 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐼))
69 eleq2 2830 . . . . . . . . . . . . . 14 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑖𝑤𝑖 ∈ (𝑥 ∪ {𝑧})))
7069ifbid 4549 . . . . . . . . . . . . 13 (𝑤 = (𝑥 ∪ {𝑧}) → if(𝑖𝑤, (𝑌𝑖), 0) = if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))
7170mpteq2dv 5244 . . . . . . . . . . . 12 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)))
7271eqeq2d 2748 . . . . . . . . . . 11 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) ↔ 𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))))
7372ifbid 4549 . . . . . . . . . 10 (𝑤 = (𝑥 ∪ {𝑧}) → if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 ))
7473mpteq2dv 5244 . . . . . . . . 9 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )))
75 mpteq1 5235 . . . . . . . . . 10 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))
7675oveq2d 7447 . . . . . . . . 9 (𝑤 = (𝑥 ∪ {𝑧}) → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))
7774, 76eqeq12d 2753 . . . . . . . 8 (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) ↔ (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))
7868, 77imbi12d 344 . . . . . . 7 (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))))) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
7978imbi2d 340 . . . . . 6 (𝑤 = (𝑥 ∪ {𝑧}) → ((𝜑 → (𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))))) ↔ (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))))
80 sseq1 4009 . . . . . . . 8 (𝑤 = (𝑌 “ ℕ) → (𝑤𝐼 ↔ (𝑌 “ ℕ) ⊆ 𝐼))
81 eleq2 2830 . . . . . . . . . . . . . 14 (𝑤 = (𝑌 “ ℕ) → (𝑖𝑤𝑖 ∈ (𝑌 “ ℕ)))
8281ifbid 4549 . . . . . . . . . . . . 13 (𝑤 = (𝑌 “ ℕ) → if(𝑖𝑤, (𝑌𝑖), 0) = if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0))
8382mpteq2dv 5244 . . . . . . . . . . . 12 (𝑤 = (𝑌 “ ℕ) → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)))
8483eqeq2d 2748 . . . . . . . . . . 11 (𝑤 = (𝑌 “ ℕ) → (𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) ↔ 𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0))))
8584ifbid 4549 . . . . . . . . . 10 (𝑤 = (𝑌 “ ℕ) → if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 ))
8685mpteq2dv 5244 . . . . . . . . 9 (𝑤 = (𝑌 “ ℕ) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )))
87 mpteq1 5235 . . . . . . . . . 10 (𝑤 = (𝑌 “ ℕ) → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))
8887oveq2d 7447 . . . . . . . . 9 (𝑤 = (𝑌 “ ℕ) → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))
8986, 88eqeq12d 2753 . . . . . . . 8 (𝑤 = (𝑌 “ ℕ) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) ↔ (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))))
9080, 89imbi12d 344 . . . . . . 7 (𝑤 = (𝑌 “ ℕ) → ((𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))))) ↔ ((𝑌 “ ℕ) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
9190imbi2d 340 . . . . . 6 (𝑤 = (𝑌 “ ℕ) → ((𝜑 → (𝑤𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))))) ↔ (𝜑 → ((𝑌 “ ℕ) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))))))
92 mplcoe1.p . . . . . . . . 9 𝑃 = (𝐼 mPoly 𝑅)
93 mplcoe1.z . . . . . . . . 9 0 = (0g𝑅)
94 mplcoe1.o . . . . . . . . 9 1 = (1r𝑅)
95 mplcoe5.r . . . . . . . . 9 (𝜑𝑅 ∈ Ring)
9692, 3, 93, 94, 49, 2, 95mpl1 22032 . . . . . . . 8 (𝜑 → (1r𝑃) = (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )))
9796, 49eqtr3di 2792 . . . . . . 7 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )) = (1r𝑃))
9897a1d 25 . . . . . 6 (𝜑 → (∅ ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )) = (1r𝑃)))
99 ssun1 4178 . . . . . . . . . . 11 𝑥 ⊆ (𝑥 ∪ {𝑧})
100 sstr2 3990 . . . . . . . . . . 11 (𝑥 ⊆ (𝑥 ∪ {𝑧}) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼𝑥𝐼))
10199, 100ax-mp 5 . . . . . . . . . 10 ((𝑥 ∪ {𝑧}) ⊆ 𝐼𝑥𝐼)
102101imim1i 63 . . . . . . . . 9 ((𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))))
103 oveq1 7438 . . . . . . . . . . . 12 ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)((𝑌𝑧) (𝑉𝑧))) = ((𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))(.r𝑃)((𝑌𝑧) (𝑉𝑧))))
104 eqid 2737 . . . . . . . . . . . . . . 15 (Base‘𝑃) = (Base‘𝑃)
1052adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝐼𝑊)
10695adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑅 ∈ Ring)
1077adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑌:𝐼⟶ℕ0)
108107ffvelcdmda 7104 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → (𝑌𝑖) ∈ ℕ0)
109 0nn0 12541 . . . . . . . . . . . . . . . . . 18 0 ∈ ℕ0
110 ifcl 4571 . . . . . . . . . . . . . . . . . 18 (((𝑌𝑖) ∈ ℕ0 ∧ 0 ∈ ℕ0) → if(𝑖𝑥, (𝑌𝑖), 0) ∈ ℕ0)
111108, 109, 110sylancl 586 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → if(𝑖𝑥, (𝑌𝑖), 0) ∈ ℕ0)
112111fmpttd 7135 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)):𝐼⟶ℕ0)
113 fcdmnn0supp 12583 . . . . . . . . . . . . . . . . . 18 ((𝐼𝑊 ∧ (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)):𝐼⟶ℕ0) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ))
114105, 112, 113syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ))
115 simprll 779 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑥 ∈ Fin)
116 eldifn 4132 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝐼𝑥) → ¬ 𝑖𝑥)
117116adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖 ∈ (𝐼𝑥)) → ¬ 𝑖𝑥)
118117iffalsed 4536 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖 ∈ (𝐼𝑥)) → if(𝑖𝑥, (𝑌𝑖), 0) = 0)
119118, 105suppss2 8225 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) ⊆ 𝑥)
120115, 119ssfid 9301 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) ∈ Fin)
121114, 120eqeltrrd 2842 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ) ∈ Fin)
1223psrbag 21937 . . . . . . . . . . . . . . . . 17 (𝐼𝑊 → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∈ 𝐷 ↔ ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)):𝐼⟶ℕ0 ∧ ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ) ∈ Fin)))
123105, 122syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∈ 𝐷 ↔ ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)):𝐼⟶ℕ0 ∧ ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ) ∈ Fin)))
124112, 121, 123mpbir2and 713 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∈ 𝐷)
125 eqid 2737 . . . . . . . . . . . . . . 15 (.r𝑃) = (.r𝑃)
126 ssun2 4179 . . . . . . . . . . . . . . . . . . 19 {𝑧} ⊆ (𝑥 ∪ {𝑧})
127 simprr 773 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑥 ∪ {𝑧}) ⊆ 𝐼)
128126, 127sstrid 3995 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → {𝑧} ⊆ 𝐼)
129 vex 3484 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ V
130129snss 4785 . . . . . . . . . . . . . . . . . 18 (𝑧𝐼 ↔ {𝑧} ⊆ 𝐼)
131128, 130sylibr 234 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑧𝐼)
132107, 131ffvelcdmd 7105 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑌𝑧) ∈ ℕ0)
1333snifpsrbag 21940 . . . . . . . . . . . . . . . 16 ((𝐼𝑊 ∧ (𝑌𝑧) ∈ ℕ0) → (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)) ∈ 𝐷)
134105, 132, 133syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)) ∈ 𝐷)
13592, 104, 93, 94, 3, 105, 106, 124, 125, 134mplmonmul 22054 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)(𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)), 1 , 0 ))) = (𝑦𝐷 ↦ if(𝑦 = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘f + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))), 1 , 0 )))
136 mplcoe2.m . . . . . . . . . . . . . . . 16 = (.g𝐺)
137 mplcoe2.v . . . . . . . . . . . . . . . 16 𝑉 = (𝐼 mVar 𝑅)
13892, 3, 93, 94, 105, 48, 136, 137, 106, 131, 132mplcoe3 22056 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)), 1 , 0 )) = ((𝑌𝑧) (𝑉𝑧)))
139138oveq2d 7447 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)(𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)), 1 , 0 ))) = ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)((𝑌𝑧) (𝑉𝑧))))
140132adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → (𝑌𝑧) ∈ ℕ0)
141 ifcl 4571 . . . . . . . . . . . . . . . . . . . 20 (((𝑌𝑧) ∈ ℕ0 ∧ 0 ∈ ℕ0) → if(𝑖 = 𝑧, (𝑌𝑧), 0) ∈ ℕ0)
142140, 109, 141sylancl 586 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → if(𝑖 = 𝑧, (𝑌𝑧), 0) ∈ ℕ0)
143 eqidd 2738 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)))
144 eqidd 2738 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)) = (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)))
145105, 111, 142, 143, 144offval2 7717 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘f + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))) = (𝑖𝐼 ↦ (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0))))
146108adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (𝑌𝑖) ∈ ℕ0)
147146nn0cnd 12589 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (𝑌𝑖) ∈ ℂ)
148147addlidd 11462 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (0 + (𝑌𝑖)) = (𝑌𝑖))
149 elsni 4643 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ {𝑧} → 𝑖 = 𝑧)
150149adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → 𝑖 = 𝑧)
151 simprlr 780 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ¬ 𝑧𝑥)
152151ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → ¬ 𝑧𝑥)
153150, 152eqneltrd 2861 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → ¬ 𝑖𝑥)
154153iffalsed 4536 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → if(𝑖𝑥, (𝑌𝑖), 0) = 0)
155150iftrued 4533 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → if(𝑖 = 𝑧, (𝑌𝑧), 0) = (𝑌𝑧))
156150fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (𝑌𝑖) = (𝑌𝑧))
157155, 156eqtr4d 2780 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → if(𝑖 = 𝑧, (𝑌𝑧), 0) = (𝑌𝑖))
158154, 157oveq12d 7449 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = (0 + (𝑌𝑖)))
159 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → 𝑖 ∈ {𝑧})
160126, 159sselid 3981 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → 𝑖 ∈ (𝑥 ∪ {𝑧}))
161160iftrued 4533 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0) = (𝑌𝑖))
162148, 158, 1613eqtr4d 2787 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))
163111adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → if(𝑖𝑥, (𝑌𝑖), 0) ∈ ℕ0)
164163nn0cnd 12589 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → if(𝑖𝑥, (𝑌𝑖), 0) ∈ ℂ)
165164addridd 11461 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + 0) = if(𝑖𝑥, (𝑌𝑖), 0))
166 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → ¬ 𝑖 ∈ {𝑧})
167 velsn 4642 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ {𝑧} ↔ 𝑖 = 𝑧)
168166, 167sylnib 328 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → ¬ 𝑖 = 𝑧)
169168iffalsed 4536 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → if(𝑖 = 𝑧, (𝑌𝑧), 0) = 0)
170169oveq2d 7447 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = (if(𝑖𝑥, (𝑌𝑖), 0) + 0))
171 elun 4153 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑖𝑥𝑖 ∈ {𝑧}))
172 orcom 871 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖𝑥𝑖 ∈ {𝑧}) ↔ (𝑖 ∈ {𝑧} ∨ 𝑖𝑥))
173171, 172bitri 275 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑖 ∈ {𝑧} ∨ 𝑖𝑥))
174 biorf 937 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑖 ∈ {𝑧} → (𝑖𝑥 ↔ (𝑖 ∈ {𝑧} ∨ 𝑖𝑥)))
175173, 174bitr4id 290 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖 ∈ {𝑧} → (𝑖 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑖𝑥))
176175adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → (𝑖 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑖𝑥))
177176ifbid 4549 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0) = if(𝑖𝑥, (𝑌𝑖), 0))
178165, 170, 1773eqtr4d 2787 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))
179162, 178pm2.61dan 813 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))
180179mpteq2dva 5242 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0))) = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)))
181145, 180eqtrd 2777 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘f + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))) = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)))
182181eqeq2d 2748 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑦 = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘f + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))) ↔ 𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))))
183182ifbid 4549 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → if(𝑦 = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘f + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))), 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 ))
184183mpteq2dv 5244 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑦𝐷 ↦ if(𝑦 = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘f + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )))
185135, 139, 1843eqtr3rd 2786 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)((𝑌𝑧) (𝑉𝑧))))
18648, 104mgpbas 20142 . . . . . . . . . . . . . 14 (Base‘𝑃) = (Base‘𝐺)
18748, 125mgpplusg 20141 . . . . . . . . . . . . . 14 (.r𝑃) = (+g𝐺)
188 eqid 2737 . . . . . . . . . . . . . 14 (Cntz‘𝐺) = (Cntz‘𝐺)
189 eqid 2737 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))
19092, 2, 95mplringd 22043 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ Ring)
19148ringmgp 20236 . . . . . . . . . . . . . . . 16 (𝑃 ∈ Ring → 𝐺 ∈ Mnd)
192190, 191syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ Mnd)
193192adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝐺 ∈ Mnd)
1941adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑌𝐷)
195 mplcoe5.c . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑥𝐼𝑦𝐼 ((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑥)(+g𝐺)(𝑉𝑦)))
196 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑎 → (𝑉𝑥) = (𝑉𝑎))
197196oveq2d 7447 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → ((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑦)(+g𝐺)(𝑉𝑎)))
198196oveq1d 7446 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → ((𝑉𝑥)(+g𝐺)(𝑉𝑦)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑦)))
199197, 198eqeq12d 2753 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → (((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑥)(+g𝐺)(𝑉𝑦)) ↔ ((𝑉𝑦)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑦))))
200 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑏 → (𝑉𝑦) = (𝑉𝑏))
201200oveq1d 7446 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 → ((𝑉𝑦)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑏)(+g𝐺)(𝑉𝑎)))
202200oveq2d 7447 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 → ((𝑉𝑎)(+g𝐺)(𝑉𝑦)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏)))
203201, 202eqeq12d 2753 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 → (((𝑉𝑦)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑦)) ↔ ((𝑉𝑏)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏))))
204199, 203cbvral2vw 3241 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐼𝑦𝐼 ((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑥)(+g𝐺)(𝑉𝑦)) ↔ ∀𝑎𝐼𝑏𝐼 ((𝑉𝑏)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏)))
205195, 204sylib 218 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑎𝐼𝑏𝐼 ((𝑉𝑏)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏)))
206205adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ∀𝑎𝐼𝑏𝐼 ((𝑉𝑏)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏)))
20792, 3, 93, 94, 105, 48, 136, 137, 106, 194, 206, 127mplcoe5lem 22057 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ran (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))) ⊆ ((Cntz‘𝐺)‘ran (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))
20899, 127sstrid 3995 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑥𝐼)
209208sselda 3983 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑘𝑥) → 𝑘𝐼)
210192adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → 𝐺 ∈ Mnd)
2117ffvelcdmda 7104 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → (𝑌𝑘) ∈ ℕ0)
2122adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → 𝐼𝑊)
21395adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → 𝑅 ∈ Ring)
214 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → 𝑘𝐼)
21592, 137, 104, 212, 213, 214mvrcl 22012 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → (𝑉𝑘) ∈ (Base‘𝑃))
216186, 136, 210, 211, 215mulgnn0cld 19113 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐼) → ((𝑌𝑘) (𝑉𝑘)) ∈ (Base‘𝑃))
217216adantlr 715 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑘𝐼) → ((𝑌𝑘) (𝑉𝑘)) ∈ (Base‘𝑃))
218209, 217syldan 591 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑘𝑥) → ((𝑌𝑘) (𝑉𝑘)) ∈ (Base‘𝑃))
21992, 137, 104, 105, 106, 131mvrcl 22012 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑉𝑧) ∈ (Base‘𝑃))
220186, 136, 193, 132, 219mulgnn0cld 19113 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑌𝑧) (𝑉𝑧)) ∈ (Base‘𝑃))
221 fveq2 6906 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑧 → (𝑌𝑘) = (𝑌𝑧))
222 fveq2 6906 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑧 → (𝑉𝑘) = (𝑉𝑧))
223221, 222oveq12d 7449 . . . . . . . . . . . . . . 15 (𝑘 = 𝑧 → ((𝑌𝑘) (𝑉𝑘)) = ((𝑌𝑧) (𝑉𝑧)))
224223adantl 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑘 = 𝑧) → ((𝑌𝑘) (𝑉𝑘)) = ((𝑌𝑧) (𝑉𝑧)))
225186, 187, 188, 189, 193, 115, 207, 218, 131, 151, 220, 224gsumzunsnd 19974 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))) = ((𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))(.r𝑃)((𝑌𝑧) (𝑉𝑧))))
226185, 225eqeq12d 2753 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))) ↔ ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)((𝑌𝑧) (𝑉𝑧))) = ((𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))(.r𝑃)((𝑌𝑧) (𝑉𝑧)))))
227103, 226imbitrrid 246 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))
228227expr 456 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧𝑥)) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
229228a2d 29 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧𝑥)) → (((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
230102, 229syl5 34 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧𝑥)) → ((𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
231230expcom 413 . . . . . . 7 ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) → (𝜑 → ((𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))))
232231a2d 29 . . . . . 6 ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) → ((𝜑 → (𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))))) → (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))))
23355, 67, 79, 91, 98, 232findcard2s 9205 . . . . 5 ((𝑌 “ ℕ) ∈ Fin → (𝜑 → ((𝑌 “ ℕ) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
23432, 233mpcom 38 . . . 4 (𝜑 → ((𝑌 “ ℕ) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))))
23531, 234mpd 15 . . 3 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))
23631resmptd 6058 . . . 4 (𝜑 → ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ↾ (𝑌 “ ℕ)) = (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))
237236oveq2d 7447 . . 3 (𝜑 → (𝐺 Σg ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ↾ (𝑌 “ ℕ))) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))
238216fmpttd 7135 . . . 4 (𝜑 → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))):𝐼⟶(Base‘𝑃))
239 ssidd 4007 . . . . 5 (𝜑𝐼𝐼)
24092, 3, 93, 94, 2, 48, 136, 137, 95, 1, 195, 239mplcoe5lem 22057 . . . 4 (𝜑 → ran (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ⊆ ((Cntz‘𝐺)‘ran (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
2417, 15, 2, 17suppssr 8220 . . . . . . 7 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → (𝑌𝑘) = 0)
242241oveq1d 7446 . . . . . 6 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → ((𝑌𝑘) (𝑉𝑘)) = (0 (𝑉𝑘)))
243 eldifi 4131 . . . . . . . 8 (𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ)) → 𝑘𝐼)
244243, 215sylan2 593 . . . . . . 7 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → (𝑉𝑘) ∈ (Base‘𝑃))
245186, 50, 136mulg0 19092 . . . . . . 7 ((𝑉𝑘) ∈ (Base‘𝑃) → (0 (𝑉𝑘)) = (1r𝑃))
246244, 245syl 17 . . . . . 6 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → (0 (𝑉𝑘)) = (1r𝑃))
247242, 246eqtrd 2777 . . . . 5 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → ((𝑌𝑘) (𝑉𝑘)) = (1r𝑃))
248247, 2suppss2 8225 . . . 4 (𝜑 → ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) supp (1r𝑃)) ⊆ (𝑌 “ ℕ))
2492mptexd 7244 . . . . 5 (𝜑 → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ∈ V)
250 funmpt 6604 . . . . . 6 Fun (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))
251250a1i 11 . . . . 5 (𝜑 → Fun (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))))
252 fvexd 6921 . . . . 5 (𝜑 → (1r𝑃) ∈ V)
253 suppssfifsupp 9420 . . . . 5 ((((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ∈ V ∧ Fun (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ∧ (1r𝑃) ∈ V) ∧ ((𝑌 “ ℕ) ∈ Fin ∧ ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) supp (1r𝑃)) ⊆ (𝑌 “ ℕ))) → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) finSupp (1r𝑃))
254249, 251, 252, 32, 248, 253syl32anc 1380 . . . 4 (𝜑 → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) finSupp (1r𝑃))
255186, 50, 188, 192, 2, 238, 240, 248, 254gsumzres 19927 . . 3 (𝜑 → (𝐺 Σg ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ↾ (𝑌 “ ℕ))) = (𝐺 Σg (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
256235, 237, 2553eqtr2d 2783 . 2 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
25729, 256eqtrd 2777 1 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) = (𝐺 Σg (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wcel 2108  wral 3061  {crab 3436  Vcvv 3480  cdif 3948  cun 3949  wss 3951  c0 4333  ifcif 4525  {csn 4626   class class class wbr 5143  cmpt 5225   × cxp 5683  ccnv 5684  cres 5687  cima 5688  Fun wfun 6555  wf 6557  cfv 6561  (class class class)co 7431  f cof 7695   supp csupp 8185  m cmap 8866  Fincfn 8985   finSupp cfsupp 9401  0cc0 11155   + caddc 11158  cn 12266  0cn0 12526  Basecbs 17247  +gcplusg 17297  .rcmulr 17298  0gc0g 17484   Σg cgsu 17485  Mndcmnd 18747  .gcmg 19085  Cntzccntz 19333  mulGrpcmgp 20137  1rcur 20178  Ringcrg 20230   mVar cmvr 21925   mPoly cmpl 21926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-ofr 7698  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-sup 9482  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-fz 13548  df-fzo 13695  df-seq 14043  df-hash 14370  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-hom 17321  df-cco 17322  df-0g 17486  df-gsum 17487  df-prds 17492  df-pws 17494  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-mhm 18796  df-submnd 18797  df-grp 18954  df-minusg 18955  df-mulg 19086  df-subg 19141  df-ghm 19231  df-cntz 19335  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-srg 20184  df-ring 20232  df-subrng 20546  df-subrg 20570  df-psr 21929  df-mvr 21930  df-mpl 21931
This theorem is referenced by:  mplcoe2  22059  ply1coe  22302
  Copyright terms: Public domain W3C validator