Step | Hyp | Ref
| Expression |
1 | | mplcoe1.p |
. . . . . 6
β’ π = (πΌ mPoly π
) |
2 | | eqid 2733 |
. . . . . 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 21427 |
. . . . 5
β’ (π β π:π·βΆ(Baseβπ
)) |
7 | 6 | feqmptd 6914 |
. . . 4
β’ (π β π = (π¦ β π· β¦ (πβπ¦))) |
8 | | iftrue 4496 |
. . . . . . 7
β’ (π¦ β (π supp 0 ) β if(π¦ β (π supp 0 ), (πβπ¦), 0 ) = (πβπ¦)) |
9 | 8 | adantl 483 |
. . . . . 6
β’ (((π β§ π¦ β π·) β§ π¦ β (π supp 0 )) β if(π¦ β (π supp 0 ), (πβπ¦), 0 ) = (πβπ¦)) |
10 | | eldif 3924 |
. . . . . . . 8
β’ (π¦ β (π· β (π supp 0 )) β (π¦ β π· β§ Β¬ π¦ β (π supp 0 ))) |
11 | | ssidd 3971 |
. . . . . . . . . . 11
β’ (π β (π supp 0 ) β (π supp 0 )) |
12 | | ovex 7394 |
. . . . . . . . . . . . 13
β’
(β0 βm πΌ) β V |
13 | 4, 12 | rabex2 5295 |
. . . . . . . . . . . 12
β’ π· β V |
14 | 13 | a1i 11 |
. . . . . . . . . . 11
β’ (π β π· β V) |
15 | | mplcoe1.z |
. . . . . . . . . . . . 13
β’ 0 =
(0gβπ
) |
16 | 15 | fvexi 6860 |
. . . . . . . . . . . 12
β’ 0 β
V |
17 | 16 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 0 β V) |
18 | 6, 11, 14, 17 | suppssr 8131 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π· β (π supp 0 ))) β (πβπ¦) = 0 ) |
19 | 18 | ifeq2d 4510 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π· β (π supp 0 ))) β if(π¦ β (π supp 0 ), (πβπ¦), (πβπ¦)) = if(π¦ β (π supp 0 ), (πβπ¦), 0 )) |
20 | | ifid 4530 |
. . . . . . . . 9
β’ if(π¦ β (π supp 0 ), (πβπ¦), (πβπ¦)) = (πβπ¦) |
21 | 19, 20 | eqtr3di 2788 |
. . . . . . . 8
β’ ((π β§ π¦ β (π· β (π supp 0 ))) β if(π¦ β (π supp 0 ), (πβπ¦), 0 ) = (πβπ¦)) |
22 | 10, 21 | sylan2br 596 |
. . . . . . 7
β’ ((π β§ (π¦ β π· β§ Β¬ π¦ β (π supp 0 ))) β if(π¦ β (π supp 0 ), (πβπ¦), 0 ) = (πβπ¦)) |
23 | 22 | anassrs 469 |
. . . . . 6
β’ (((π β§ π¦ β π·) β§ Β¬ π¦ β (π supp 0 )) β if(π¦ β (π supp 0 ), (πβπ¦), 0 ) = (πβπ¦)) |
24 | 9, 23 | pm2.61dan 812 |
. . . . 5
β’ ((π β§ π¦ β π·) β if(π¦ β (π supp 0 ), (πβπ¦), 0 ) = (πβπ¦)) |
25 | 24 | mpteq2dva 5209 |
. . . 4
β’ (π β (π¦ β π· β¦ if(π¦ β (π supp 0 ), (πβπ¦), 0 )) = (π¦ β π· β¦ (πβπ¦))) |
26 | 7, 25 | eqtr4d 2776 |
. . 3
β’ (π β π = (π¦ β π· β¦ if(π¦ β (π supp 0 ), (πβπ¦), 0 ))) |
27 | | suppssdm 8112 |
. . . . 5
β’ (π supp 0 ) β dom π |
28 | 27, 6 | fssdm 6692 |
. . . 4
β’ (π β (π supp 0 ) β π·) |
29 | | eqid 2733 |
. . . . . . . . 9
β’ (πΌ mPwSer π
) = (πΌ mPwSer π
) |
30 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβ(πΌ
mPwSer π
)) =
(Baseβ(πΌ mPwSer π
)) |
31 | 1, 29, 30, 15, 3 | mplelbas 21422 |
. . . . . . . 8
β’ (π β π΅ β (π β (Baseβ(πΌ mPwSer π
)) β§ π finSupp 0 )) |
32 | 31 | simprbi 498 |
. . . . . . 7
β’ (π β π΅ β π finSupp 0 ) |
33 | 5, 32 | syl 17 |
. . . . . 6
β’ (π β π finSupp 0 ) |
34 | 33 | fsuppimpd 9319 |
. . . . 5
β’ (π β (π supp 0 ) β
Fin) |
35 | | sseq1 3973 |
. . . . . . . 8
β’ (π€ = β
β (π€ β π· β β
β π·)) |
36 | | mpteq1 5202 |
. . . . . . . . . . . 12
β’ (π€ = β
β (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) = (π β β
β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) |
37 | | mpt0 6647 |
. . . . . . . . . . . 12
β’ (π β β
β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) =
β
|
38 | 36, 37 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (π€ = β
β (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) =
β
) |
39 | 38 | oveq2d 7377 |
. . . . . . . . . 10
β’ (π€ = β
β (π Ξ£g
(π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π Ξ£g
β
)) |
40 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0gβπ) = (0gβπ) |
41 | 40 | gsum0 18547 |
. . . . . . . . . 10
β’ (π Ξ£g
β
) = (0gβπ) |
42 | 39, 41 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π€ = β
β (π Ξ£g
(π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) =
(0gβπ)) |
43 | | noel 4294 |
. . . . . . . . . . . 12
β’ Β¬
π¦ β
β
|
44 | | eleq2 2823 |
. . . . . . . . . . . 12
β’ (π€ = β
β (π¦ β π€ β π¦ β β
)) |
45 | 43, 44 | mtbiri 327 |
. . . . . . . . . . 11
β’ (π€ = β
β Β¬ π¦ β π€) |
46 | 45 | iffalsed 4501 |
. . . . . . . . . 10
β’ (π€ = β
β if(π¦ β π€, (πβπ¦), 0 ) = 0 ) |
47 | 46 | mpteq2dv 5211 |
. . . . . . . . 9
β’ (π€ = β
β (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 )) = (π¦ β π· β¦ 0 )) |
48 | 42, 47 | eqeq12d 2749 |
. . . . . . . 8
β’ (π€ = β
β ((π Ξ£g
(π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 )) β
(0gβπ) =
(π¦ β π· β¦ 0 ))) |
49 | 35, 48 | imbi12d 345 |
. . . . . . 7
β’ (π€ = β
β ((π€ β π· β (π Ξ£g (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 ))) β (β
β π· β
(0gβπ) =
(π¦ β π· β¦ 0 )))) |
50 | 49 | imbi2d 341 |
. . . . . 6
β’ (π€ = β
β ((π β (π€ β π· β (π Ξ£g (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 )))) β (π β (β
β π· β
(0gβπ) =
(π¦ β π· β¦ 0 ))))) |
51 | | sseq1 3973 |
. . . . . . . 8
β’ (π€ = π₯ β (π€ β π· β π₯ β π·)) |
52 | | mpteq1 5202 |
. . . . . . . . . 10
β’ (π€ = π₯ β (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) = (π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) |
53 | 52 | oveq2d 7377 |
. . . . . . . . 9
β’ (π€ = π₯ β (π Ξ£g (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π Ξ£g (π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))))) |
54 | | eleq2 2823 |
. . . . . . . . . . 11
β’ (π€ = π₯ β (π¦ β π€ β π¦ β π₯)) |
55 | 54 | ifbid 4513 |
. . . . . . . . . 10
β’ (π€ = π₯ β if(π¦ β π€, (πβπ¦), 0 ) = if(π¦ β π₯, (πβπ¦), 0 )) |
56 | 55 | mpteq2dv 5211 |
. . . . . . . . 9
β’ (π€ = π₯ β (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 )) = (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 ))) |
57 | 53, 56 | eqeq12d 2749 |
. . . . . . . 8
β’ (π€ = π₯ β ((π Ξ£g (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 )) β (π Ξ£g
(π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )))) |
58 | 51, 57 | imbi12d 345 |
. . . . . . 7
β’ (π€ = π₯ β ((π€ β π· β (π Ξ£g (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 ))) β (π₯ β π· β (π Ξ£g (π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 ))))) |
59 | 58 | imbi2d 341 |
. . . . . 6
β’ (π€ = π₯ β ((π β (π€ β π· β (π Ξ£g (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 )))) β (π β (π₯ β π· β (π Ξ£g (π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )))))) |
60 | | sseq1 3973 |
. . . . . . . 8
β’ (π€ = (π₯ βͺ {π§}) β (π€ β π· β (π₯ βͺ {π§}) β π·)) |
61 | | mpteq1 5202 |
. . . . . . . . . 10
β’ (π€ = (π₯ βͺ {π§}) β (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) = (π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) |
62 | 61 | oveq2d 7377 |
. . . . . . . . 9
β’ (π€ = (π₯ βͺ {π§}) β (π Ξ£g (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π Ξ£g (π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))))) |
63 | | eleq2 2823 |
. . . . . . . . . . 11
β’ (π€ = (π₯ βͺ {π§}) β (π¦ β π€ β π¦ β (π₯ βͺ {π§}))) |
64 | 63 | ifbid 4513 |
. . . . . . . . . 10
β’ (π€ = (π₯ βͺ {π§}) β if(π¦ β π€, (πβπ¦), 0 ) = if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 )) |
65 | 64 | mpteq2dv 5211 |
. . . . . . . . 9
β’ (π€ = (π₯ βͺ {π§}) β (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 )) = (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 ))) |
66 | 62, 65 | eqeq12d 2749 |
. . . . . . . 8
β’ (π€ = (π₯ βͺ {π§}) β ((π Ξ£g (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 )) β (π Ξ£g
(π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 )))) |
67 | 60, 66 | imbi12d 345 |
. . . . . . 7
β’ (π€ = (π₯ βͺ {π§}) β ((π€ β π· β (π Ξ£g (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 ))) β ((π₯ βͺ {π§}) β π· β (π Ξ£g (π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 ))))) |
68 | 67 | imbi2d 341 |
. . . . . 6
β’ (π€ = (π₯ βͺ {π§}) β ((π β (π€ β π· β (π Ξ£g (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 )))) β (π β ((π₯ βͺ {π§}) β π· β (π Ξ£g (π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 )))))) |
69 | | sseq1 3973 |
. . . . . . . 8
β’ (π€ = (π supp 0 ) β (π€ β π· β (π supp 0 ) β π·)) |
70 | | mpteq1 5202 |
. . . . . . . . . 10
β’ (π€ = (π supp 0 ) β (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) = (π β (π supp 0 ) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) |
71 | 70 | oveq2d 7377 |
. . . . . . . . 9
β’ (π€ = (π supp 0 ) β (π Ξ£g
(π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π Ξ£g (π β (π supp 0 ) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))))) |
72 | | eleq2 2823 |
. . . . . . . . . . 11
β’ (π€ = (π supp 0 ) β (π¦ β π€ β π¦ β (π supp 0 ))) |
73 | 72 | ifbid 4513 |
. . . . . . . . . 10
β’ (π€ = (π supp 0 ) β if(π¦ β π€, (πβπ¦), 0 ) = if(π¦ β (π supp 0 ), (πβπ¦), 0 )) |
74 | 73 | mpteq2dv 5211 |
. . . . . . . . 9
β’ (π€ = (π supp 0 ) β (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 )) = (π¦ β π· β¦ if(π¦ β (π supp 0 ), (πβπ¦), 0 ))) |
75 | 71, 74 | eqeq12d 2749 |
. . . . . . . 8
β’ (π€ = (π supp 0 ) β ((π Ξ£g
(π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 )) β (π Ξ£g
(π β (π supp 0 ) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π supp 0 ), (πβπ¦), 0 )))) |
76 | 69, 75 | imbi12d 345 |
. . . . . . 7
β’ (π€ = (π supp 0 ) β ((π€ β π· β (π Ξ£g (π β π€ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π€, (πβπ¦), 0 ))) β ((π supp 0 ) β π· β (π Ξ£g (π β (π supp 0 ) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π supp 0 ), (πβπ¦), 0 ))))) |
77 | 76 | imbi2d 341 |
. . . . . 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 19977 |
. . . . . . . . . 10
β’ (π
β Ring β π
β Grp) |
81 | 79, 80 | syl 17 |
. . . . . . . . 9
β’ (π β π
β Grp) |
82 | 1, 4, 15, 40, 78, 81 | mpl0 21435 |
. . . . . . . 8
β’ (π β (0gβπ) = (π· Γ { 0 })) |
83 | | fconstmpt 5698 |
. . . . . . . 8
β’ (π· Γ { 0 }) = (π¦ β π· β¦ 0 ) |
84 | 82, 83 | eqtrdi 2789 |
. . . . . . 7
β’ (π β (0gβπ) = (π¦ β π· β¦ 0 )) |
85 | 84 | a1d 25 |
. . . . . 6
β’ (π β (β
β π· β
(0gβπ) =
(π¦ β π· β¦ 0 ))) |
86 | | ssun1 4136 |
. . . . . . . . . . 11
β’ π₯ β (π₯ βͺ {π§}) |
87 | | sstr2 3955 |
. . . . . . . . . . 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 7368 |
. . . . . . . . . . . 12
β’ ((π Ξ£g
(π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β ((π Ξ£g
(π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0
)))))(+gβπ)((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 )))) = ((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0
))(+gβπ)((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 ))))) |
91 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(+gβπ) = (+gβπ) |
92 | 1 | mplring 21447 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ β π β§ π
β Ring) β π β Ring) |
93 | 78, 79, 92 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β π β Ring) |
94 | | ringcmn 20011 |
. . . . . . . . . . . . . . . 16
β’ (π β Ring β π β CMnd) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β CMnd) |
96 | 95 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β π β CMnd) |
97 | | simprll 778 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β π₯ β Fin) |
98 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π₯ βͺ {π§}) β π·) |
99 | 98 | unssad 4151 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β π₯ β π·) |
100 | 99 | sselda 3948 |
. . . . . . . . . . . . . . 15
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π β π₯) β π β π·) |
101 | 78 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π·) β πΌ β π) |
102 | 79 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π·) β π
β Ring) |
103 | 1 | mpllmod 21446 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΌ β π β§ π
β Ring) β π β LMod) |
104 | 101, 102,
103 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π·) β π β LMod) |
105 | 6 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π·) β (πβπ) β (Baseβπ
)) |
106 | 1, 78, 79 | mplsca 21440 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π
= (Scalarβπ)) |
107 | 106 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π·) β π
= (Scalarβπ)) |
108 | 107 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π·) β (Baseβπ
) = (Baseβ(Scalarβπ))) |
109 | 105, 108 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π·) β (πβπ) β (Baseβ(Scalarβπ))) |
110 | | mplcoe1.o |
. . . . . . . . . . . . . . . . . 18
β’ 1 =
(1rβπ
) |
111 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π·) β π β π·) |
112 | 1, 3, 15, 110, 4, 101, 102, 111 | mplmon 21459 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π·) β (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) β π΅) |
113 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(Scalarβπ) =
(Scalarβπ) |
114 | | mplcoe1.n |
. . . . . . . . . . . . . . . . . 18
β’ Β· = (
Β·π βπ) |
115 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
116 | 3, 113, 114, 115 | lmodvscl 20383 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LMod β§ (πβπ) β (Baseβ(Scalarβπ)) β§ (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) β π΅) β ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) β π΅) |
117 | 104, 109,
112, 116 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) β π΅) |
118 | 117 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π β π·) β ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) β π΅) |
119 | 100, 118 | syldan 592 |
. . . . . . . . . . . . . 14
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π β π₯) β ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) β π΅) |
120 | | vex 3451 |
. . . . . . . . . . . . . . 15
β’ π§ β V |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β π§ β V) |
122 | | simprlr 779 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β Β¬ π§ β π₯) |
123 | 78, 79, 103 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β π β LMod) |
124 | 123 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β π β LMod) |
125 | 6 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β π:π·βΆ(Baseβπ
)) |
126 | 98 | unssbd 4152 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β {π§} β π·) |
127 | 120 | snss 4750 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β π· β {π§} β π·) |
128 | 126, 127 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β π§ β π·) |
129 | 125, 128 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (πβπ§) β (Baseβπ
)) |
130 | 106 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β π
= (Scalarβπ)) |
131 | 130 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (Baseβπ
) = (Baseβ(Scalarβπ))) |
132 | 129, 131 | eleqtrd 2836 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (πβπ§) β (Baseβ(Scalarβπ))) |
133 | 78 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β πΌ β π) |
134 | 79 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β π
β Ring) |
135 | 1, 3, 15, 110, 4, 133, 134, 128 | mplmon 21459 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π¦ β π· β¦ if(π¦ = π§, 1 , 0 )) β π΅) |
136 | 3, 113, 114, 115 | lmodvscl 20383 |
. . . . . . . . . . . . . . 15
β’ ((π β LMod β§ (πβπ§) β (Baseβ(Scalarβπ)) β§ (π¦ β π· β¦ if(π¦ = π§, 1 , 0 )) β π΅) β ((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 ))) β π΅) |
137 | 124, 132,
135, 136 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 ))) β π΅) |
138 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = π§ β (πβπ) = (πβπ§)) |
139 | | equequ2 2030 |
. . . . . . . . . . . . . . . . 17
β’ (π = π§ β (π¦ = π β π¦ = π§)) |
140 | 139 | ifbid 4513 |
. . . . . . . . . . . . . . . 16
β’ (π = π§ β if(π¦ = π, 1 , 0 ) = if(π¦ = π§, 1 , 0 )) |
141 | 140 | mpteq2dv 5211 |
. . . . . . . . . . . . . . 15
β’ (π = π§ β (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) = (π¦ β π· β¦ if(π¦ = π§, 1 , 0 ))) |
142 | 138, 141 | oveq12d 7379 |
. . . . . . . . . . . . . 14
β’ (π = π§ β ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) = ((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 )))) |
143 | 3, 91, 96, 97, 119, 121, 122, 137, 142 | gsumunsn 19745 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π Ξ£g (π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = ((π Ξ£g
(π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0
)))))(+gβπ)((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 ))))) |
144 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(+gβπ
) = (+gβπ
) |
145 | 125 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β (πβπ¦) β (Baseβπ
)) |
146 | 2, 15 | ring0cl 19998 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π
β Ring β 0 β
(Baseβπ
)) |
147 | 79, 146 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 0 β (Baseβπ
)) |
148 | 147 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β 0 β (Baseβπ
)) |
149 | 145, 148 | ifcld 4536 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β if(π¦ β π₯, (πβπ¦), 0 ) β (Baseβπ
)) |
150 | 149 | fmpttd 7067 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )):π·βΆ(Baseβπ
)) |
151 | | fvex 6859 |
. . . . . . . . . . . . . . . . . . 19
β’
(Baseβπ
)
β V |
152 | 151, 13 | elmap 8815 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β
((Baseβπ
)
βm π·)
β (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )):π·βΆ(Baseβπ
)) |
153 | 150, 152 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β
((Baseβπ
)
βm π·)) |
154 | 29, 2, 4, 30, 133 | psrbas 21369 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (Baseβ(πΌ mPwSer π
)) = ((Baseβπ
) βm π·)) |
155 | 153, 154 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β
(Baseβ(πΌ mPwSer π
))) |
156 | 13 | mptex 7177 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β
V |
157 | | funmpt 6543 |
. . . . . . . . . . . . . . . . . . 19
β’ Fun
(π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) |
158 | 156, 157,
16 | 3pm3.2i 1340 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β V β§ Fun
(π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β§ 0 β
V) |
159 | 158 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β V β§ Fun
(π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β§ 0 β
V)) |
160 | | eldifn 4091 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β (π· β π₯) β Β¬ π¦ β π₯) |
161 | 160 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β (π· β π₯)) β Β¬ π¦ β π₯) |
162 | 161 | iffalsed 4501 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β (π· β π₯)) β if(π¦ β π₯, (πβπ¦), 0 ) = 0 ) |
163 | 13 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β π· β V) |
164 | 162, 163 | suppss2 8135 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) supp 0 ) β π₯) |
165 | | suppssfifsupp 9328 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β V β§ Fun
(π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β§ 0 β V)
β§ (π₯ β Fin β§
((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) supp 0 ) β π₯)) β (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) finSupp 0
) |
166 | 159, 97, 164, 165 | syl12anc 836 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) finSupp 0
) |
167 | 1, 29, 30, 15, 3 | mplelbas 21422 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β π΅ β ((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β
(Baseβ(πΌ mPwSer π
)) β§ (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) finSupp 0
)) |
168 | 155, 166,
167 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β π΅) |
169 | 1, 3, 144, 91, 168, 137 | mpladd 21436 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0
))(+gβπ)((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 )))) = ((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) βf
(+gβπ
)((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 ))))) |
170 | | ovexd 7396 |
. . . . . . . . . . . . . . 15
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β ((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 )) β
V) |
171 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) = (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 ))) |
172 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(.rβπ
) = (.rβπ
) |
173 | 1, 114, 2, 3, 172, 4, 129, 135 | mplvsca 21442 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 ))) = ((π· Γ {(πβπ§)}) βf
(.rβπ
)(π¦ β π· β¦ if(π¦ = π§, 1 , 0 )))) |
174 | 129 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β (πβπ§) β (Baseβπ
)) |
175 | 2, 110 | ringidcl 19997 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π
β Ring β 1 β
(Baseβπ
)) |
176 | 175, 146 | ifcld 4536 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
β Ring β if(π¦ = π§, 1 , 0 ) β (Baseβπ
)) |
177 | 79, 176 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β if(π¦ = π§, 1 , 0 ) β (Baseβπ
)) |
178 | 177 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β if(π¦ = π§, 1 , 0 ) β (Baseβπ
)) |
179 | | fconstmpt 5698 |
. . . . . . . . . . . . . . . . . 18
β’ (π· Γ {(πβπ§)}) = (π¦ β π· β¦ (πβπ§)) |
180 | 179 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π· Γ {(πβπ§)}) = (π¦ β π· β¦ (πβπ§))) |
181 | | eqidd 2734 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π¦ β π· β¦ if(π¦ = π§, 1 , 0 )) = (π¦ β π· β¦ if(π¦ = π§, 1 , 0 ))) |
182 | 163, 174,
178, 180, 181 | offval2 7641 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ((π· Γ {(πβπ§)}) βf
(.rβπ
)(π¦ β π· β¦ if(π¦ = π§, 1 , 0 ))) = (π¦ β π· β¦ ((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 )))) |
183 | 173, 182 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 ))) = (π¦ β π· β¦ ((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 )))) |
184 | 163, 149,
170, 171, 183 | offval2 7641 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) βf
(+gβπ
)((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 )))) = (π¦ β π· β¦ (if(π¦ β π₯, (πβπ¦), 0
)(+gβπ
)((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 ))))) |
185 | 134, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β π
β Grp) |
186 | 2, 144, 15 | grplid 18788 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π
β Grp β§ (πβπ§) β (Baseβπ
)) β ( 0 (+gβπ
)(πβπ§)) = (πβπ§)) |
187 | 185, 129,
186 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ( 0 (+gβπ
)(πβπ§)) = (πβπ§)) |
188 | 187 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β ( 0 (+gβπ
)(πβπ§)) = (πβπ§)) |
189 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β π¦ β {π§}) |
190 | | velsn 4606 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β {π§} β π¦ = π§) |
191 | 189, 190 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β π¦ = π§) |
192 | 191 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β (πβπ¦) = (πβπ§)) |
193 | 188, 192 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β ( 0 (+gβπ
)(πβπ§)) = (πβπ¦)) |
194 | 122 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β Β¬ π§ β π₯) |
195 | 191, 194 | eqneltrd 2854 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β Β¬ π¦ β π₯) |
196 | 195 | iffalsed 4501 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β if(π¦ β π₯, (πβπ¦), 0 ) = 0 ) |
197 | 191 | iftrued 4498 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β if(π¦ = π§, 1 , 0 ) = 1 ) |
198 | 197 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β ((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 )) = ((πβπ§)(.rβπ
) 1 )) |
199 | 2, 172, 110 | ringridm 20001 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
β Ring β§ (πβπ§) β (Baseβπ
)) β ((πβπ§)(.rβπ
) 1 ) = (πβπ§)) |
200 | 134, 129,
199 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ((πβπ§)(.rβπ
) 1 ) = (πβπ§)) |
201 | 200 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β ((πβπ§)(.rβπ
) 1 ) = (πβπ§)) |
202 | 198, 201 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β ((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 )) = (πβπ§)) |
203 | 196, 202 | oveq12d 7379 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β (if(π¦ β π₯, (πβπ¦), 0
)(+gβπ
)((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 ))) = ( 0 (+gβπ
)(πβπ§))) |
204 | | elun2 4141 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β {π§} β π¦ β (π₯ βͺ {π§})) |
205 | 204 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β π¦ β (π₯ βͺ {π§})) |
206 | 205 | iftrued 4498 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 ) = (πβπ¦)) |
207 | 193, 203,
206 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ π¦ β {π§}) β (if(π¦ β π₯, (πβπ¦), 0
)(+gβπ
)((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 ))) = if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 )) |
208 | 81 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β π
β Grp) |
209 | 2, 144, 15 | grprid 18789 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π
β Grp β§ if(π¦ β π₯, (πβπ¦), 0 ) β (Baseβπ
)) β (if(π¦ β π₯, (πβπ¦), 0
)(+gβπ
)
0 ) =
if(π¦ β π₯, (πβπ¦), 0 )) |
210 | 208, 149,
209 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β (if(π¦ β π₯, (πβπ¦), 0
)(+gβπ
)
0 ) =
if(π¦ β π₯, (πβπ¦), 0 )) |
211 | 210 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ Β¬ π¦ β {π§}) β (if(π¦ β π₯, (πβπ¦), 0
)(+gβπ
)
0 ) =
if(π¦ β π₯, (πβπ¦), 0 )) |
212 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ Β¬ π¦ β {π§}) β Β¬ π¦ β {π§}) |
213 | 212, 190 | sylnib 328 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ Β¬ π¦ β {π§}) β Β¬ π¦ = π§) |
214 | 213 | iffalsed 4501 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ Β¬ π¦ β {π§}) β if(π¦ = π§, 1 , 0 ) = 0 ) |
215 | 214 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ Β¬ π¦ β {π§}) β ((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 )) = ((πβπ§)(.rβπ
) 0 )) |
216 | 2, 172, 15 | ringrz 20020 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
β Ring β§ (πβπ§) β (Baseβπ
)) β ((πβπ§)(.rβπ
) 0 ) = 0 ) |
217 | 134, 129,
216 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ((πβπ§)(.rβπ
) 0 ) = 0 ) |
218 | 217 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ Β¬ π¦ β {π§}) β ((πβπ§)(.rβπ
) 0 ) = 0 ) |
219 | 215, 218 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ Β¬ π¦ β {π§}) β ((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 )) = 0 ) |
220 | 219 | oveq2d 7377 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ Β¬ π¦ β {π§}) β (if(π¦ β π₯, (πβπ¦), 0
)(+gβπ
)((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 ))) = (if(π¦ β π₯, (πβπ¦), 0
)(+gβπ
)
0
)) |
221 | | elun 4112 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ β (π₯ βͺ {π§}) β (π¦ β π₯ β¨ π¦ β {π§})) |
222 | | orcom 869 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ β π₯ β¨ π¦ β {π§}) β (π¦ β {π§} β¨ π¦ β π₯)) |
223 | 221, 222 | bitri 275 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β (π₯ βͺ {π§}) β (π¦ β {π§} β¨ π¦ β π₯)) |
224 | | biorf 936 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Β¬
π¦ β {π§} β (π¦ β π₯ β (π¦ β {π§} β¨ π¦ β π₯))) |
225 | 223, 224 | bitr4id 290 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
π¦ β {π§} β (π¦ β (π₯ βͺ {π§}) β π¦ β π₯)) |
226 | 225 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ Β¬ π¦ β {π§}) β (π¦ β (π₯ βͺ {π§}) β π¦ β π₯)) |
227 | 226 | ifbid 4513 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ Β¬ π¦ β {π§}) β if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 ) = if(π¦ β π₯, (πβπ¦), 0 )) |
228 | 211, 220,
227 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β§ Β¬ π¦ β {π§}) β (if(π¦ β π₯, (πβπ¦), 0
)(+gβπ
)((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 ))) = if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 )) |
229 | 207, 228 | pm2.61dan 812 |
. . . . . . . . . . . . . . 15
β’ (((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β§ π¦ β π·) β (if(π¦ β π₯, (πβπ¦), 0
)(+gβπ
)((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 ))) = if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 )) |
230 | 229 | mpteq2dva 5209 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π¦ β π· β¦ (if(π¦ β π₯, (πβπ¦), 0
)(+gβπ
)((πβπ§)(.rβπ
)if(π¦ = π§, 1 , 0 )))) = (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 ))) |
231 | 169, 184,
230 | 3eqtrrd 2778 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 )) = ((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0
))(+gβπ)((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 ))))) |
232 | 143, 231 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ((π Ξ£g (π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 )) β ((π Ξ£g
(π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0
)))))(+gβπ)((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 )))) = ((π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0
))(+gβπ)((πβπ§) Β· (π¦ β π· β¦ if(π¦ = π§, 1 , 0 )))))) |
233 | 90, 232 | syl5ibr 246 |
. . . . . . . . . . 11
β’ ((π β§ ((π₯ β Fin β§ Β¬ π§ β π₯) β§ (π₯ βͺ {π§}) β π·)) β ((π Ξ£g (π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β (π Ξ£g
(π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 )))) |
234 | 233 | expr 458 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β Fin β§ Β¬ π§ β π₯)) β ((π₯ βͺ {π§}) β π· β ((π Ξ£g (π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )) β (π Ξ£g
(π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 ))))) |
235 | 234 | a2d 29 |
. . . . . . . . 9
β’ ((π β§ (π₯ β Fin β§ Β¬ π§ β π₯)) β (((π₯ βͺ {π§}) β π· β (π Ξ£g (π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 ))) β ((π₯ βͺ {π§}) β π· β (π Ξ£g (π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 ))))) |
236 | 89, 235 | syl5 34 |
. . . . . . . 8
β’ ((π β§ (π₯ β Fin β§ Β¬ π§ β π₯)) β ((π₯ β π· β (π Ξ£g (π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 ))) β ((π₯ βͺ {π§}) β π· β (π Ξ£g (π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 ))))) |
237 | 236 | expcom 415 |
. . . . . . 7
β’ ((π₯ β Fin β§ Β¬ π§ β π₯) β (π β ((π₯ β π· β (π Ξ£g (π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 ))) β ((π₯ βͺ {π§}) β π· β (π Ξ£g (π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 )))))) |
238 | 237 | a2d 29 |
. . . . . 6
β’ ((π₯ β Fin β§ Β¬ π§ β π₯) β ((π β (π₯ β π· β (π Ξ£g (π β π₯ β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β π₯, (πβπ¦), 0 )))) β (π β ((π₯ βͺ {π§}) β π· β (π Ξ£g (π β (π₯ βͺ {π§}) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π₯ βͺ {π§}), (πβπ¦), 0 )))))) |
239 | 50, 59, 68, 77, 85, 238 | findcard2s 9115 |
. . . . 5
β’ ((π supp 0 ) β Fin β (π β ((π supp 0 ) β π· β (π Ξ£g (π β (π supp 0 ) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π supp 0 ), (πβπ¦), 0 ))))) |
240 | 34, 239 | mpcom 38 |
. . . 4
β’ (π β ((π supp 0 ) β π· β (π Ξ£g (π β (π supp 0 ) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π supp 0 ), (πβπ¦), 0 )))) |
241 | 28, 240 | mpd 15 |
. . 3
β’ (π β (π Ξ£g (π β (π supp 0 ) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π¦ β π· β¦ if(π¦ β (π supp 0 ), (πβπ¦), 0 ))) |
242 | 26, 241 | eqtr4d 2776 |
. 2
β’ (π β π = (π Ξ£g (π β (π supp 0 ) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))))) |
243 | 28 | resmptd 5998 |
. . . 4
β’ (π β ((π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) βΎ (π supp 0 )) = (π β (π supp 0 ) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) |
244 | 243 | oveq2d 7377 |
. . 3
β’ (π β (π Ξ£g ((π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) βΎ (π supp 0 ))) = (π Ξ£g (π β (π supp 0 ) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))))) |
245 | 117 | fmpttd 7067 |
. . . 4
β’ (π β (π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))):π·βΆπ΅) |
246 | 6, 11, 14, 17 | suppssr 8131 |
. . . . . . 7
β’ ((π β§ π β (π· β (π supp 0 ))) β (πβπ) = 0 ) |
247 | 246 | oveq1d 7376 |
. . . . . 6
β’ ((π β§ π β (π· β (π supp 0 ))) β ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) = ( 0 Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) |
248 | | eldifi 4090 |
. . . . . . 7
β’ (π β (π· β (π supp 0 )) β π β π·) |
249 | 107 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (0gβπ
) =
(0gβ(Scalarβπ))) |
250 | 15, 249 | eqtrid 2785 |
. . . . . . . . 9
β’ ((π β§ π β π·) β 0 =
(0gβ(Scalarβπ))) |
251 | 250 | oveq1d 7376 |
. . . . . . . 8
β’ ((π β§ π β π·) β ( 0 Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) =
((0gβ(Scalarβπ)) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) |
252 | | eqid 2733 |
. . . . . . . . . 10
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
253 | 3, 113, 114, 252, 40 | lmod0vs 20399 |
. . . . . . . . 9
β’ ((π β LMod β§ (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) β π΅) β
((0gβ(Scalarβπ)) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) =
(0gβπ)) |
254 | 104, 112,
253 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β π·) β
((0gβ(Scalarβπ)) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) =
(0gβπ)) |
255 | 251, 254 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π β π·) β ( 0 Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) =
(0gβπ)) |
256 | 248, 255 | sylan2 594 |
. . . . . 6
β’ ((π β§ π β (π· β (π supp 0 ))) β ( 0 Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) =
(0gβπ)) |
257 | 247, 256 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π β (π· β (π supp 0 ))) β ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) =
(0gβπ)) |
258 | 257, 14 | suppss2 8135 |
. . . 4
β’ (π β ((π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) supp
(0gβπ))
β (π supp 0
)) |
259 | 13 | mptex 7177 |
. . . . . . 7
β’ (π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) β
V |
260 | | funmpt 6543 |
. . . . . . 7
β’ Fun
(π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) |
261 | | fvex 6859 |
. . . . . . 7
β’
(0gβπ) β V |
262 | 259, 260,
261 | 3pm3.2i 1340 |
. . . . . 6
β’ ((π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) β V β§ Fun
(π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) β§
(0gβπ)
β V) |
263 | 262 | a1i 11 |
. . . . 5
β’ (π β ((π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) β V β§ Fun
(π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) β§
(0gβπ)
β V)) |
264 | | suppssfifsupp 9328 |
. . . . 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βπ)) |
265 | 263, 34, 258, 264 | syl12anc 836 |
. . . 4
β’ (π β (π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) finSupp
(0gβπ)) |
266 | 3, 40, 95, 14, 245, 258, 265 | gsumres 19698 |
. . 3
β’ (π β (π Ξ£g ((π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))) βΎ (π supp 0 ))) = (π Ξ£g (π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))))) |
267 | 244, 266 | eqtr3d 2775 |
. 2
β’ (π β (π Ξ£g (π β (π supp 0 ) β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))))) = (π Ξ£g (π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))))) |
268 | 242, 267 | eqtrd 2773 |
1
β’ (π β π = (π Ξ£g (π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))))) |