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

Theorem mplcoe5 21441
Description: Decompose a monomial into a finite product of powers of variables. Instead of assuming that 𝑅 is a commutative ring (as in mplcoe2 21442), 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 21319 . . . . . . . . . 10 (𝐼𝑊 → (𝑌𝐷 ↔ (𝑌:𝐼⟶ℕ0 ∧ (𝑌 “ ℕ) ∈ Fin)))
52, 4syl 17 . . . . . . . . 9 (𝜑 → (𝑌𝐷 ↔ (𝑌:𝐼⟶ℕ0 ∧ (𝑌 “ ℕ) ∈ Fin)))
61, 5mpbid 231 . . . . . . . 8 (𝜑 → (𝑌:𝐼⟶ℕ0 ∧ (𝑌 “ ℕ) ∈ Fin))
76simpld 495 . . . . . . 7 (𝜑𝑌:𝐼⟶ℕ0)
87feqmptd 6910 . . . . . 6 (𝜑𝑌 = (𝑖𝐼 ↦ (𝑌𝑖)))
9 iftrue 4492 . . . . . . . . 9 (𝑖 ∈ (𝑌 “ ℕ) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
109adantl 482 . . . . . . . 8 (((𝜑𝑖𝐼) ∧ 𝑖 ∈ (𝑌 “ ℕ)) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
11 eldif 3920 . . . . . . . . . 10 (𝑖 ∈ (𝐼 ∖ (𝑌 “ ℕ)) ↔ (𝑖𝐼 ∧ ¬ 𝑖 ∈ (𝑌 “ ℕ)))
12 fcdmnn0supp 12469 . . . . . . . . . . . . . . 15 ((𝐼𝑊𝑌:𝐼⟶ℕ0) → (𝑌 supp 0) = (𝑌 “ ℕ))
132, 7, 12syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 supp 0) = (𝑌 “ ℕ))
14 eqimss 4000 . . . . . . . . . . . . . 14 ((𝑌 supp 0) = (𝑌 “ ℕ) → (𝑌 supp 0) ⊆ (𝑌 “ ℕ))
1513, 14syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑌 supp 0) ⊆ (𝑌 “ ℕ))
16 c0ex 11149 . . . . . . . . . . . . . 14 0 ∈ V
1716a1i 11 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ V)
187, 15, 2, 17suppssr 8127 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → (𝑌𝑖) = 0)
1918ifeq2d 4506 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), (𝑌𝑖)) = if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0))
20 ifid 4526 . . . . . . . . . . 11 if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), (𝑌𝑖)) = (𝑌𝑖)
2119, 20eqtr3di 2791 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
2211, 21sylan2br 595 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝐼 ∧ ¬ 𝑖 ∈ (𝑌 “ ℕ))) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
2322anassrs 468 . . . . . . . 8 (((𝜑𝑖𝐼) ∧ ¬ 𝑖 ∈ (𝑌 “ ℕ)) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
2410, 23pm2.61dan 811 . . . . . . 7 ((𝜑𝑖𝐼) → if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0) = (𝑌𝑖))
2524mpteq2dva 5205 . . . . . 6 (𝜑 → (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)) = (𝑖𝐼 ↦ (𝑌𝑖)))
268, 25eqtr4d 2779 . . . . 5 (𝜑𝑌 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)))
2726eqeq2d 2747 . . . 4 (𝜑 → (𝑦 = 𝑌𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0))))
2827ifbid 4509 . . 3 (𝜑 → if(𝑦 = 𝑌, 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 ))
2928mpteq2dv 5207 . 2 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )))
30 cnvimass 6033 . . . . 5 (𝑌 “ ℕ) ⊆ dom 𝑌
3130, 7fssdm 6688 . . . 4 (𝜑 → (𝑌 “ ℕ) ⊆ 𝐼)
326simprd 496 . . . . 5 (𝜑 → (𝑌 “ ℕ) ∈ Fin)
33 sseq1 3969 . . . . . . . 8 (𝑤 = ∅ → (𝑤𝐼 ↔ ∅ ⊆ 𝐼))
34 noel 4290 . . . . . . . . . . . . . . . 16 ¬ 𝑖 ∈ ∅
35 eleq2 2826 . . . . . . . . . . . . . . . 16 (𝑤 = ∅ → (𝑖𝑤𝑖 ∈ ∅))
3634, 35mtbiri 326 . . . . . . . . . . . . . . 15 (𝑤 = ∅ → ¬ 𝑖𝑤)
3736iffalsed 4497 . . . . . . . . . . . . . 14 (𝑤 = ∅ → if(𝑖𝑤, (𝑌𝑖), 0) = 0)
3837mpteq2dv 5207 . . . . . . . . . . . . 13 (𝑤 = ∅ → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ 0))
39 fconstmpt 5694 . . . . . . . . . . . . 13 (𝐼 × {0}) = (𝑖𝐼 ↦ 0)
4038, 39eqtr4di 2794 . . . . . . . . . . . 12 (𝑤 = ∅ → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝐼 × {0}))
4140eqeq2d 2747 . . . . . . . . . . 11 (𝑤 = ∅ → (𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) ↔ 𝑦 = (𝐼 × {0})))
4241ifbid 4509 . . . . . . . . . 10 (𝑤 = ∅ → if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 ) = if(𝑦 = (𝐼 × {0}), 1 , 0 ))
4342mpteq2dv 5207 . . . . . . . . 9 (𝑤 = ∅ → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )))
44 mpteq1 5198 . . . . . . . . . . . 12 (𝑤 = ∅ → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘 ∈ ∅ ↦ ((𝑌𝑘) (𝑉𝑘))))
45 mpt0 6643 . . . . . . . . . . . 12 (𝑘 ∈ ∅ ↦ ((𝑌𝑘) (𝑉𝑘))) = ∅
4644, 45eqtrdi 2792 . . . . . . . . . . 11 (𝑤 = ∅ → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = ∅)
4746oveq2d 7373 . . . . . . . . . 10 (𝑤 = ∅ → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (𝐺 Σg ∅))
48 mplcoe2.g . . . . . . . . . . . 12 𝐺 = (mulGrp‘𝑃)
49 eqid 2736 . . . . . . . . . . . 12 (1r𝑃) = (1r𝑃)
5048, 49ringidval 19915 . . . . . . . . . . 11 (1r𝑃) = (0g𝐺)
5150gsum0 18539 . . . . . . . . . 10 (𝐺 Σg ∅) = (1r𝑃)
5247, 51eqtrdi 2792 . . . . . . . . 9 (𝑤 = ∅ → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (1r𝑃))
5343, 52eqeq12d 2752 . . . . . . . 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 3969 . . . . . . . 8 (𝑤 = 𝑥 → (𝑤𝐼𝑥𝐼))
57 eleq2 2826 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝑖𝑤𝑖𝑥))
5857ifbid 4509 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → if(𝑖𝑤, (𝑌𝑖), 0) = if(𝑖𝑥, (𝑌𝑖), 0))
5958mpteq2dv 5207 . . . . . . . . . . . 12 (𝑤 = 𝑥 → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)))
6059eqeq2d 2747 . . . . . . . . . . 11 (𝑤 = 𝑥 → (𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) ↔ 𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0))))
6160ifbid 4509 . . . . . . . . . 10 (𝑤 = 𝑥 → if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))
6261mpteq2dv 5207 . . . . . . . . 9 (𝑤 = 𝑥 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )))
63 mpteq1 5198 . . . . . . . . . 10 (𝑤 = 𝑥 → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))
6463oveq2d 7373 . . . . . . . . 9 (𝑤 = 𝑥 → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))))
6562, 64eqeq12d 2752 . . . . . . . 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 3969 . . . . . . . 8 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑤𝐼 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐼))
69 eleq2 2826 . . . . . . . . . . . . . 14 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑖𝑤𝑖 ∈ (𝑥 ∪ {𝑧})))
7069ifbid 4509 . . . . . . . . . . . . 13 (𝑤 = (𝑥 ∪ {𝑧}) → if(𝑖𝑤, (𝑌𝑖), 0) = if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))
7170mpteq2dv 5207 . . . . . . . . . . . 12 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)))
7271eqeq2d 2747 . . . . . . . . . . 11 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) ↔ 𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))))
7372ifbid 4509 . . . . . . . . . 10 (𝑤 = (𝑥 ∪ {𝑧}) → if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 ))
7473mpteq2dv 5207 . . . . . . . . 9 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )))
75 mpteq1 5198 . . . . . . . . . 10 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))
7675oveq2d 7373 . . . . . . . . 9 (𝑤 = (𝑥 ∪ {𝑧}) → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))
7774, 76eqeq12d 2752 . . . . . . . 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 3969 . . . . . . . 8 (𝑤 = (𝑌 “ ℕ) → (𝑤𝐼 ↔ (𝑌 “ ℕ) ⊆ 𝐼))
81 eleq2 2826 . . . . . . . . . . . . . 14 (𝑤 = (𝑌 “ ℕ) → (𝑖𝑤𝑖 ∈ (𝑌 “ ℕ)))
8281ifbid 4509 . . . . . . . . . . . . 13 (𝑤 = (𝑌 “ ℕ) → if(𝑖𝑤, (𝑌𝑖), 0) = if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0))
8382mpteq2dv 5207 . . . . . . . . . . . 12 (𝑤 = (𝑌 “ ℕ) → (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)))
8483eqeq2d 2747 . . . . . . . . . . 11 (𝑤 = (𝑌 “ ℕ) → (𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)) ↔ 𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0))))
8584ifbid 4509 . . . . . . . . . 10 (𝑤 = (𝑌 “ ℕ) → if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 ))
8685mpteq2dv 5207 . . . . . . . . 9 (𝑤 = (𝑌 “ ℕ) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑤, (𝑌𝑖), 0)), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )))
87 mpteq1 5198 . . . . . . . . . 10 (𝑤 = (𝑌 “ ℕ) → (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))
8887oveq2d 7373 . . . . . . . . 9 (𝑤 = (𝑌 “ ℕ) → (𝐺 Σg (𝑘𝑤 ↦ ((𝑌𝑘) (𝑉𝑘)))) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))
8986, 88eqeq12d 2752 . . . . . . . 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 21416 . . . . . . . 8 (𝜑 → (1r𝑃) = (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )))
9796, 49eqtr3di 2791 . . . . . . 7 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )) = (1r𝑃))
9897a1d 25 . . . . . 6 (𝜑 → (∅ ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 1 , 0 )) = (1r𝑃)))
99 ssun1 4132 . . . . . . . . . . 11 𝑥 ⊆ (𝑥 ∪ {𝑧})
100 sstr2 3951 . . . . . . . . . . 11 (𝑥 ⊆ (𝑥 ∪ {𝑧}) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼𝑥𝐼))
10199, 100ax-mp 5 . . . . . . . . . 10 ((𝑥 ∪ {𝑧}) ⊆ 𝐼𝑥𝐼)
102101imim1i 63 . . . . . . . . 9 ((𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))))
103 oveq1 7364 . . . . . . . . . . . 12 ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)((𝑌𝑧) (𝑉𝑧))) = ((𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))(.r𝑃)((𝑌𝑧) (𝑉𝑧))))
104 eqid 2736 . . . . . . . . . . . . . . 15 (Base‘𝑃) = (Base‘𝑃)
1052adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝐼𝑊)
10695adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑅 ∈ Ring)
1077adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑌:𝐼⟶ℕ0)
108107ffvelcdmda 7035 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → (𝑌𝑖) ∈ ℕ0)
109 0nn0 12428 . . . . . . . . . . . . . . . . . 18 0 ∈ ℕ0
110 ifcl 4531 . . . . . . . . . . . . . . . . . 18 (((𝑌𝑖) ∈ ℕ0 ∧ 0 ∈ ℕ0) → if(𝑖𝑥, (𝑌𝑖), 0) ∈ ℕ0)
111108, 109, 110sylancl 586 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → if(𝑖𝑥, (𝑌𝑖), 0) ∈ ℕ0)
112111fmpttd 7063 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)):𝐼⟶ℕ0)
113 fcdmnn0supp 12469 . . . . . . . . . . . . . . . . . 18 ((𝐼𝑊 ∧ (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)):𝐼⟶ℕ0) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ))
114105, 112, 113syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ))
115 simprll 777 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑥 ∈ Fin)
116 eldifn 4087 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝐼𝑥) → ¬ 𝑖𝑥)
117116adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖 ∈ (𝐼𝑥)) → ¬ 𝑖𝑥)
118117iffalsed 4497 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖 ∈ (𝐼𝑥)) → if(𝑖𝑥, (𝑌𝑖), 0) = 0)
119118, 105suppss2 8131 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) ⊆ 𝑥)
120115, 119ssfid 9211 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) supp 0) ∈ Fin)
121114, 120eqeltrrd 2839 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) “ ℕ) ∈ Fin)
1223psrbag 21319 . . . . . . . . . . . . . . . . 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 711 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∈ 𝐷)
125 eqid 2736 . . . . . . . . . . . . . . 15 (.r𝑃) = (.r𝑃)
126 ssun2 4133 . . . . . . . . . . . . . . . . . . 19 {𝑧} ⊆ (𝑥 ∪ {𝑧})
127 simprr 771 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑥 ∪ {𝑧}) ⊆ 𝐼)
128126, 127sstrid 3955 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → {𝑧} ⊆ 𝐼)
129 vex 3449 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ V
130129snss 4746 . . . . . . . . . . . . . . . . . 18 (𝑧𝐼 ↔ {𝑧} ⊆ 𝐼)
131128, 130sylibr 233 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑧𝐼)
132107, 131ffvelcdmd 7036 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑌𝑧) ∈ ℕ0)
1333snifpsrbag 21324 . . . . . . . . . . . . . . . 16 ((𝐼𝑊 ∧ (𝑌𝑧) ∈ ℕ0) → (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)) ∈ 𝐷)
134105, 132, 133syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)) ∈ 𝐷)
13592, 104, 93, 94, 3, 105, 106, 124, 125, 134mplmonmul 21437 . . . . . . . . . . . . . 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 21439 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)), 1 , 0 )) = ((𝑌𝑧) (𝑉𝑧)))
139138oveq2d 7373 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)(𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)), 1 , 0 ))) = ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)((𝑌𝑧) (𝑉𝑧))))
140132adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → (𝑌𝑧) ∈ ℕ0)
141 ifcl 4531 . . . . . . . . . . . . . . . . . . . 20 (((𝑌𝑧) ∈ ℕ0 ∧ 0 ∈ ℕ0) → if(𝑖 = 𝑧, (𝑌𝑧), 0) ∈ ℕ0)
142140, 109, 141sylancl 586 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → if(𝑖 = 𝑧, (𝑌𝑧), 0) ∈ ℕ0)
143 eqidd 2737 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)))
144 eqidd 2737 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)) = (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0)))
145105, 111, 142, 143, 144offval2 7637 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘f + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))) = (𝑖𝐼 ↦ (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0))))
146108adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (𝑌𝑖) ∈ ℕ0)
147146nn0cnd 12475 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (𝑌𝑖) ∈ ℂ)
148147addid2d 11356 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (0 + (𝑌𝑖)) = (𝑌𝑖))
149 elsni 4603 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ {𝑧} → 𝑖 = 𝑧)
150149adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → 𝑖 = 𝑧)
151 simprlr 778 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ¬ 𝑧𝑥)
152151ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → ¬ 𝑧𝑥)
153150, 152eqneltrd 2857 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → ¬ 𝑖𝑥)
154153iffalsed 4497 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → if(𝑖𝑥, (𝑌𝑖), 0) = 0)
155150iftrued 4494 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → if(𝑖 = 𝑧, (𝑌𝑧), 0) = (𝑌𝑧))
156150fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (𝑌𝑖) = (𝑌𝑧))
157155, 156eqtr4d 2779 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → if(𝑖 = 𝑧, (𝑌𝑧), 0) = (𝑌𝑖))
158154, 157oveq12d 7375 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = (0 + (𝑌𝑖)))
159 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → 𝑖 ∈ {𝑧})
160126, 159sselid 3942 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → 𝑖 ∈ (𝑥 ∪ {𝑧}))
161160iftrued 4494 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0) = (𝑌𝑖))
162148, 158, 1613eqtr4d 2786 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))
163111adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → if(𝑖𝑥, (𝑌𝑖), 0) ∈ ℕ0)
164163nn0cnd 12475 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → if(𝑖𝑥, (𝑌𝑖), 0) ∈ ℂ)
165164addid1d 11355 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + 0) = if(𝑖𝑥, (𝑌𝑖), 0))
166 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → ¬ 𝑖 ∈ {𝑧})
167 velsn 4602 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ {𝑧} ↔ 𝑖 = 𝑧)
168166, 167sylnib 327 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → ¬ 𝑖 = 𝑧)
169168iffalsed 4497 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → if(𝑖 = 𝑧, (𝑌𝑧), 0) = 0)
170169oveq2d 7373 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = (if(𝑖𝑥, (𝑌𝑖), 0) + 0))
171 elun 4108 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑖𝑥𝑖 ∈ {𝑧}))
172 orcom 868 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖𝑥𝑖 ∈ {𝑧}) ↔ (𝑖 ∈ {𝑧} ∨ 𝑖𝑥))
173171, 172bitri 274 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑖 ∈ {𝑧} ∨ 𝑖𝑥))
174 biorf 935 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑖 ∈ {𝑧} → (𝑖𝑥 ↔ (𝑖 ∈ {𝑧} ∨ 𝑖𝑥)))
175173, 174bitr4id 289 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖 ∈ {𝑧} → (𝑖 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑖𝑥))
176175adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → (𝑖 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑖𝑥))
177176ifbid 4509 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0) = if(𝑖𝑥, (𝑌𝑖), 0))
178165, 170, 1773eqtr4d 2786 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) ∧ ¬ 𝑖 ∈ {𝑧}) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))
179162, 178pm2.61dan 811 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑖𝐼) → (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0)) = if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))
180179mpteq2dva 5205 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑖𝐼 ↦ (if(𝑖𝑥, (𝑌𝑖), 0) + if(𝑖 = 𝑧, (𝑌𝑧), 0))) = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)))
181145, 180eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘f + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))) = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)))
182181eqeq2d 2747 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑦 = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘f + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))) ↔ 𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0))))
183182ifbid 4509 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → if(𝑦 = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘f + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))), 1 , 0 ) = if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 ))
184183mpteq2dv 5207 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑦𝐷 ↦ if(𝑦 = ((𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)) ∘f + (𝑖𝐼 ↦ if(𝑖 = 𝑧, (𝑌𝑧), 0))), 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )))
185135, 139, 1843eqtr3rd 2785 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)((𝑌𝑧) (𝑉𝑧))))
18648, 104mgpbas 19902 . . . . . . . . . . . . . 14 (Base‘𝑃) = (Base‘𝐺)
18748, 125mgpplusg 19900 . . . . . . . . . . . . . 14 (.r𝑃) = (+g𝐺)
188 eqid 2736 . . . . . . . . . . . . . 14 (Cntz‘𝐺) = (Cntz‘𝐺)
189 eqid 2736 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))) = (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))
19092mplring 21424 . . . . . . . . . . . . . . . . 17 ((𝐼𝑊𝑅 ∈ Ring) → 𝑃 ∈ Ring)
1912, 95, 190syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ Ring)
19248ringmgp 19970 . . . . . . . . . . . . . . . 16 (𝑃 ∈ Ring → 𝐺 ∈ Mnd)
193191, 192syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ Mnd)
194193adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝐺 ∈ Mnd)
1951adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑌𝐷)
196 mplcoe5.c . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑥𝐼𝑦𝐼 ((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑥)(+g𝐺)(𝑉𝑦)))
197 fveq2 6842 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑎 → (𝑉𝑥) = (𝑉𝑎))
198197oveq2d 7373 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → ((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑦)(+g𝐺)(𝑉𝑎)))
199197oveq1d 7372 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → ((𝑉𝑥)(+g𝐺)(𝑉𝑦)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑦)))
200198, 199eqeq12d 2752 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → (((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑥)(+g𝐺)(𝑉𝑦)) ↔ ((𝑉𝑦)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑦))))
201 fveq2 6842 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑏 → (𝑉𝑦) = (𝑉𝑏))
202201oveq1d 7372 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 → ((𝑉𝑦)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑏)(+g𝐺)(𝑉𝑎)))
203201oveq2d 7373 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 → ((𝑉𝑎)(+g𝐺)(𝑉𝑦)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏)))
204202, 203eqeq12d 2752 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 → (((𝑉𝑦)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑦)) ↔ ((𝑉𝑏)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏))))
205200, 204cbvral2vw 3227 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐼𝑦𝐼 ((𝑉𝑦)(+g𝐺)(𝑉𝑥)) = ((𝑉𝑥)(+g𝐺)(𝑉𝑦)) ↔ ∀𝑎𝐼𝑏𝐼 ((𝑉𝑏)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏)))
206196, 205sylib 217 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑎𝐼𝑏𝐼 ((𝑉𝑏)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏)))
207206adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ∀𝑎𝐼𝑏𝐼 ((𝑉𝑏)(+g𝐺)(𝑉𝑎)) = ((𝑉𝑎)(+g𝐺)(𝑉𝑏)))
20892, 3, 93, 94, 105, 48, 136, 137, 106, 195, 207, 127mplcoe5lem 21440 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ran (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))) ⊆ ((Cntz‘𝐺)‘ran (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))
20999, 127sstrid 3955 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → 𝑥𝐼)
210209sselda 3944 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑘𝑥) → 𝑘𝐼)
211193adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → 𝐺 ∈ Mnd)
2127ffvelcdmda 7035 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → (𝑌𝑘) ∈ ℕ0)
2132adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → 𝐼𝑊)
21495adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → 𝑅 ∈ Ring)
215 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → 𝑘𝐼)
21692, 137, 104, 213, 214, 215mvrcl 21421 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → (𝑉𝑘) ∈ (Base‘𝑃))
217186, 136, 211, 212, 216mulgnn0cld 18897 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐼) → ((𝑌𝑘) (𝑉𝑘)) ∈ (Base‘𝑃))
218217adantlr 713 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑘𝐼) → ((𝑌𝑘) (𝑉𝑘)) ∈ (Base‘𝑃))
219210, 218syldan 591 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑘𝑥) → ((𝑌𝑘) (𝑉𝑘)) ∈ (Base‘𝑃))
22092, 137, 104, 105, 106, 131mvrcl 21421 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝑉𝑧) ∈ (Base‘𝑃))
221186, 136, 194, 132, 220mulgnn0cld 18897 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑌𝑧) (𝑉𝑧)) ∈ (Base‘𝑃))
222 fveq2 6842 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑧 → (𝑌𝑘) = (𝑌𝑧))
223 fveq2 6842 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑧 → (𝑉𝑘) = (𝑉𝑧))
224222, 223oveq12d 7375 . . . . . . . . . . . . . . 15 (𝑘 = 𝑧 → ((𝑌𝑘) (𝑉𝑘)) = ((𝑌𝑧) (𝑉𝑧)))
225224adantl 482 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) ∧ 𝑘 = 𝑧) → ((𝑌𝑘) (𝑉𝑘)) = ((𝑌𝑧) (𝑉𝑧)))
226186, 187, 188, 189, 194, 115, 208, 219, 131, 151, 221, 225gsumzunsnd 19733 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))) = ((𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))(.r𝑃)((𝑌𝑧) (𝑉𝑧))))
227185, 226eqeq12d 2752 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))) ↔ ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 ))(.r𝑃)((𝑌𝑧) (𝑉𝑧))) = ((𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))(.r𝑃)((𝑌𝑧) (𝑉𝑧)))))
228103, 227syl5ibr 245 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐼)) → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))
229228expr 457 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧𝑥)) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → ((𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))) → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
230229a2d 29 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧𝑥)) → (((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
231102, 230syl5 34 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧𝑥)) → ((𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
232231expcom 414 . . . . . . 7 ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) → (𝜑 → ((𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘))))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))))
233232a2d 29 . . . . . 6 ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) → ((𝜑 → (𝑥𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖𝑥, (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝑥 ↦ ((𝑌𝑘) (𝑉𝑘)))))) → (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑥 ∪ {𝑧}), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑌𝑘) (𝑉𝑘))))))))
23455, 67, 79, 91, 98, 233findcard2s 9109 . . . . 5 ((𝑌 “ ℕ) ∈ Fin → (𝜑 → ((𝑌 “ ℕ) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))))
23532, 234mpcom 38 . . . 4 (𝜑 → ((𝑌 “ ℕ) ⊆ 𝐼 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))))
23631, 235mpd 15 . . 3 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))
23731resmptd 5994 . . . 4 (𝜑 → ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ↾ (𝑌 “ ℕ)) = (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘))))
238237oveq2d 7373 . . 3 (𝜑 → (𝐺 Σg ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ↾ (𝑌 “ ℕ))) = (𝐺 Σg (𝑘 ∈ (𝑌 “ ℕ) ↦ ((𝑌𝑘) (𝑉𝑘)))))
239217fmpttd 7063 . . . 4 (𝜑 → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))):𝐼⟶(Base‘𝑃))
240 ssidd 3967 . . . . 5 (𝜑𝐼𝐼)
24192, 3, 93, 94, 2, 48, 136, 137, 95, 1, 196, 240mplcoe5lem 21440 . . . 4 (𝜑 → ran (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ⊆ ((Cntz‘𝐺)‘ran (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
2427, 15, 2, 17suppssr 8127 . . . . . . 7 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → (𝑌𝑘) = 0)
243242oveq1d 7372 . . . . . 6 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → ((𝑌𝑘) (𝑉𝑘)) = (0 (𝑉𝑘)))
244 eldifi 4086 . . . . . . . 8 (𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ)) → 𝑘𝐼)
245244, 216sylan2 593 . . . . . . 7 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → (𝑉𝑘) ∈ (Base‘𝑃))
246186, 50, 136mulg0 18879 . . . . . . 7 ((𝑉𝑘) ∈ (Base‘𝑃) → (0 (𝑉𝑘)) = (1r𝑃))
247245, 246syl 17 . . . . . 6 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → (0 (𝑉𝑘)) = (1r𝑃))
248243, 247eqtrd 2776 . . . . 5 ((𝜑𝑘 ∈ (𝐼 ∖ (𝑌 “ ℕ))) → ((𝑌𝑘) (𝑉𝑘)) = (1r𝑃))
249248, 2suppss2 8131 . . . 4 (𝜑 → ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) supp (1r𝑃)) ⊆ (𝑌 “ ℕ))
2502mptexd 7174 . . . . 5 (𝜑 → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ∈ V)
251 funmpt 6539 . . . . . 6 Fun (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))
252251a1i 11 . . . . 5 (𝜑 → Fun (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))))
253 fvexd 6857 . . . . 5 (𝜑 → (1r𝑃) ∈ V)
254 suppssfifsupp 9320 . . . . 5 ((((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ∈ V ∧ Fun (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ∧ (1r𝑃) ∈ V) ∧ ((𝑌 “ ℕ) ∈ Fin ∧ ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) supp (1r𝑃)) ⊆ (𝑌 “ ℕ))) → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) finSupp (1r𝑃))
255250, 252, 253, 32, 249, 254syl32anc 1378 . . . 4 (𝜑 → (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) finSupp (1r𝑃))
256186, 50, 188, 193, 2, 239, 241, 249, 255gsumzres 19686 . . 3 (𝜑 → (𝐺 Σg ((𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘))) ↾ (𝑌 “ ℕ))) = (𝐺 Σg (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
257236, 238, 2563eqtr2d 2782 . 2 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = (𝑖𝐼 ↦ if(𝑖 ∈ (𝑌 “ ℕ), (𝑌𝑖), 0)), 1 , 0 )) = (𝐺 Σg (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
25829, 257eqtrd 2776 1 (𝜑 → (𝑦𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) = (𝐺 Σg (𝑘𝐼 ↦ ((𝑌𝑘) (𝑉𝑘)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  wral 3064  {crab 3407  Vcvv 3445  cdif 3907  cun 3908  wss 3910  c0 4282  ifcif 4486  {csn 4586   class class class wbr 5105  cmpt 5188   × cxp 5631  ccnv 5632  cres 5635  cima 5636  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357  f cof 7615   supp csupp 8092  m cmap 8765  Fincfn 8883   finSupp cfsupp 9305  0cc0 11051   + caddc 11054  cn 12153  0cn0 12413  Basecbs 17083  +gcplusg 17133  .rcmulr 17134  0gc0g 17321   Σg cgsu 17322  Mndcmnd 18556  .gcmg 18872  Cntzccntz 19095  mulGrpcmgp 19896  1rcur 19913  Ringcrg 19964   mVar cmvr 21307   mPoly cmpl 21308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-ofr 7618  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-sup 9378  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-fz 13425  df-fzo 13568  df-seq 13907  df-hash 14231  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-hom 17157  df-cco 17158  df-0g 17323  df-gsum 17324  df-prds 17329  df-pws 17331  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-mhm 18601  df-submnd 18602  df-grp 18751  df-minusg 18752  df-mulg 18873  df-subg 18925  df-ghm 19006  df-cntz 19097  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-srg 19918  df-ring 19966  df-subrg 20220  df-psr 21311  df-mvr 21312  df-mpl 21313
This theorem is referenced by:  mplcoe2  21442  ply1coe  21667
  Copyright terms: Public domain W3C validator