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

Theorem mplcoe1 19234
Description: Decompose a polynomial into a finite sum of monomials. (Contributed by Mario Carneiro, 9-Jan-2015.)
Hypotheses
Ref Expression
mplcoe1.p 𝑃 = (𝐼 mPoly 𝑅)
mplcoe1.d 𝐷 = {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
mplcoe1.z 0 = (0g𝑅)
mplcoe1.o 1 = (1r𝑅)
mplcoe1.i (𝜑𝐼𝑊)
mplcoe1.b 𝐵 = (Base‘𝑃)
mplcoe1.n · = ( ·𝑠𝑃)
mplcoe1.r (𝜑𝑅 ∈ Ring)
mplcoe1.x (𝜑𝑋𝐵)
Assertion
Ref Expression
mplcoe1 (𝜑𝑋 = (𝑃 Σg (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
Distinct variable groups:   𝑦,𝑘, 1   𝐵,𝑘   𝑓,𝑘,𝑦,𝐼   𝜑,𝑘,𝑦   𝑅,𝑓,𝑦   𝐷,𝑘,𝑦   𝑃,𝑘   0 ,𝑓,𝑘,𝑦   𝑓,𝑋,𝑘,𝑦   𝑘,𝑊,𝑦   · ,𝑘
Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑦,𝑓)   𝐷(𝑓)   𝑃(𝑦,𝑓)   𝑅(𝑘)   · (𝑦,𝑓)   1 (𝑓)   𝑊(𝑓)

Proof of Theorem mplcoe1
Dummy variables 𝑤 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplcoe1.p . . . . . 6 𝑃 = (𝐼 mPoly 𝑅)
2 eqid 2609 . . . . . 6 (Base‘𝑅) = (Base‘𝑅)
3 mplcoe1.b . . . . . 6 𝐵 = (Base‘𝑃)
4 mplcoe1.d . . . . . 6 𝐷 = {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
5 mplcoe1.x . . . . . 6 (𝜑𝑋𝐵)
61, 2, 3, 4, 5mplelf 19202 . . . . 5 (𝜑𝑋:𝐷⟶(Base‘𝑅))
76feqmptd 6143 . . . 4 (𝜑𝑋 = (𝑦𝐷 ↦ (𝑋𝑦)))
8 iftrue 4041 . . . . . . 7 (𝑦 ∈ (𝑋 supp 0 ) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 ) = (𝑋𝑦))
98adantl 480 . . . . . 6 (((𝜑𝑦𝐷) ∧ 𝑦 ∈ (𝑋 supp 0 )) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 ) = (𝑋𝑦))
10 eldif 3549 . . . . . . . 8 (𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ (𝑦𝐷 ∧ ¬ 𝑦 ∈ (𝑋 supp 0 )))
11 ifid 4074 . . . . . . . . 9 if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), (𝑋𝑦)) = (𝑋𝑦)
12 ssid 3586 . . . . . . . . . . . 12 (𝑋 supp 0 ) ⊆ (𝑋 supp 0 )
1312a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑋 supp 0 ) ⊆ (𝑋 supp 0 ))
14 ovex 6554 . . . . . . . . . . . . 13 (ℕ0𝑚 𝐼) ∈ V
154, 14rabex2 4736 . . . . . . . . . . . 12 𝐷 ∈ V
1615a1i 11 . . . . . . . . . . 11 (𝜑𝐷 ∈ V)
17 mplcoe1.z . . . . . . . . . . . . 13 0 = (0g𝑅)
18 fvex 6097 . . . . . . . . . . . . 13 (0g𝑅) ∈ V
1917, 18eqeltri 2683 . . . . . . . . . . . 12 0 ∈ V
2019a1i 11 . . . . . . . . . . 11 (𝜑0 ∈ V)
216, 13, 16, 20suppssr 7190 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋𝑦) = 0 )
2221ifeq2d 4054 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), (𝑋𝑦)) = if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 ))
2311, 22syl5reqr 2658 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 ) = (𝑋𝑦))
2410, 23sylan2br 491 . . . . . . 7 ((𝜑 ∧ (𝑦𝐷 ∧ ¬ 𝑦 ∈ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 ) = (𝑋𝑦))
2524anassrs 677 . . . . . 6 (((𝜑𝑦𝐷) ∧ ¬ 𝑦 ∈ (𝑋 supp 0 )) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 ) = (𝑋𝑦))
269, 25pm2.61dan 827 . . . . 5 ((𝜑𝑦𝐷) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 ) = (𝑋𝑦))
2726mpteq2dva 4666 . . . 4 (𝜑 → (𝑦𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 )) = (𝑦𝐷 ↦ (𝑋𝑦)))
287, 27eqtr4d 2646 . . 3 (𝜑𝑋 = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 )))
29 suppssdm 7172 . . . . 5 (𝑋 supp 0 ) ⊆ dom 𝑋
30 fdm 5949 . . . . . 6 (𝑋:𝐷⟶(Base‘𝑅) → dom 𝑋 = 𝐷)
316, 30syl 17 . . . . 5 (𝜑 → dom 𝑋 = 𝐷)
3229, 31syl5sseq 3615 . . . 4 (𝜑 → (𝑋 supp 0 ) ⊆ 𝐷)
33 eqid 2609 . . . . . . . . 9 (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
34 eqid 2609 . . . . . . . . 9 (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
351, 33, 34, 17, 3mplelbas 19199 . . . . . . . 8 (𝑋𝐵 ↔ (𝑋 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑋 finSupp 0 ))
3635simprbi 478 . . . . . . 7 (𝑋𝐵𝑋 finSupp 0 )
375, 36syl 17 . . . . . 6 (𝜑𝑋 finSupp 0 )
3837fsuppimpd 8142 . . . . 5 (𝜑 → (𝑋 supp 0 ) ∈ Fin)
39 sseq1 3588 . . . . . . . 8 (𝑤 = ∅ → (𝑤𝐷 ↔ ∅ ⊆ 𝐷))
40 mpteq1 4659 . . . . . . . . . . . 12 (𝑤 = ∅ → (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ ∅ ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
41 mpt0 5919 . . . . . . . . . . . 12 (𝑘 ∈ ∅ ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = ∅
4240, 41syl6eq 2659 . . . . . . . . . . 11 (𝑤 = ∅ → (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = ∅)
4342oveq2d 6542 . . . . . . . . . 10 (𝑤 = ∅ → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg ∅))
44 eqid 2609 . . . . . . . . . . 11 (0g𝑃) = (0g𝑃)
4544gsum0 17049 . . . . . . . . . 10 (𝑃 Σg ∅) = (0g𝑃)
4643, 45syl6eq 2659 . . . . . . . . 9 (𝑤 = ∅ → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (0g𝑃))
47 noel 3877 . . . . . . . . . . . 12 ¬ 𝑦 ∈ ∅
48 eleq2 2676 . . . . . . . . . . . 12 (𝑤 = ∅ → (𝑦𝑤𝑦 ∈ ∅))
4947, 48mtbiri 315 . . . . . . . . . . 11 (𝑤 = ∅ → ¬ 𝑦𝑤)
5049iffalsed 4046 . . . . . . . . . 10 (𝑤 = ∅ → if(𝑦𝑤, (𝑋𝑦), 0 ) = 0 )
5150mpteq2dv 4667 . . . . . . . . 9 (𝑤 = ∅ → (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 )) = (𝑦𝐷0 ))
5246, 51eqeq12d 2624 . . . . . . . 8 (𝑤 = ∅ → ((𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 )) ↔ (0g𝑃) = (𝑦𝐷0 )))
5339, 52imbi12d 332 . . . . . . 7 (𝑤 = ∅ → ((𝑤𝐷 → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 ))) ↔ (∅ ⊆ 𝐷 → (0g𝑃) = (𝑦𝐷0 ))))
5453imbi2d 328 . . . . . 6 (𝑤 = ∅ → ((𝜑 → (𝑤𝐷 → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 )))) ↔ (𝜑 → (∅ ⊆ 𝐷 → (0g𝑃) = (𝑦𝐷0 )))))
55 sseq1 3588 . . . . . . . 8 (𝑤 = 𝑥 → (𝑤𝐷𝑥𝐷))
56 mpteq1 4659 . . . . . . . . . 10 (𝑤 = 𝑥 → (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
5756oveq2d 6542 . . . . . . . . 9 (𝑤 = 𝑥 → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
58 eleq2 2676 . . . . . . . . . . 11 (𝑤 = 𝑥 → (𝑦𝑤𝑦𝑥))
5958ifbid 4057 . . . . . . . . . 10 (𝑤 = 𝑥 → if(𝑦𝑤, (𝑋𝑦), 0 ) = if(𝑦𝑥, (𝑋𝑦), 0 ))
6059mpteq2dv 4667 . . . . . . . . 9 (𝑤 = 𝑥 → (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 )) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )))
6157, 60eqeq12d 2624 . . . . . . . 8 (𝑤 = 𝑥 → ((𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 )) ↔ (𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))))
6255, 61imbi12d 332 . . . . . . 7 (𝑤 = 𝑥 → ((𝑤𝐷 → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 ))) ↔ (𝑥𝐷 → (𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )))))
6362imbi2d 328 . . . . . 6 (𝑤 = 𝑥 → ((𝜑 → (𝑤𝐷 → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 )))) ↔ (𝜑 → (𝑥𝐷 → (𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))))))
64 sseq1 3588 . . . . . . . 8 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑤𝐷 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐷))
65 mpteq1 4659 . . . . . . . . . 10 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
6665oveq2d 6542 . . . . . . . . 9 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
67 eleq2 2676 . . . . . . . . . . 11 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦𝑤𝑦 ∈ (𝑥 ∪ {𝑧})))
6867ifbid 4057 . . . . . . . . . 10 (𝑤 = (𝑥 ∪ {𝑧}) → if(𝑦𝑤, (𝑋𝑦), 0 ) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 ))
6968mpteq2dv 4667 . . . . . . . . 9 (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 )) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 )))
7066, 69eqeq12d 2624 . . . . . . . 8 (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 )) ↔ (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 ))))
7164, 70imbi12d 332 . . . . . . 7 (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑤𝐷 → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 ))) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 )))))
7271imbi2d 328 . . . . . 6 (𝑤 = (𝑥 ∪ {𝑧}) → ((𝜑 → (𝑤𝐷 → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 )))) ↔ (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 ))))))
73 sseq1 3588 . . . . . . . 8 (𝑤 = (𝑋 supp 0 ) → (𝑤𝐷 ↔ (𝑋 supp 0 ) ⊆ 𝐷))
74 mpteq1 4659 . . . . . . . . . 10 (𝑤 = (𝑋 supp 0 ) → (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
7574oveq2d 6542 . . . . . . . . 9 (𝑤 = (𝑋 supp 0 ) → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
76 eleq2 2676 . . . . . . . . . . 11 (𝑤 = (𝑋 supp 0 ) → (𝑦𝑤𝑦 ∈ (𝑋 supp 0 )))
7776ifbid 4057 . . . . . . . . . 10 (𝑤 = (𝑋 supp 0 ) → if(𝑦𝑤, (𝑋𝑦), 0 ) = if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 ))
7877mpteq2dv 4667 . . . . . . . . 9 (𝑤 = (𝑋 supp 0 ) → (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 )) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 )))
7975, 78eqeq12d 2624 . . . . . . . 8 (𝑤 = (𝑋 supp 0 ) → ((𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 )) ↔ (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 ))))
8073, 79imbi12d 332 . . . . . . 7 (𝑤 = (𝑋 supp 0 ) → ((𝑤𝐷 → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 ))) ↔ ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 )))))
8180imbi2d 328 . . . . . 6 (𝑤 = (𝑋 supp 0 ) → ((𝜑 → (𝑤𝐷 → (𝑃 Σg (𝑘𝑤 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑤, (𝑋𝑦), 0 )))) ↔ (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 ))))))
82 mplcoe1.i . . . . . . . . 9 (𝜑𝐼𝑊)
83 mplcoe1.r . . . . . . . . . 10 (𝜑𝑅 ∈ Ring)
84 ringgrp 18323 . . . . . . . . . 10 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
8583, 84syl 17 . . . . . . . . 9 (𝜑𝑅 ∈ Grp)
861, 4, 17, 44, 82, 85mpl0 19210 . . . . . . . 8 (𝜑 → (0g𝑃) = (𝐷 × { 0 }))
87 fconstmpt 5074 . . . . . . . 8 (𝐷 × { 0 }) = (𝑦𝐷0 )
8886, 87syl6eq 2659 . . . . . . 7 (𝜑 → (0g𝑃) = (𝑦𝐷0 ))
8988a1d 25 . . . . . 6 (𝜑 → (∅ ⊆ 𝐷 → (0g𝑃) = (𝑦𝐷0 )))
90 ssun1 3737 . . . . . . . . . . 11 𝑥 ⊆ (𝑥 ∪ {𝑧})
91 sstr2 3574 . . . . . . . . . . 11 (𝑥 ⊆ (𝑥 ∪ {𝑧}) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷𝑥𝐷))
9290, 91ax-mp 5 . . . . . . . . . 10 ((𝑥 ∪ {𝑧}) ⊆ 𝐷𝑥𝐷)
9392imim1i 60 . . . . . . . . 9 ((𝑥𝐷 → (𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))))
94 oveq1 6533 . . . . . . . . . . . 12 ((𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) → ((𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))(+g𝑃)((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))(+g𝑃)((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))
95 eqid 2609 . . . . . . . . . . . . . 14 (+g𝑃) = (+g𝑃)
961mplring 19221 . . . . . . . . . . . . . . . . 17 ((𝐼𝑊𝑅 ∈ Ring) → 𝑃 ∈ Ring)
9782, 83, 96syl2anc 690 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ Ring)
98 ringcmn 18352 . . . . . . . . . . . . . . . 16 (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
9997, 98syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ CMnd)
10099adantr 479 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑃 ∈ CMnd)
101 simprll 797 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑥 ∈ Fin)
102 simprr 791 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑥 ∪ {𝑧}) ⊆ 𝐷)
103102unssad 3751 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑥𝐷)
104103sselda 3567 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘𝑥) → 𝑘𝐷)
10582adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐷) → 𝐼𝑊)
10683adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐷) → 𝑅 ∈ Ring)
1071mpllmod 19220 . . . . . . . . . . . . . . . . . 18 ((𝐼𝑊𝑅 ∈ Ring) → 𝑃 ∈ LMod)
108105, 106, 107syl2anc 690 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐷) → 𝑃 ∈ LMod)
1096ffvelrnda 6251 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐷) → (𝑋𝑘) ∈ (Base‘𝑅))
1101, 82, 83mplsca 19214 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑅 = (Scalar‘𝑃))
111110adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝐷) → 𝑅 = (Scalar‘𝑃))
112111fveq2d 6091 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐷) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
113109, 112eleqtrd 2689 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐷) → (𝑋𝑘) ∈ (Base‘(Scalar‘𝑃)))
114 mplcoe1.o . . . . . . . . . . . . . . . . . 18 1 = (1r𝑅)
115 simpr 475 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐷) → 𝑘𝐷)
1161, 3, 17, 114, 4, 105, 106, 115mplmon 19232 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐷) → (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵)
117 eqid 2609 . . . . . . . . . . . . . . . . . 18 (Scalar‘𝑃) = (Scalar‘𝑃)
118 mplcoe1.n . . . . . . . . . . . . . . . . . 18 · = ( ·𝑠𝑃)
119 eqid 2609 . . . . . . . . . . . . . . . . . 18 (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
1203, 117, 118, 119lmodvscl 18651 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ LMod ∧ (𝑋𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵) → ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵)
121108, 113, 116, 120syl3anc 1317 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐷) → ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵)
122121adantlr 746 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘𝐷) → ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵)
123104, 122syldan 485 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘𝑥) → ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵)
124 vex 3175 . . . . . . . . . . . . . . 15 𝑧 ∈ V
125124a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑧 ∈ V)
126 simprlr 798 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ¬ 𝑧𝑥)
12782, 83, 107syl2anc 690 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ LMod)
128127adantr 479 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑃 ∈ LMod)
1296adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑋:𝐷⟶(Base‘𝑅))
130102unssbd 3752 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → {𝑧} ⊆ 𝐷)
131124snss 4258 . . . . . . . . . . . . . . . . . 18 (𝑧𝐷 ↔ {𝑧} ⊆ 𝐷)
132130, 131sylibr 222 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑧𝐷)
133129, 132ffvelrnd 6252 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑋𝑧) ∈ (Base‘𝑅))
134110adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 = (Scalar‘𝑃))
135134fveq2d 6091 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
136133, 135eleqtrd 2689 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑋𝑧) ∈ (Base‘(Scalar‘𝑃)))
13782adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝐼𝑊)
13883adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 ∈ Ring)
1391, 3, 17, 114, 4, 137, 138, 132mplmon 19232 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) ∈ 𝐵)
1403, 117, 118, 119lmodvscl 18651 . . . . . . . . . . . . . . 15 ((𝑃 ∈ LMod ∧ (𝑋𝑧) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) ∈ 𝐵) → ((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) ∈ 𝐵)
141128, 136, 139, 140syl3anc 1317 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) ∈ 𝐵)
142 fveq2 6087 . . . . . . . . . . . . . . 15 (𝑘 = 𝑧 → (𝑋𝑘) = (𝑋𝑧))
143 equequ2 1939 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑧 → (𝑦 = 𝑘𝑦 = 𝑧))
144143ifbid 4057 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑧 → if(𝑦 = 𝑘, 1 , 0 ) = if(𝑦 = 𝑧, 1 , 0 ))
145144mpteq2dv 4667 . . . . . . . . . . . . . . 15 (𝑘 = 𝑧 → (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))
146142, 145oveq12d 6544 . . . . . . . . . . . . . 14 (𝑘 = 𝑧 → ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))
1473, 95, 100, 101, 123, 125, 126, 141, 146gsumunsn 18130 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = ((𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))(+g𝑃)((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))
148 eqid 2609 . . . . . . . . . . . . . . 15 (+g𝑅) = (+g𝑅)
149129ffvelrnda 6251 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) → (𝑋𝑦) ∈ (Base‘𝑅))
1502, 17ring0cl 18340 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ Ring → 0 ∈ (Base‘𝑅))
15183, 150syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑0 ∈ (Base‘𝑅))
152151ad2antrr 757 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) → 0 ∈ (Base‘𝑅))
153149, 152ifcld 4080 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) → if(𝑦𝑥, (𝑋𝑦), 0 ) ∈ (Base‘𝑅))
154 eqid 2609 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))
155153, 154fmptd 6276 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )):𝐷⟶(Base‘𝑅))
156 fvex 6097 . . . . . . . . . . . . . . . . . . 19 (Base‘𝑅) ∈ V
157156, 15elmap 7749 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∈ ((Base‘𝑅) ↑𝑚 𝐷) ↔ (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )):𝐷⟶(Base‘𝑅))
158155, 157sylibr 222 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∈ ((Base‘𝑅) ↑𝑚 𝐷))
15933, 2, 4, 34, 137psrbas 19147 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (Base‘(𝐼 mPwSer 𝑅)) = ((Base‘𝑅) ↑𝑚 𝐷))
160158, 159eleqtrrd 2690 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∈ (Base‘(𝐼 mPwSer 𝑅)))
16115mptex 6367 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∈ V
162 funmpt 5825 . . . . . . . . . . . . . . . . . . 19 Fun (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))
163161, 162, 193pm3.2i 1231 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∈ V ∧ Fun (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∧ 0 ∈ V)
164163a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∈ V ∧ Fun (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∧ 0 ∈ V))
165 eldifn 3694 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐷𝑥) → ¬ 𝑦𝑥)
166165adantl 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ (𝐷𝑥)) → ¬ 𝑦𝑥)
167166iffalsed 4046 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ (𝐷𝑥)) → if(𝑦𝑥, (𝑋𝑦), 0 ) = 0 )
16815a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝐷 ∈ V)
169167, 168suppss2 7193 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) supp 0 ) ⊆ 𝑥)
170 suppssfifsupp 8150 . . . . . . . . . . . . . . . . 17 ((((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∈ V ∧ Fun (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∧ 0 ∈ V) ∧ (𝑥 ∈ Fin ∧ ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) supp 0 ) ⊆ 𝑥)) → (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) finSupp 0 )
171164, 101, 169, 170syl12anc 1315 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) finSupp 0 )
1721, 33, 34, 17, 3mplelbas 19199 . . . . . . . . . . . . . . . 16 ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∈ 𝐵 ↔ ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) finSupp 0 ))
173160, 171, 172sylanbrc 694 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∈ 𝐵)
1741, 3, 148, 95, 173, 141mpladd 19211 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))(+g𝑃)((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∘𝑓 (+g𝑅)((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))
175 ovex 6554 . . . . . . . . . . . . . . . 16 ((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 )) ∈ V
176175a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) → ((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 )) ∈ V)
177 eqidd 2610 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )))
178 eqid 2609 . . . . . . . . . . . . . . . . 17 (.r𝑅) = (.r𝑅)
1791, 118, 2, 3, 178, 4, 133, 139mplvsca 19216 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = ((𝐷 × {(𝑋𝑧)}) ∘𝑓 (.r𝑅)(𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))
180133adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) → (𝑋𝑧) ∈ (Base‘𝑅))
1812, 114ringidcl 18339 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∈ Ring → 1 ∈ (Base‘𝑅))
182181, 150ifcld 4080 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ Ring → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅))
18383, 182syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅))
184183ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅))
185 fconstmpt 5074 . . . . . . . . . . . . . . . . . 18 (𝐷 × {(𝑋𝑧)}) = (𝑦𝐷 ↦ (𝑋𝑧))
186185a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝐷 × {(𝑋𝑧)}) = (𝑦𝐷 ↦ (𝑋𝑧)))
187 eqidd 2610 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) = (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))
188168, 180, 184, 186, 187offval2 6789 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝐷 × {(𝑋𝑧)}) ∘𝑓 (.r𝑅)(𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = (𝑦𝐷 ↦ ((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 ))))
189179, 188eqtrd 2643 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = (𝑦𝐷 ↦ ((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 ))))
190168, 153, 176, 177, 189offval2 6789 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) ∘𝑓 (+g𝑅)((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = (𝑦𝐷 ↦ (if(𝑦𝑥, (𝑋𝑦), 0 )(+g𝑅)((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 )))))
191138, 84syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 ∈ Grp)
1922, 148, 17grplid 17223 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ Grp ∧ (𝑋𝑧) ∈ (Base‘𝑅)) → ( 0 (+g𝑅)(𝑋𝑧)) = (𝑋𝑧))
193191, 133, 192syl2anc 690 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ( 0 (+g𝑅)(𝑋𝑧)) = (𝑋𝑧))
194193ad2antrr 757 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → ( 0 (+g𝑅)(𝑋𝑧)) = (𝑋𝑧))
195 simpr 475 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 ∈ {𝑧})
196 velsn 4140 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ {𝑧} ↔ 𝑦 = 𝑧)
197195, 196sylib 206 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 = 𝑧)
198197fveq2d 6091 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → (𝑋𝑦) = (𝑋𝑧))
199194, 198eqtr4d 2646 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → ( 0 (+g𝑅)(𝑋𝑧)) = (𝑋𝑦))
200126ad2antrr 757 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → ¬ 𝑧𝑥)
201197, 200eqneltrd 2706 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → ¬ 𝑦𝑥)
202201iffalsed 4046 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦𝑥, (𝑋𝑦), 0 ) = 0 )
203197iftrued 4043 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 = 𝑧, 1 , 0 ) = 1 )
204203oveq2d 6542 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 )) = ((𝑋𝑧)(.r𝑅) 1 ))
2052, 178, 114ringridm 18343 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ Ring ∧ (𝑋𝑧) ∈ (Base‘𝑅)) → ((𝑋𝑧)(.r𝑅) 1 ) = (𝑋𝑧))
206138, 133, 205syl2anc 690 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋𝑧)(.r𝑅) 1 ) = (𝑋𝑧))
207206ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋𝑧)(.r𝑅) 1 ) = (𝑋𝑧))
208204, 207eqtrd 2643 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 )) = (𝑋𝑧))
209202, 208oveq12d 6544 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → (if(𝑦𝑥, (𝑋𝑦), 0 )(+g𝑅)((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = ( 0 (+g𝑅)(𝑋𝑧)))
210 elun2 3742 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ {𝑧} → 𝑦 ∈ (𝑥 ∪ {𝑧}))
211210adantl 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 ∈ (𝑥 ∪ {𝑧}))
212211iftrued 4043 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 ) = (𝑋𝑦))
213199, 209, 2123eqtr4d 2653 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ {𝑧}) → (if(𝑦𝑥, (𝑋𝑦), 0 )(+g𝑅)((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 ))
21485ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) → 𝑅 ∈ Grp)
2152, 148, 17grprid 17224 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ Grp ∧ if(𝑦𝑥, (𝑋𝑦), 0 ) ∈ (Base‘𝑅)) → (if(𝑦𝑥, (𝑋𝑦), 0 )(+g𝑅) 0 ) = if(𝑦𝑥, (𝑋𝑦), 0 ))
216214, 153, 215syl2anc 690 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) → (if(𝑦𝑥, (𝑋𝑦), 0 )(+g𝑅) 0 ) = if(𝑦𝑥, (𝑋𝑦), 0 ))
217216adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦𝑥, (𝑋𝑦), 0 )(+g𝑅) 0 ) = if(𝑦𝑥, (𝑋𝑦), 0 ))
218 simpr 475 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ¬ 𝑦 ∈ {𝑧})
219218, 196sylnib 316 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ¬ 𝑦 = 𝑧)
220219iffalsed 4046 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → if(𝑦 = 𝑧, 1 , 0 ) = 0 )
221220oveq2d 6542 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 )) = ((𝑋𝑧)(.r𝑅) 0 ))
2222, 178, 17ringrz 18359 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ Ring ∧ (𝑋𝑧) ∈ (Base‘𝑅)) → ((𝑋𝑧)(.r𝑅) 0 ) = 0 )
223138, 133, 222syl2anc 690 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋𝑧)(.r𝑅) 0 ) = 0 )
224223ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋𝑧)(.r𝑅) 0 ) = 0 )
225221, 224eqtrd 2643 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 )) = 0 )
226225oveq2d 6542 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦𝑥, (𝑋𝑦), 0 )(+g𝑅)((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = (if(𝑦𝑥, (𝑋𝑦), 0 )(+g𝑅) 0 ))
227 biorf 418 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ {𝑧} → (𝑦𝑥 ↔ (𝑦 ∈ {𝑧} ∨ 𝑦𝑥)))
228 elun 3714 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑦𝑥𝑦 ∈ {𝑧}))
229 orcom 400 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑥𝑦 ∈ {𝑧}) ↔ (𝑦 ∈ {𝑧} ∨ 𝑦𝑥))
230228, 229bitri 262 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑦 ∈ {𝑧} ∨ 𝑦𝑥))
231227, 230syl6rbbr 277 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ {𝑧} → (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑦𝑥))
232231adantl 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑦𝑥))
233232ifbid 4057 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 ) = if(𝑦𝑥, (𝑋𝑦), 0 ))
234217, 226, 2333eqtr4d 2653 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦𝑥, (𝑋𝑦), 0 )(+g𝑅)((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 ))
235213, 234pm2.61dan 827 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦𝐷) → (if(𝑦𝑥, (𝑋𝑦), 0 )(+g𝑅)((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 ))
236235mpteq2dva 4666 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦𝐷 ↦ (if(𝑦𝑥, (𝑋𝑦), 0 )(+g𝑅)((𝑋𝑧)(.r𝑅)if(𝑦 = 𝑧, 1 , 0 )))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 )))
237174, 190, 2363eqtrrd 2648 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 )) = ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))(+g𝑃)((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))
238147, 237eqeq12d 2624 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 )) ↔ ((𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))(+g𝑃)((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))(+g𝑃)((𝑋𝑧) · (𝑦𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))))
23994, 238syl5ibr 234 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 ))))
240239expr 640 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧𝑥)) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → ((𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )) → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 )))))
241240a2d 29 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧𝑥)) → (((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 )))))
24293, 241syl5 33 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧𝑥)) → ((𝑥𝐷 → (𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 )))))
243242expcom 449 . . . . . . 7 ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) → (𝜑 → ((𝑥𝐷 → (𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 ))))))
244243a2d 29 . . . . . 6 ((𝑥 ∈ Fin ∧ ¬ 𝑧𝑥) → ((𝜑 → (𝑥𝐷 → (𝑃 Σg (𝑘𝑥 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦𝑥, (𝑋𝑦), 0 )))) → (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋𝑦), 0 ))))))
24554, 63, 72, 81, 89, 244findcard2s 8063 . . . . 5 ((𝑋 supp 0 ) ∈ Fin → (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 )))))
24638, 245mpcom 37 . . . 4 (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 ))))
24732, 246mpd 15 . . 3 (𝜑 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋𝑦), 0 )))
24828, 247eqtr4d 2646 . 2 (𝜑𝑋 = (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
24932resmptd 5357 . . . 4 (𝜑 → ((𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 )) = (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
250249oveq2d 6542 . . 3 (𝜑 → (𝑃 Σg ((𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 ))) = (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
251 eqid 2609 . . . . 5 (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))
252121, 251fmptd 6276 . . . 4 (𝜑 → (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))):𝐷𝐵)
2536, 13, 16, 20suppssr 7190 . . . . . . 7 ((𝜑𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋𝑘) = 0 )
254253oveq1d 6541 . . . . . 6 ((𝜑𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ( 0 · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))
255 eldifi 3693 . . . . . . 7 (𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 )) → 𝑘𝐷)
256111fveq2d 6091 . . . . . . . . . 10 ((𝜑𝑘𝐷) → (0g𝑅) = (0g‘(Scalar‘𝑃)))
25717, 256syl5eq 2655 . . . . . . . . 9 ((𝜑𝑘𝐷) → 0 = (0g‘(Scalar‘𝑃)))
258257oveq1d 6541 . . . . . . . 8 ((𝜑𝑘𝐷) → ( 0 · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ((0g‘(Scalar‘𝑃)) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))
259 eqid 2609 . . . . . . . . . 10 (0g‘(Scalar‘𝑃)) = (0g‘(Scalar‘𝑃))
2603, 117, 118, 259, 44lmod0vs 18667 . . . . . . . . 9 ((𝑃 ∈ LMod ∧ (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵) → ((0g‘(Scalar‘𝑃)) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0g𝑃))
261108, 116, 260syl2anc 690 . . . . . . . 8 ((𝜑𝑘𝐷) → ((0g‘(Scalar‘𝑃)) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0g𝑃))
262258, 261eqtrd 2643 . . . . . . 7 ((𝜑𝑘𝐷) → ( 0 · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0g𝑃))
263255, 262sylan2 489 . . . . . 6 ((𝜑𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ( 0 · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0g𝑃))
264254, 263eqtrd 2643 . . . . 5 ((𝜑𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0g𝑃))
265264, 16suppss2 7193 . . . 4 (𝜑 → ((𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) supp (0g𝑃)) ⊆ (𝑋 supp 0 ))
26615mptex 6367 . . . . . . 7 (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V
267 funmpt 5825 . . . . . . 7 Fun (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))
268 fvex 6097 . . . . . . 7 (0g𝑃) ∈ V
269266, 267, 2683pm3.2i 1231 . . . . . 6 ((𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V ∧ Fun (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∧ (0g𝑃) ∈ V)
270269a1i 11 . . . . 5 (𝜑 → ((𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V ∧ Fun (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∧ (0g𝑃) ∈ V))
271 suppssfifsupp 8150 . . . . 5 ((((𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V ∧ Fun (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∧ (0g𝑃) ∈ V) ∧ ((𝑋 supp 0 ) ∈ Fin ∧ ((𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) supp (0g𝑃)) ⊆ (𝑋 supp 0 ))) → (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) finSupp (0g𝑃))
272270, 38, 265, 271syl12anc 1315 . . . 4 (𝜑 → (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) finSupp (0g𝑃))
2733, 44, 99, 16, 252, 265, 272gsumres 18085 . . 3 (𝜑 → (𝑃 Σg ((𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 ))) = (𝑃 Σg (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
274250, 273eqtr3d 2645 . 2 (𝜑 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
275248, 274eqtrd 2643 1 (𝜑𝑋 = (𝑃 Σg (𝑘𝐷 ↦ ((𝑋𝑘) · (𝑦𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1976  {crab 2899  Vcvv 3172  cdif 3536  cun 3537  wss 3539  c0 3873  ifcif 4035  {csn 4124   class class class wbr 4577  cmpt 4637   × cxp 5025  ccnv 5026  dom cdm 5027  cres 5029  cima 5030  Fun wfun 5783  wf 5785  cfv 5789  (class class class)co 6526  𝑓 cof 6770   supp csupp 7159  𝑚 cmap 7721  Fincfn 7818   finSupp cfsupp 8135  cn 10869  0cn0 11141  Basecbs 15643  +gcplusg 15716  .rcmulr 15717  Scalarcsca 15719   ·𝑠 cvsca 15720  0gc0g 15871   Σg cgsu 15872  Grpcgrp 17193  CMndccmn 17964  1rcur 18272  Ringcrg 18318  LModclmod 18634   mPwSer cmps 19120   mPoly cmpl 19122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-se 4987  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-isom 5798  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-of 6772  df-ofr 6773  df-om 6935  df-1st 7036  df-2nd 7037  df-supp 7160  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fsupp 8136  df-oi 8275  df-card 8625  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10870  df-2 10928  df-3 10929  df-4 10930  df-5 10931  df-6 10932  df-7 10933  df-8 10934  df-9 10935  df-n0 11142  df-z 11213  df-uz 11522  df-fz 12155  df-fzo 12292  df-seq 12621  df-hash 12937  df-struct 15645  df-ndx 15646  df-slot 15647  df-base 15648  df-sets 15649  df-ress 15650  df-plusg 15729  df-mulr 15730  df-sca 15732  df-vsca 15733  df-tset 15735  df-0g 15873  df-gsum 15874  df-mre 16017  df-mrc 16018  df-acs 16020  df-mgm 17013  df-sgrp 17055  df-mnd 17066  df-mhm 17106  df-submnd 17107  df-grp 17196  df-minusg 17197  df-sbg 17198  df-mulg 17312  df-subg 17362  df-ghm 17429  df-cntz 17521  df-cmn 17966  df-abl 17967  df-mgp 18261  df-ur 18273  df-ring 18320  df-subrg 18549  df-lmod 18636  df-lss 18702  df-psr 19125  df-mpl 19127
This theorem is referenced by:  mplbas2  19239  mplcoe4  19272  ply1coe  19435
  Copyright terms: Public domain W3C validator