Step | Hyp | Ref
| Expression |
1 | | mplcoe1.p |
. . . . . 6
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
2 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | mplcoe1.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑃) |
4 | | mplcoe1.d |
. . . . . 6
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
5 | | mplcoe1.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
6 | 1, 2, 3, 4, 5 | mplelf 19433 |
. . . . 5
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
7 | 6 | feqmptd 6249 |
. . . 4
⊢ (𝜑 → 𝑋 = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑦))) |
8 | | iftrue 4092 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑋 supp 0 ) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) |
9 | 8 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝑋 supp 0 )) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) |
10 | | eldif 3584 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ (𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ (𝑋 supp 0 ))) |
11 | | ifid 4125 |
. . . . . . . . 9
⊢ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), (𝑋‘𝑦)) = (𝑋‘𝑦) |
12 | | ssid 3624 |
. . . . . . . . . . . 12
⊢ (𝑋 supp 0 ) ⊆ (𝑋 supp 0 ) |
13 | 12 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 supp 0 ) ⊆ (𝑋 supp 0 )) |
14 | | ovex 6678 |
. . . . . . . . . . . . 13
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
15 | 4, 14 | rabex2 4815 |
. . . . . . . . . . . 12
⊢ 𝐷 ∈ V |
16 | 15 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ V) |
17 | | mplcoe1.z |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘𝑅) |
18 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑅) ∈ V |
19 | 17, 18 | eqeltri 2697 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ V) |
21 | 6, 13, 16, 20 | suppssr 7326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋‘𝑦) = 0 ) |
22 | 21 | ifeq2d 4105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), (𝑋‘𝑦)) = if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )) |
23 | 11, 22 | syl5reqr 2671 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) |
24 | 10, 23 | sylan2br 493 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) |
25 | 24 | anassrs 680 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ (𝑋 supp 0 )) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) |
26 | 9, 25 | pm2.61dan 832 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) |
27 | 26 | mpteq2dva 4744 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑦))) |
28 | 7, 27 | eqtr4d 2659 |
. . 3
⊢ (𝜑 → 𝑋 = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))) |
29 | | suppssdm 7308 |
. . . . 5
⊢ (𝑋 supp 0 ) ⊆ dom 𝑋 |
30 | | fdm 6051 |
. . . . . 6
⊢ (𝑋:𝐷⟶(Base‘𝑅) → dom 𝑋 = 𝐷) |
31 | 6, 30 | syl 17 |
. . . . 5
⊢ (𝜑 → dom 𝑋 = 𝐷) |
32 | 29, 31 | syl5sseq 3653 |
. . . 4
⊢ (𝜑 → (𝑋 supp 0 ) ⊆ 𝐷) |
33 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) |
34 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) |
35 | 1, 33, 34, 17, 3 | mplelbas 19430 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 ↔ (𝑋 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑋 finSupp 0 )) |
36 | 35 | simprbi 480 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → 𝑋 finSupp 0 ) |
37 | 5, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑋 finSupp 0 ) |
38 | 37 | fsuppimpd 8282 |
. . . . 5
⊢ (𝜑 → (𝑋 supp 0 ) ∈
Fin) |
39 | | sseq1 3626 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (𝑤 ⊆ 𝐷 ↔ ∅ ⊆ 𝐷)) |
40 | | mpteq1 4737 |
. . . . . . . . . . . 12
⊢ (𝑤 = ∅ → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ ∅ ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) |
41 | | mpt0 6021 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ∅ ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) =
∅ |
42 | 40, 41 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝑤 = ∅ → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) =
∅) |
43 | 42 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑤 = ∅ → (𝑃 Σg
(𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg
∅)) |
44 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(0g‘𝑃) = (0g‘𝑃) |
45 | 44 | gsum0 17278 |
. . . . . . . . . 10
⊢ (𝑃 Σg
∅) = (0g‘𝑃) |
46 | 43, 45 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → (𝑃 Σg
(𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) =
(0g‘𝑃)) |
47 | | noel 3919 |
. . . . . . . . . . . 12
⊢ ¬
𝑦 ∈
∅ |
48 | | eleq2 2690 |
. . . . . . . . . . . 12
⊢ (𝑤 = ∅ → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ∅)) |
49 | 47, 48 | mtbiri 317 |
. . . . . . . . . . 11
⊢ (𝑤 = ∅ → ¬ 𝑦 ∈ 𝑤) |
50 | 49 | iffalsed 4097 |
. . . . . . . . . 10
⊢ (𝑤 = ∅ → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = 0 ) |
51 | 50 | mpteq2dv 4745 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ 0 )) |
52 | 46, 51 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑤 = ∅ → ((𝑃 Σg
(𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔
(0g‘𝑃) =
(𝑦 ∈ 𝐷 ↦ 0 ))) |
53 | 39, 52 | imbi12d 334 |
. . . . . . 7
⊢ (𝑤 = ∅ → ((𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ (∅
⊆ 𝐷 →
(0g‘𝑃) =
(𝑦 ∈ 𝐷 ↦ 0 )))) |
54 | 53 | imbi2d 330 |
. . . . . 6
⊢ (𝑤 = ∅ → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → (∅ ⊆ 𝐷 →
(0g‘𝑃) =
(𝑦 ∈ 𝐷 ↦ 0 ))))) |
55 | | sseq1 3626 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (𝑤 ⊆ 𝐷 ↔ 𝑥 ⊆ 𝐷)) |
56 | | mpteq1 4737 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) |
57 | 56 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) |
58 | | eleq2 2690 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥)) |
59 | 58 | ifbid 4108 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) |
60 | 59 | mpteq2dv 4745 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) |
61 | 57, 60 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → ((𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (𝑃 Σg
(𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))) |
62 | 55, 61 | imbi12d 334 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → ((𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ (𝑥 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))))) |
63 | 62 | imbi2d 330 |
. . . . . 6
⊢ (𝑤 = 𝑥 → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → (𝑥 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))))) |
64 | | sseq1 3626 |
. . . . . . . 8
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑤 ⊆ 𝐷 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) |
65 | | mpteq1 4737 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) |
66 | 65 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) |
67 | | eleq2 2690 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ (𝑥 ∪ {𝑧}))) |
68 | 67 | ifbid 4108 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) |
69 | 68 | mpteq2dv 4745 |
. . . . . . . . 9
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))) |
70 | 66, 69 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (𝑃 Σg
(𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))) |
71 | 64, 70 | imbi12d 334 |
. . . . . . 7
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))) |
72 | 71 | imbi2d 330 |
. . . . . 6
⊢ (𝑤 = (𝑥 ∪ {𝑧}) → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))) |
73 | | sseq1 3626 |
. . . . . . . 8
⊢ (𝑤 = (𝑋 supp 0 ) → (𝑤 ⊆ 𝐷 ↔ (𝑋 supp 0 ) ⊆ 𝐷)) |
74 | | mpteq1 4737 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑋 supp 0 ) → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) |
75 | 74 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑤 = (𝑋 supp 0 ) → (𝑃 Σg
(𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) |
76 | | eleq2 2690 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑋 supp 0 ) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ (𝑋 supp 0 ))) |
77 | 76 | ifbid 4108 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑋 supp 0 ) → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )) |
78 | 77 | mpteq2dv 4745 |
. . . . . . . . 9
⊢ (𝑤 = (𝑋 supp 0 ) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))) |
79 | 75, 78 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑤 = (𝑋 supp 0 ) → ((𝑃 Σg
(𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (𝑃 Σg
(𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))) |
80 | 73, 79 | imbi12d 334 |
. . . . . . 7
⊢ (𝑤 = (𝑋 supp 0 ) → ((𝑤 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))))) |
81 | 80 | imbi2d 330 |
. . . . . 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 18552 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
85 | 83, 84 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Grp) |
86 | 1, 4, 17, 44, 82, 85 | mpl0 19441 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑃) = (𝐷 × { 0 })) |
87 | | fconstmpt 5163 |
. . . . . . . 8
⊢ (𝐷 × { 0 }) = (𝑦 ∈ 𝐷 ↦ 0 ) |
88 | 86, 87 | syl6eq 2672 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝑃) = (𝑦 ∈ 𝐷 ↦ 0 )) |
89 | 88 | a1d 25 |
. . . . . 6
⊢ (𝜑 → (∅ ⊆ 𝐷 →
(0g‘𝑃) =
(𝑦 ∈ 𝐷 ↦ 0 ))) |
90 | | ssun1 3776 |
. . . . . . . . . . 11
⊢ 𝑥 ⊆ (𝑥 ∪ {𝑧}) |
91 | | sstr2 3610 |
. . . . . . . . . . 11
⊢ (𝑥 ⊆ (𝑥 ∪ {𝑧}) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → 𝑥 ⊆ 𝐷)) |
92 | 90, 91 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → 𝑥 ⊆ 𝐷) |
93 | 92 | imim1i 63 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))) |
94 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ ((𝑃 Σg
(𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) → ((𝑃 Σg
(𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0
)))))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))) |
95 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝑃) = (+g‘𝑃) |
96 | 1 | mplring 19452 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring) |
97 | 82, 83, 96 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ Ring) |
98 | | ringcmn 18581 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ CMnd) |
100 | 99 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑃 ∈ CMnd) |
101 | | simprll 802 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑥 ∈ Fin) |
102 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑥 ∪ {𝑧}) ⊆ 𝐷) |
103 | 102 | unssad 3790 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑥 ⊆ 𝐷) |
104 | 103 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝐷) |
105 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝐼 ∈ 𝑊) |
106 | 83 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring) |
107 | 1 | mpllmod 19451 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ LMod) |
108 | 105, 106,
107 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑃 ∈ LMod) |
109 | 6 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑋‘𝑘) ∈ (Base‘𝑅)) |
110 | 1, 82, 83 | mplsca 19445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) |
111 | 110 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 = (Scalar‘𝑃)) |
112 | 111 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (Base‘𝑅) = (Base‘(Scalar‘𝑃))) |
113 | 109, 112 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑋‘𝑘) ∈ (Base‘(Scalar‘𝑃))) |
114 | | mplcoe1.o |
. . . . . . . . . . . . . . . . . 18
⊢ 1 =
(1r‘𝑅) |
115 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑘 ∈ 𝐷) |
116 | 1, 3, 17, 114, 4, 105, 106, 115 | mplmon 19463 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵) |
117 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
118 | | mplcoe1.n |
. . . . . . . . . . . . . . . . . 18
⊢ · = (
·𝑠 ‘𝑃) |
119 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
120 | 3, 117, 118, 119 | lmodvscl 18880 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ LMod ∧ (𝑋‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵) |
121 | 108, 113,
116, 120 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵) |
122 | 121 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘 ∈ 𝐷) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵) |
123 | 104, 122 | syldan 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘 ∈ 𝑥) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵) |
124 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
125 | 124 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑧 ∈ V) |
126 | | simprlr 803 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ¬ 𝑧 ∈ 𝑥) |
127 | 82, 83, 107 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ LMod) |
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑃 ∈ LMod) |
129 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑋:𝐷⟶(Base‘𝑅)) |
130 | 102 | unssbd 3791 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → {𝑧} ⊆ 𝐷) |
131 | 124 | snss 4316 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝐷 ↔ {𝑧} ⊆ 𝐷) |
132 | 130, 131 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑧 ∈ 𝐷) |
133 | 129, 132 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑋‘𝑧) ∈ (Base‘𝑅)) |
134 | 110 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 = (Scalar‘𝑃)) |
135 | 134 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃))) |
136 | 133, 135 | eleqtrd 2703 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑋‘𝑧) ∈ (Base‘(Scalar‘𝑃))) |
137 | 82 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝐼 ∈ 𝑊) |
138 | 83 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 ∈ Ring) |
139 | 1, 3, 17, 114, 4, 137, 138, 132 | mplmon 19463 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) ∈ 𝐵) |
140 | 3, 117, 118, 119 | lmodvscl 18880 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ LMod ∧ (𝑋‘𝑧) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) ∈ 𝐵) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) ∈ 𝐵) |
141 | 128, 136,
139, 140 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) ∈ 𝐵) |
142 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑧 → (𝑋‘𝑘) = (𝑋‘𝑧)) |
143 | | equequ2 1953 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑧 → (𝑦 = 𝑘 ↔ 𝑦 = 𝑧)) |
144 | 143 | ifbid 4108 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑧 → if(𝑦 = 𝑘, 1 , 0 ) = if(𝑦 = 𝑧, 1 , 0 )) |
145 | 144 | mpteq2dv 4745 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑧 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) |
146 | 142, 145 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑧 → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) |
147 | 3, 95, 100, 101, 123, 125, 126, 141, 146 | gsumunsn 18359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = ((𝑃 Σg
(𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0
)))))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))) |
148 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(+g‘𝑅) = (+g‘𝑅) |
149 | 129 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅)) |
150 | 2, 17 | ring0cl 18569 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ Ring → 0 ∈
(Base‘𝑅)) |
151 | 83, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 ∈ (Base‘𝑅)) |
152 | 151 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → 0 ∈ (Base‘𝑅)) |
153 | 149, 152 | ifcld 4131 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) ∈ (Base‘𝑅)) |
154 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) |
155 | 153, 154 | fmptd 6385 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )):𝐷⟶(Base‘𝑅)) |
156 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝑅)
∈ V |
157 | 156, 15 | elmap 7886 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈
((Base‘𝑅)
↑𝑚 𝐷) ↔ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )):𝐷⟶(Base‘𝑅)) |
158 | 155, 157 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈
((Base‘𝑅)
↑𝑚 𝐷)) |
159 | 33, 2, 4, 34, 137 | psrbas 19378 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (Base‘(𝐼 mPwSer 𝑅)) = ((Base‘𝑅) ↑𝑚 𝐷)) |
160 | 158, 159 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈
(Base‘(𝐼 mPwSer 𝑅))) |
161 | 15 | mptex 6486 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈
V |
162 | | funmpt 5926 |
. . . . . . . . . . . . . . . . . . 19
⊢ Fun
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) |
163 | 161, 162,
19 | 3pm3.2i 1239 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ V ∧ Fun
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∧ 0 ∈
V) |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ V ∧ Fun
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∧ 0 ∈
V)) |
165 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝐷 ∖ 𝑥) → ¬ 𝑦 ∈ 𝑥) |
166 | 165 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ (𝐷 ∖ 𝑥)) → ¬ 𝑦 ∈ 𝑥) |
167 | 166 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ (𝐷 ∖ 𝑥)) → if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) = 0 ) |
168 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝐷 ∈ V) |
169 | 167, 168 | suppss2 7329 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) supp 0 ) ⊆ 𝑥) |
170 | | suppssfifsupp 8290 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ V ∧ Fun
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∧ 0 ∈ V)
∧ (𝑥 ∈ Fin ∧
((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) supp 0 ) ⊆ 𝑥)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) finSupp 0
) |
171 | 164, 101,
169, 170 | syl12anc 1324 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) finSupp 0
) |
172 | 1, 33, 34, 17, 3 | mplelbas 19430 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ 𝐵 ↔ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈
(Base‘(𝐼 mPwSer 𝑅)) ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) finSupp 0
)) |
173 | 160, 171,
172 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ 𝐵) |
174 | 1, 3, 148, 95, 173, 141 | mpladd 19442 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
∘𝑓 (+g‘𝑅)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))) |
175 | | ovexd 6680 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) ∈
V) |
176 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) |
177 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑅) = (.r‘𝑅) |
178 | 1, 118, 2, 3, 177, 4, 133, 139 | mplvsca 19447 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = ((𝐷 × {(𝑋‘𝑧)}) ∘𝑓
(.r‘𝑅)(𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) |
179 | 133 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑧) ∈ (Base‘𝑅)) |
180 | 2, 114 | ringidcl 18568 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ Ring → 1 ∈
(Base‘𝑅)) |
181 | 180, 150 | ifcld 4131 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ Ring → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅)) |
182 | 83, 181 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅)) |
183 | 182 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅)) |
184 | | fconstmpt 5163 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐷 × {(𝑋‘𝑧)}) = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑧)) |
185 | 184 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝐷 × {(𝑋‘𝑧)}) = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑧))) |
186 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) |
187 | 168, 179,
183, 185, 186 | offval2 6914 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝐷 × {(𝑋‘𝑧)}) ∘𝑓
(.r‘𝑅)(𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )))) |
188 | 178, 187 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )))) |
189 | 168, 153,
175, 176, 188 | offval2 6914 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
∘𝑓 (+g‘𝑅)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = (𝑦 ∈ 𝐷 ↦ (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))))) |
190 | 138, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 ∈ Grp) |
191 | 2, 148, 17 | grplid 17452 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Grp ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ( 0 (+g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑧)) |
192 | 190, 133,
191 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ( 0 (+g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑧)) |
193 | 192 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ( 0 (+g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑧)) |
194 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 ∈ {𝑧}) |
195 | | velsn 4193 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ {𝑧} ↔ 𝑦 = 𝑧) |
196 | 194, 195 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 = 𝑧) |
197 | 196 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → (𝑋‘𝑦) = (𝑋‘𝑧)) |
198 | 193, 197 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ( 0 (+g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑦)) |
199 | 126 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ¬ 𝑧 ∈ 𝑥) |
200 | 196, 199 | eqneltrd 2720 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ¬ 𝑦 ∈ 𝑥) |
201 | 200 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) = 0 ) |
202 | 196 | iftrued 4094 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 = 𝑧, 1 , 0 ) = 1 ) |
203 | 202 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = ((𝑋‘𝑧)(.r‘𝑅) 1 )) |
204 | 2, 177, 114 | ringridm 18572 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(.r‘𝑅) 1 ) = (𝑋‘𝑧)) |
205 | 138, 133,
204 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧)(.r‘𝑅) 1 ) = (𝑋‘𝑧)) |
206 | 205 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(.r‘𝑅) 1 ) = (𝑋‘𝑧)) |
207 | 203, 206 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = (𝑋‘𝑧)) |
208 | 201, 207 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = ( 0 (+g‘𝑅)(𝑋‘𝑧))) |
209 | | elun2 3781 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ {𝑧} → 𝑦 ∈ (𝑥 ∪ {𝑧})) |
210 | 209 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 ∈ (𝑥 ∪ {𝑧})) |
211 | 210 | iftrued 4094 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦)) |
212 | 198, 208,
211 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) |
213 | 85 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Grp) |
214 | 2, 148, 17 | grprid 17453 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ Grp ∧ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) ∈ (Base‘𝑅)) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)
0 ) =
if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) |
215 | 213, 153,
214 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)
0 ) =
if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) |
216 | 215 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)
0 ) =
if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) |
217 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ¬ 𝑦 ∈ {𝑧}) |
218 | 217, 195 | sylnib 318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ¬ 𝑦 = 𝑧) |
219 | 218 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → if(𝑦 = 𝑧, 1 , 0 ) = 0 ) |
220 | 219 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = ((𝑋‘𝑧)(.r‘𝑅) 0 )) |
221 | 2, 177, 17 | ringrz 18588 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 ) |
222 | 138, 133,
221 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 ) |
223 | 222 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 ) |
224 | 220, 223 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = 0 ) |
225 | 224 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)
0
)) |
226 | | biorf 420 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑦 ∈ {𝑧} → (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ {𝑧} ∨ 𝑦 ∈ 𝑥))) |
227 | | elun 3753 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑦 ∈ 𝑥 ∨ 𝑦 ∈ {𝑧})) |
228 | | orcom 402 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ 𝑥 ∨ 𝑦 ∈ {𝑧}) ↔ (𝑦 ∈ {𝑧} ∨ 𝑦 ∈ 𝑥)) |
229 | 227, 228 | bitri 264 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑦 ∈ {𝑧} ∨ 𝑦 ∈ 𝑥)) |
230 | 226, 229 | syl6rbbr 279 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑦 ∈ {𝑧} → (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑦 ∈ 𝑥)) |
231 | 230 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑦 ∈ 𝑥)) |
232 | 231 | ifbid 4108 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) |
233 | 216, 225,
232 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) |
234 | 212, 233 | pm2.61dan 832 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) |
235 | 234 | mpteq2dva 4744 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
)(+g‘𝑅)((𝑋‘𝑧)(.r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))) |
236 | 174, 189,
235 | 3eqtrrd 2661 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))) |
237 | 147, 236 | eqeq12d 2637 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) ↔ ((𝑃 Σg
(𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0
)))))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0
))(+g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))) |
238 | 94, 237 | syl5ibr 236 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) → (𝑃 Σg
(𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))) |
239 | 238 | expr 643 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥)) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → ((𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) → (𝑃 Σg
(𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))) |
240 | 239 | a2d 29 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥)) → (((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))) |
241 | 93, 240 | syl5 34 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥)) → ((𝑥 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))) |
242 | 241 | expcom 451 |
. . . . . . 7
⊢ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) → (𝜑 → ((𝑥 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))) |
243 | 242 | a2d 29 |
. . . . . 6
⊢ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) → ((𝜑 → (𝑥 ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))) → (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))) |
244 | 54, 63, 72, 81, 89, 243 | findcard2s 8201 |
. . . . 5
⊢ ((𝑋 supp 0 ) ∈ Fin → (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))))) |
245 | 38, 244 | mpcom 38 |
. . . 4
⊢ (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))) |
246 | 32, 245 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))) |
247 | 28, 246 | eqtr4d 2659 |
. 2
⊢ (𝜑 → 𝑋 = (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) |
248 | 32 | resmptd 5452 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 )) = (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) |
249 | 248 | oveq2d 6666 |
. . 3
⊢ (𝜑 → (𝑃 Σg ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 ))) = (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) |
250 | | eqid 2622 |
. . . . 5
⊢ (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) |
251 | 121, 250 | fmptd 6385 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))):𝐷⟶𝐵) |
252 | 6, 13, 16, 20 | suppssr 7326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋‘𝑘) = 0 ) |
253 | 252 | oveq1d 6665 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) |
254 | | eldifi 3732 |
. . . . . . 7
⊢ (𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 )) → 𝑘 ∈ 𝐷) |
255 | 111 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
256 | 17, 255 | syl5eq 2668 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 0 =
(0g‘(Scalar‘𝑃))) |
257 | 256 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) =
((0g‘(Scalar‘𝑃)) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) |
258 | | eqid 2622 |
. . . . . . . . . 10
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝑃)) |
259 | 3, 117, 118, 258, 44 | lmod0vs 18896 |
. . . . . . . . 9
⊢ ((𝑃 ∈ LMod ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵) →
((0g‘(Scalar‘𝑃)) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) =
(0g‘𝑃)) |
260 | 108, 116,
259 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) →
((0g‘(Scalar‘𝑃)) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) =
(0g‘𝑃)) |
261 | 257, 260 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) =
(0g‘𝑃)) |
262 | 254, 261 | sylan2 491 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) =
(0g‘𝑃)) |
263 | 253, 262 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) =
(0g‘𝑃)) |
264 | 263, 16 | suppss2 7329 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) supp
(0g‘𝑃))
⊆ (𝑋 supp 0
)) |
265 | 15 | mptex 6486 |
. . . . . . 7
⊢ (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈
V |
266 | | funmpt 5926 |
. . . . . . 7
⊢ Fun
(𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) |
267 | | fvex 6201 |
. . . . . . 7
⊢
(0g‘𝑃) ∈ V |
268 | 265, 266,
267 | 3pm3.2i 1239 |
. . . . . 6
⊢ ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V ∧ Fun
(𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∧
(0g‘𝑃)
∈ V) |
269 | 268 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V ∧ Fun
(𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∧
(0g‘𝑃)
∈ V)) |
270 | | suppssfifsupp 8290 |
. . . . 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‘𝑃)) |
271 | 269, 38, 264, 270 | syl12anc 1324 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) finSupp
(0g‘𝑃)) |
272 | 3, 44, 99, 16, 251, 264, 271 | gsumres 18314 |
. . 3
⊢ (𝜑 → (𝑃 Σg ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 ))) = (𝑃 Σg (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) |
273 | 249, 272 | eqtr3d 2658 |
. 2
⊢ (𝜑 → (𝑃 Σg (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σg (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) |
274 | 247, 273 | eqtrd 2656 |
1
⊢ (𝜑 → 𝑋 = (𝑃 Σg (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) |