| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mplcoe1.p | . . . . . 6
⊢ 𝑃 = (𝐼 mPoly 𝑅) | 
| 2 |  | eqid 2736 | . . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 3 |  | mplcoe1.b | . . . . . 6
⊢ 𝐵 = (Base‘𝑃) | 
| 4 |  | mplcoe1.d | . . . . . 6
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} | 
| 5 |  | mplcoe1.x | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 6 | 1, 2, 3, 4, 5 | mplelf 22019 | . . . . 5
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) | 
| 7 | 6 | feqmptd 6976 | . . . 4
⊢ (𝜑 → 𝑋 = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑦))) | 
| 8 |  | iftrue 4530 | . . . . . . 7
⊢ (𝑦 ∈ (𝑋 supp 0 ) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) | 
| 9 | 8 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝑋 supp 0 )) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) | 
| 10 |  | eldif 3960 | . . . . . . . 8
⊢ (𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ (𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ (𝑋 supp 0 ))) | 
| 11 |  | ssidd 4006 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑋 supp 0 ) ⊆ (𝑋 supp 0 )) | 
| 12 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢
(ℕ0 ↑m 𝐼) ∈ V | 
| 13 | 4, 12 | rabex2 5340 | . . . . . . . . . . . 12
⊢ 𝐷 ∈ V | 
| 14 | 13 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ V) | 
| 15 |  | mplcoe1.z | . . . . . . . . . . . . 13
⊢  0 =
(0g‘𝑅) | 
| 16 | 15 | fvexi 6919 | . . . . . . . . . . . 12
⊢  0 ∈
V | 
| 17 | 16 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ V) | 
| 18 | 6, 11, 14, 17 | suppssr 8221 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋‘𝑦) = 0 ) | 
| 19 | 18 | ifeq2d 4545 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), (𝑋‘𝑦)) = if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )) | 
| 20 |  | ifid 4565 | . . . . . . . . 9
⊢ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), (𝑋‘𝑦)) = (𝑋‘𝑦) | 
| 21 | 19, 20 | eqtr3di 2791 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) | 
| 22 | 10, 21 | sylan2br 595 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) | 
| 23 | 22 | anassrs 467 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ (𝑋 supp 0 )) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) | 
| 24 | 9, 23 | pm2.61dan 812 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) | 
| 25 | 24 | mpteq2dva 5241 | . . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑦))) | 
| 26 | 7, 25 | eqtr4d 2779 | . . 3
⊢ (𝜑 → 𝑋 = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))) | 
| 27 |  | suppssdm 8203 | . . . . 5
⊢ (𝑋 supp 0 ) ⊆ dom 𝑋 | 
| 28 | 27, 6 | fssdm 6754 | . . . 4
⊢ (𝜑 → (𝑋 supp 0 ) ⊆ 𝐷) | 
| 29 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) | 
| 30 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) | 
| 31 | 1, 29, 30, 15, 3 | mplelbas 22012 | . . . . . . . 8
⊢ (𝑋 ∈ 𝐵 ↔ (𝑋 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑋 finSupp 0 )) | 
| 32 | 31 | simprbi 496 | . . . . . . 7
⊢ (𝑋 ∈ 𝐵 → 𝑋 finSupp 0 ) | 
| 33 | 5, 32 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑋 finSupp 0 ) | 
| 34 | 33 | fsuppimpd 9410 | . . . . 5
⊢ (𝜑 → (𝑋 supp 0 ) ∈
Fin) | 
| 35 |  | sseq1 4008 | . . . . . . . 8
⊢ (𝑤 = ∅ → (𝑤 ⊆ 𝐷 ↔ ∅ ⊆ 𝐷)) | 
| 36 |  | mpteq1 5234 | . . . . . . . . . . . 12
⊢ (𝑤 = ∅ → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ ∅ ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) | 
| 37 |  | mpt0 6709 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ∅ ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) =
∅ | 
| 38 | 36, 37 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝑤 = ∅ → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) =
∅) | 
| 39 | 38 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑤 = ∅ → (𝑃 Σg
(𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg
∅)) | 
| 40 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(0g‘𝑃) = (0g‘𝑃) | 
| 41 | 40 | gsum0 18698 | . . . . . . . . . 10
⊢ (𝑃 Σg
∅) = (0g‘𝑃) | 
| 42 | 39, 41 | eqtrdi 2792 | . . . . . . . . 9
⊢ (𝑤 = ∅ → (𝑃 Σg
(𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) =
(0g‘𝑃)) | 
| 43 |  | noel 4337 | . . . . . . . . . . . 12
⊢  ¬
𝑦 ∈
∅ | 
| 44 |  | eleq2 2829 | . . . . . . . . . . . 12
⊢ (𝑤 = ∅ → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ∅)) | 
| 45 | 43, 44 | mtbiri 327 | . . . . . . . . . . 11
⊢ (𝑤 = ∅ → ¬ 𝑦 ∈ 𝑤) | 
| 46 | 45 | iffalsed 4535 | . . . . . . . . . 10
⊢ (𝑤 = ∅ → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = 0 ) | 
| 47 | 46 | mpteq2dv 5243 | . . . . . . . . 9
⊢ (𝑤 = ∅ → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ 0 )) | 
| 48 | 42, 47 | eqeq12d 2752 | . . . . . . . 8
⊢ (𝑤 = ∅ → ((𝑃 Σg
(𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔
(0g‘𝑃) =
(𝑦 ∈ 𝐷 ↦ 0 ))) | 
| 49 | 35, 48 | imbi12d 344 | . . . . . . 7
⊢ (𝑤 = ∅ → ((𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ (∅
⊆ 𝐷 →
(0g‘𝑃) =
(𝑦 ∈ 𝐷 ↦ 0 )))) | 
| 50 | 49 | imbi2d 340 | . . . . . 6
⊢ (𝑤 = ∅ → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → (∅ ⊆ 𝐷 →
(0g‘𝑃) =
(𝑦 ∈ 𝐷 ↦ 0 ))))) | 
| 51 |  | sseq1 4008 | . . . . . . . 8
⊢ (𝑤 = 𝑥 → (𝑤 ⊆ 𝐷 ↔ 𝑥 ⊆ 𝐷)) | 
| 52 |  | mpteq1 5234 | . . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) | 
| 53 | 52 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) | 
| 54 |  | eleq2 2829 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥)) | 
| 55 | 54 | ifbid 4548 | . . . . . . . . . 10
⊢ (𝑤 = 𝑥 → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) | 
| 56 | 55 | mpteq2dv 5243 | . . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) | 
| 57 | 53, 56 | eqeq12d 2752 | . . . . . . . 8
⊢ (𝑤 = 𝑥 → ((𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (𝑃 Σg
(𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))) | 
| 58 | 51, 57 | imbi12d 344 | . . . . . . 7
⊢ (𝑤 = 𝑥 → ((𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ (𝑥 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))))) | 
| 59 | 58 | imbi2d 340 | . . . . . 6
⊢ (𝑤 = 𝑥 → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → (𝑥 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))))) | 
| 60 |  | sseq1 4008 | . . . . . . . 8
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑤 ⊆ 𝐷 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) | 
| 61 |  | mpteq1 5234 | . . . . . . . . . 10
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) | 
| 62 | 61 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) | 
| 63 |  | eleq2 2829 | . . . . . . . . . . 11
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ (𝑥 ∪ {𝑧}))) | 
| 64 | 63 | ifbid 4548 | . . . . . . . . . 10
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) | 
| 65 | 64 | mpteq2dv 5243 | . . . . . . . . 9
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))) | 
| 66 | 62, 65 | eqeq12d 2752 | . . . . . . . 8
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (𝑃 Σg
(𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))) | 
| 67 | 60, 66 | imbi12d 344 | . . . . . . 7
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))) | 
| 68 | 67 | imbi2d 340 | . . . . . 6
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))) | 
| 69 |  | sseq1 4008 | . . . . . . . 8
⊢ (𝑤 = (𝑋 supp 0 ) → (𝑤 ⊆ 𝐷 ↔ (𝑋 supp 0 ) ⊆ 𝐷)) | 
| 70 |  | mpteq1 5234 | . . . . . . . . . 10
⊢ (𝑤 = (𝑋 supp 0 ) → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) | 
| 71 | 70 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑤 = (𝑋 supp 0 ) → (𝑃 Σg
(𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) | 
| 72 |  | eleq2 2829 | . . . . . . . . . . 11
⊢ (𝑤 = (𝑋 supp 0 ) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ (𝑋 supp 0 ))) | 
| 73 | 72 | ifbid 4548 | . . . . . . . . . 10
⊢ (𝑤 = (𝑋 supp 0 ) → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )) | 
| 74 | 73 | mpteq2dv 5243 | . . . . . . . . 9
⊢ (𝑤 = (𝑋 supp 0 ) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))) | 
| 75 | 71, 74 | eqeq12d 2752 | . . . . . . . 8
⊢ (𝑤 = (𝑋 supp 0 ) → ((𝑃 Σg
(𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (𝑃 Σg
(𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))) | 
| 76 | 69, 75 | imbi12d 344 | . . . . . . 7
⊢ (𝑤 = (𝑋 supp 0 ) → ((𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))))) | 
| 77 | 76 | imbi2d 340 | . . . . . 6
⊢ (𝑤 = (𝑋 supp 0 ) → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))))) | 
| 78 |  | mplcoe1.i | . . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑊) | 
| 79 |  | mplcoe1.r | . . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 80 |  | ringgrp 20236 | . . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | 
| 81 | 79, 80 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Grp) | 
| 82 | 1, 4, 15, 40, 78, 81 | mpl0 22027 | . . . . . . . 8
⊢ (𝜑 → (0g‘𝑃) = (𝐷 × { 0 })) | 
| 83 |  | fconstmpt 5746 | . . . . . . . 8
⊢ (𝐷 × { 0 }) = (𝑦 ∈ 𝐷 ↦ 0 ) | 
| 84 | 82, 83 | eqtrdi 2792 | . . . . . . 7
⊢ (𝜑 → (0g‘𝑃) = (𝑦 ∈ 𝐷 ↦ 0 )) | 
| 85 | 84 | a1d 25 | . . . . . 6
⊢ (𝜑 → (∅ ⊆ 𝐷 →
(0g‘𝑃) =
(𝑦 ∈ 𝐷 ↦ 0 ))) | 
| 86 |  | ssun1 4177 | . . . . . . . . . . 11
⊢ 𝑥 ⊆ (𝑥 ∪ {𝑧}) | 
| 87 |  | sstr2 3989 | . . . . . . . . . . 11
⊢ (𝑥 ⊆ (𝑥 ∪ {𝑧}) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → 𝑥 ⊆ 𝐷)) | 
| 88 | 86, 87 | ax-mp 5 | . . . . . . . . . 10
⊢ ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → 𝑥 ⊆ 𝐷) | 
| 89 | 88 | imim1i 63 | . . . . . . . . 9
⊢ ((𝑥 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))) | 
| 90 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ ((𝑃 Σg
(𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) → ((𝑃 Σg
(𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0
)))))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))) | 
| 91 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(+g‘𝑃) = (+g‘𝑃) | 
| 92 | 1, 78, 79 | mplringd 22044 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ Ring) | 
| 93 |  | ringcmn 20280 | . . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd) | 
| 94 | 92, 93 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ CMnd) | 
| 95 | 94 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑃 ∈ CMnd) | 
| 96 |  | simprll 778 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑥 ∈ Fin) | 
| 97 |  | simprr 772 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑥 ∪ {𝑧}) ⊆ 𝐷) | 
| 98 | 97 | unssad 4192 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑥 ⊆ 𝐷) | 
| 99 | 98 | sselda 3982 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝐷) | 
| 100 | 78 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝐼 ∈ 𝑊) | 
| 101 | 79 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring) | 
| 102 | 1, 100, 101 | mpllmodd 22045 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑃 ∈ LMod) | 
| 103 | 6 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑋‘𝑘) ∈ (Base‘𝑅)) | 
| 104 | 1, 78, 79 | mplsca 22034 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) | 
| 105 | 104 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 = (Scalar‘𝑃)) | 
| 106 | 105 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (Base‘𝑅) = (Base‘(Scalar‘𝑃))) | 
| 107 | 103, 106 | eleqtrd 2842 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑋‘𝑘) ∈ (Base‘(Scalar‘𝑃))) | 
| 108 |  | mplcoe1.o | . . . . . . . . . . . . . . . . . 18
⊢  1 =
(1r‘𝑅) | 
| 109 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑘 ∈ 𝐷) | 
| 110 | 1, 3, 15, 108, 4, 100, 101, 109 | mplmon 22054 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵) | 
| 111 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) | 
| 112 |  | mplcoe1.n | . . . . . . . . . . . . . . . . . 18
⊢  · = (
·𝑠 ‘𝑃) | 
| 113 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) | 
| 114 | 3, 111, 112, 113 | lmodvscl 20877 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ LMod ∧ (𝑋‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵) | 
| 115 | 102, 107,
110, 114 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵) | 
| 116 | 115 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘 ∈ 𝐷) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵) | 
| 117 | 99, 116 | syldan 591 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘 ∈ 𝑥) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵) | 
| 118 |  | vex 3483 | . . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V | 
| 119 | 118 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑧 ∈ V) | 
| 120 |  | simprlr 779 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ¬ 𝑧 ∈ 𝑥) | 
| 121 | 1, 78, 79 | mpllmodd 22045 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ LMod) | 
| 122 | 121 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑃 ∈ LMod) | 
| 123 | 6 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑋:𝐷⟶(Base‘𝑅)) | 
| 124 | 97 | unssbd 4193 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → {𝑧} ⊆ 𝐷) | 
| 125 | 118 | snss 4784 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝐷 ↔ {𝑧} ⊆ 𝐷) | 
| 126 | 124, 125 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑧 ∈ 𝐷) | 
| 127 | 123, 126 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑋‘𝑧) ∈ (Base‘𝑅)) | 
| 128 | 104 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 = (Scalar‘𝑃)) | 
| 129 | 128 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃))) | 
| 130 | 127, 129 | eleqtrd 2842 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑋‘𝑧) ∈ (Base‘(Scalar‘𝑃))) | 
| 131 | 78 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝐼 ∈ 𝑊) | 
| 132 | 79 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 ∈ Ring) | 
| 133 | 1, 3, 15, 108, 4, 131, 132, 126 | mplmon 22054 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) ∈ 𝐵) | 
| 134 | 3, 111, 112, 113 | lmodvscl 20877 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ LMod ∧ (𝑋‘𝑧) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) ∈ 𝐵) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) ∈ 𝐵) | 
| 135 | 122, 130,
133, 134 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) ∈ 𝐵) | 
| 136 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑧 → (𝑋‘𝑘) = (𝑋‘𝑧)) | 
| 137 |  | equequ2 2024 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑧 → (𝑦 = 𝑘 ↔ 𝑦 = 𝑧)) | 
| 138 | 137 | ifbid 4548 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑧 → if(𝑦 = 𝑘, 1 , 0 ) = if(𝑦 = 𝑧, 1 , 0 )) | 
| 139 | 138 | mpteq2dv 5243 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑧 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) | 
| 140 | 136, 139 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑧 → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) | 
| 141 | 3, 91, 95, 96, 117, 119, 120, 135, 140 | gsumunsn 19979 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = ((𝑃 Σg
(𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0
)))))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))) | 
| 142 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 143 | 123 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅)) | 
| 144 | 2, 15 | ring0cl 20265 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ Ring → 0 ∈
(Base‘𝑅)) | 
| 145 | 79, 144 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 ∈ (Base‘𝑅)) | 
| 146 | 145 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → 0 ∈ (Base‘𝑅)) | 
| 147 | 143, 146 | ifcld 4571 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) ∈ (Base‘𝑅)) | 
| 148 | 147 | fmpttd 7134 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )):𝐷⟶(Base‘𝑅)) | 
| 149 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝑅)
∈ V | 
| 150 | 149, 13 | elmap 8912 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈
((Base‘𝑅)
↑m 𝐷)
↔ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )):𝐷⟶(Base‘𝑅)) | 
| 151 | 148, 150 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈
((Base‘𝑅)
↑m 𝐷)) | 
| 152 | 29, 2, 4, 30, 131 | psrbas 21954 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (Base‘(𝐼 mPwSer 𝑅)) = ((Base‘𝑅) ↑m 𝐷)) | 
| 153 | 151, 152 | eleqtrrd 2843 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈
(Base‘(𝐼 mPwSer 𝑅))) | 
| 154 | 13 | mptex 7244 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈
V | 
| 155 |  | funmpt 6603 | . . . . . . . . . . . . . . . . . . 19
⊢ Fun
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) | 
| 156 | 154, 155,
16 | 3pm3.2i 1339 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ V ∧ Fun
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∧ 0 ∈
V) | 
| 157 | 156 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ V ∧ Fun
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∧ 0 ∈
V)) | 
| 158 |  | eldifn 4131 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝐷 ∖ 𝑥) → ¬ 𝑦 ∈ 𝑥) | 
| 159 | 158 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ (𝐷 ∖ 𝑥)) → ¬ 𝑦 ∈ 𝑥) | 
| 160 | 159 | iffalsed 4535 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ (𝐷 ∖ 𝑥)) → if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) = 0 ) | 
| 161 | 13 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝐷 ∈ V) | 
| 162 | 160, 161 | suppss2 8226 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) supp 0 ) ⊆ 𝑥) | 
| 163 |  | suppssfifsupp 9421 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ V ∧ Fun
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∧ 0 ∈ V)
∧ (𝑥 ∈ Fin ∧
((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) supp 0 ) ⊆ 𝑥)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) finSupp 0
) | 
| 164 | 157, 96, 162, 163 | syl12anc 836 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) finSupp 0
) | 
| 165 | 1, 29, 30, 15, 3 | mplelbas 22012 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ 𝐵 ↔ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈
(Base‘(𝐼 mPwSer 𝑅)) ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) finSupp 0
)) | 
| 166 | 153, 164,
165 | sylanbrc 583 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ 𝐵) | 
| 167 | 1, 3, 142, 91, 166, 135 | mpladd 22030 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∘f
(+g‘𝑅)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))) | 
| 168 |  | ovexd 7467 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) ∈
V) | 
| 169 |  | eqidd 2737 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) | 
| 170 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 171 | 1, 112, 2, 3, 170, 4, 127, 133 | mplvsca 22036 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = ((𝐷 × {(𝑋‘𝑧)}) ∘f
(.r‘𝑅)(𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) | 
| 172 | 127 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑧) ∈ (Base‘𝑅)) | 
| 173 | 2, 108 | ringidcl 20263 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ Ring → 1 ∈
(Base‘𝑅)) | 
| 174 | 173, 144 | ifcld 4571 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ Ring → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅)) | 
| 175 | 79, 174 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅)) | 
| 176 | 175 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅)) | 
| 177 |  | fconstmpt 5746 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐷 × {(𝑋‘𝑧)}) = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑧)) | 
| 178 | 177 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝐷 × {(𝑋‘𝑧)}) = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑧))) | 
| 179 |  | eqidd 2737 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) | 
| 180 | 161, 172,
176, 178, 179 | offval2 7718 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝐷 × {(𝑋‘𝑧)}) ∘f
(.r‘𝑅)(𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )))) | 
| 181 | 171, 180 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )))) | 
| 182 | 161, 147,
168, 169, 181 | offval2 7718 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∘f
(+g‘𝑅)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = (𝑦 ∈ 𝐷 ↦ (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))))) | 
| 183 | 132, 80 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 ∈ Grp) | 
| 184 | 2, 142, 15 | grplid 18986 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Grp ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ( 0 (+g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑧)) | 
| 185 | 183, 127,
184 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ( 0 (+g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑧)) | 
| 186 | 185 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ( 0 (+g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑧)) | 
| 187 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 ∈ {𝑧}) | 
| 188 |  | velsn 4641 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ {𝑧} ↔ 𝑦 = 𝑧) | 
| 189 | 187, 188 | sylib 218 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 = 𝑧) | 
| 190 | 189 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → (𝑋‘𝑦) = (𝑋‘𝑧)) | 
| 191 | 186, 190 | eqtr4d 2779 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ( 0 (+g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑦)) | 
| 192 | 120 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ¬ 𝑧 ∈ 𝑥) | 
| 193 | 189, 192 | eqneltrd 2860 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ¬ 𝑦 ∈ 𝑥) | 
| 194 | 193 | iffalsed 4535 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) = 0 ) | 
| 195 | 189 | iftrued 4532 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 = 𝑧, 1 , 0 ) = 1 ) | 
| 196 | 195 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = ((𝑋‘𝑧)(.r‘𝑅) 1 )) | 
| 197 | 2, 170, 108 | ringridm 20268 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(.r‘𝑅) 1 ) = (𝑋‘𝑧)) | 
| 198 | 132, 127,
197 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧)(.r‘𝑅) 1 ) = (𝑋‘𝑧)) | 
| 199 | 198 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(.r‘𝑅) 1 ) = (𝑋‘𝑧)) | 
| 200 | 196, 199 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = (𝑋‘𝑧)) | 
| 201 | 194, 200 | oveq12d 7450 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = ( 0 (+g‘𝑅)(𝑋‘𝑧))) | 
| 202 |  | elun2 4182 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ {𝑧} → 𝑦 ∈ (𝑥 ∪ {𝑧})) | 
| 203 | 202 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 ∈ (𝑥 ∪ {𝑧})) | 
| 204 | 203 | iftrued 4532 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) | 
| 205 | 191, 201,
204 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) | 
| 206 | 81 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Grp) | 
| 207 | 2, 142, 15 | grprid 18987 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ Grp ∧ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) ∈ (Base‘𝑅)) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)
0 ) =
if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) | 
| 208 | 206, 147,
207 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)
0 ) =
if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) | 
| 209 | 208 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)
0 ) =
if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) | 
| 210 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ¬ 𝑦 ∈ {𝑧}) | 
| 211 | 210, 188 | sylnib 328 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ¬ 𝑦 = 𝑧) | 
| 212 | 211 | iffalsed 4535 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → if(𝑦 = 𝑧, 1 , 0 ) = 0 ) | 
| 213 | 212 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = ((𝑋‘𝑧)(.r‘𝑅) 0 )) | 
| 214 | 2, 170, 15 | ringrz 20292 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 ) | 
| 215 | 132, 127,
214 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 ) | 
| 216 | 215 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 ) | 
| 217 | 213, 216 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = 0 ) | 
| 218 | 217 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)
0
)) | 
| 219 |  | elun 4152 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑦 ∈ 𝑥 ∨ 𝑦 ∈ {𝑧})) | 
| 220 |  | orcom 870 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ 𝑥 ∨ 𝑦 ∈ {𝑧}) ↔ (𝑦 ∈ {𝑧} ∨ 𝑦 ∈ 𝑥)) | 
| 221 | 219, 220 | bitri 275 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑦 ∈ {𝑧} ∨ 𝑦 ∈ 𝑥)) | 
| 222 |  | biorf 936 | . . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑦 ∈ {𝑧} → (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ {𝑧} ∨ 𝑦 ∈ 𝑥))) | 
| 223 | 221, 222 | bitr4id 290 | . . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑦 ∈ {𝑧} → (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑦 ∈ 𝑥)) | 
| 224 | 223 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑦 ∈ 𝑥)) | 
| 225 | 224 | ifbid 4548 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) | 
| 226 | 209, 218,
225 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) | 
| 227 | 205, 226 | pm2.61dan 812 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) | 
| 228 | 227 | mpteq2dva 5241 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))) | 
| 229 | 167, 182,
228 | 3eqtrrd 2781 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))) | 
| 230 | 141, 229 | eqeq12d 2752 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) ↔ ((𝑃 Σg
(𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0
)))))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))) | 
| 231 | 90, 230 | imbitrrid 246 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) → (𝑃 Σg
(𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))) | 
| 232 | 231 | expr 456 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥)) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → ((𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) → (𝑃 Σg
(𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))) | 
| 233 | 232 | a2d 29 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥)) → (((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))) | 
| 234 | 89, 233 | syl5 34 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥)) → ((𝑥 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))) | 
| 235 | 234 | expcom 413 | . . . . . . 7
⊢ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) → (𝜑 → ((𝑥 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))) | 
| 236 | 235 | a2d 29 | . . . . . 6
⊢ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) → ((𝜑 → (𝑥 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))) → (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))) | 
| 237 | 50, 59, 68, 77, 85, 236 | findcard2s 9206 | . . . . 5
⊢ ((𝑋 supp 0 ) ∈ Fin → (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))))) | 
| 238 | 34, 237 | mpcom 38 | . . . 4
⊢ (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))) | 
| 239 | 28, 238 | mpd 15 | . . 3
⊢ (𝜑 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))) | 
| 240 | 26, 239 | eqtr4d 2779 | . 2
⊢ (𝜑 → 𝑋 = (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) | 
| 241 | 28 | resmptd 6057 | . . . 4
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 )) = (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) | 
| 242 | 241 | oveq2d 7448 | . . 3
⊢ (𝜑 → (𝑃 Σg ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 ))) = (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) | 
| 243 | 115 | fmpttd 7134 | . . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))):𝐷⟶𝐵) | 
| 244 | 6, 11, 14, 17 | suppssr 8221 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋‘𝑘) = 0 ) | 
| 245 | 244 | oveq1d 7447 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) | 
| 246 |  | eldifi 4130 | . . . . . . 7
⊢ (𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 )) → 𝑘 ∈ 𝐷) | 
| 247 | 105 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (0g‘𝑅) =
(0g‘(Scalar‘𝑃))) | 
| 248 | 15, 247 | eqtrid 2788 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 0 =
(0g‘(Scalar‘𝑃))) | 
| 249 | 248 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) =
((0g‘(Scalar‘𝑃)) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) | 
| 250 |  | eqid 2736 | . . . . . . . . . 10
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝑃)) | 
| 251 | 3, 111, 112, 250, 40 | lmod0vs 20894 | . . . . . . . . 9
⊢ ((𝑃 ∈ LMod ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵) →
((0g‘(Scalar‘𝑃)) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) =
(0g‘𝑃)) | 
| 252 | 102, 110,
251 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) →
((0g‘(Scalar‘𝑃)) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) =
(0g‘𝑃)) | 
| 253 | 249, 252 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) =
(0g‘𝑃)) | 
| 254 | 246, 253 | sylan2 593 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) =
(0g‘𝑃)) | 
| 255 | 245, 254 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) =
(0g‘𝑃)) | 
| 256 | 255, 14 | suppss2 8226 | . . . 4
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) supp
(0g‘𝑃))
⊆ (𝑋 supp 0
)) | 
| 257 | 13 | mptex 7244 | . . . . . . 7
⊢ (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈
V | 
| 258 |  | funmpt 6603 | . . . . . . 7
⊢ Fun
(𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) | 
| 259 |  | fvex 6918 | . . . . . . 7
⊢
(0g‘𝑃) ∈ V | 
| 260 | 257, 258,
259 | 3pm3.2i 1339 | . . . . . 6
⊢ ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V ∧ Fun
(𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∧
(0g‘𝑃)
∈ V) | 
| 261 | 260 | a1i 11 | . . . . 5
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V ∧ Fun
(𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∧
(0g‘𝑃)
∈ V)) | 
| 262 |  | suppssfifsupp 9421 | . . . . 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‘𝑃)) | 
| 263 | 261, 34, 256, 262 | syl12anc 836 | . . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) finSupp
(0g‘𝑃)) | 
| 264 | 3, 40, 94, 14, 243, 256, 263 | gsumres 19932 | . . 3
⊢ (𝜑 → (𝑃 Σg ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 ))) = (𝑃 Σg (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) | 
| 265 | 242, 264 | eqtr3d 2778 | . 2
⊢ (𝜑 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) | 
| 266 | 240, 265 | eqtrd 2776 | 1
⊢ (𝜑 → 𝑋 = (𝑃 Σg (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) |