Step | Hyp | Ref
| Expression |
1 | | elrspunidl.n |
. . 3
β’ π = (RSpanβπ
) |
2 | | elrspunidl.b |
. . 3
β’ π΅ = (Baseβπ
) |
3 | | elrspunidl.1 |
. . 3
β’ 0 =
(0gβπ
) |
4 | | elrspunidl.x |
. . 3
β’ Β· =
(.rβπ
) |
5 | | elrspunidl.r |
. . 3
β’ (π β π
β Ring) |
6 | | elrspunidl.i |
. . . . . . 7
β’ (π β π β (LIdealβπ
)) |
7 | 6 | sselda 3945 |
. . . . . 6
β’ ((π β§ π β π) β π β (LIdealβπ
)) |
8 | | eqid 2733 |
. . . . . . 7
β’
(LIdealβπ
) =
(LIdealβπ
) |
9 | 2, 8 | lidlss 20696 |
. . . . . 6
β’ (π β (LIdealβπ
) β π β π΅) |
10 | 7, 9 | syl 17 |
. . . . 5
β’ ((π β§ π β π) β π β π΅) |
11 | 10 | ralrimiva 3140 |
. . . 4
β’ (π β βπ β π π β π΅) |
12 | | unissb 4901 |
. . . 4
β’ (βͺ π
β π΅ β
βπ β π π β π΅) |
13 | 11, 12 | sylibr 233 |
. . 3
β’ (π β βͺ π
β π΅) |
14 | 1, 2, 3, 4, 5, 13 | elrsp 32209 |
. 2
β’ (π β (π β (πββͺ π) β βπ β (π΅ βm βͺ π)(π finSupp 0 β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))))) |
15 | | fvexd 6858 |
. . . . . . . . . 10
β’ (π β (LIdealβπ
) β V) |
16 | 15, 6 | ssexd 5282 |
. . . . . . . . 9
β’ (π β π β V) |
17 | 16 | uniexd 7680 |
. . . . . . . 8
β’ (π β βͺ π
β V) |
18 | | eluni2 4870 |
. . . . . . . . . . 11
β’ (π β βͺ π
β βπ β
π π β π) |
19 | 18 | biimpi 215 |
. . . . . . . . . 10
β’ (π β βͺ π
β βπ β
π π β π) |
20 | 19 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β βͺ π) β βπ β π π β π) |
21 | 20 | ralrimiva 3140 |
. . . . . . . 8
β’ (π β βπ β βͺ πβπ β π π β π) |
22 | | eleq2 2823 |
. . . . . . . . 9
β’ (π = (πβπ) β (π β π β π β (πβπ))) |
23 | 22 | ac6sg 10429 |
. . . . . . . 8
β’ (βͺ π
β V β (βπ
β βͺ πβπ β π π β π β βπ(π:βͺ πβΆπ β§ βπ β βͺ ππ β (πβπ)))) |
24 | 17, 21, 23 | sylc 65 |
. . . . . . 7
β’ (π β βπ(π:βͺ πβΆπ β§ βπ β βͺ ππ β (πβπ))) |
25 | 24 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β βπ(π:βͺ πβΆπ β§ βπ β βͺ ππ β (πβπ))) |
26 | | simp-5l 784 |
. . . . . . . . 9
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β π) |
27 | 26 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β π) |
28 | | ringcmn 20008 |
. . . . . . . . . . . 12
β’ (π
β Ring β π
β CMnd) |
29 | 27, 5, 28 | 3syl 18 |
. . . . . . . . . . 11
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β π
β CMnd) |
30 | | vex 3448 |
. . . . . . . . . . . . 13
β’ π β V |
31 | | cnvexg 7862 |
. . . . . . . . . . . . 13
β’ (π β V β β‘π β V) |
32 | | imaexg 7853 |
. . . . . . . . . . . . 13
β’ (β‘π β V β (β‘π β {π}) β V) |
33 | 30, 31, 32 | mp2b 10 |
. . . . . . . . . . . 12
β’ (β‘π β {π}) β V |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (β‘π β {π}) β V) |
35 | 5 | ad7antr 737 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β π
β Ring) |
36 | | elmapi 8790 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ βm βͺ π)
β π:βͺ πβΆπ΅) |
37 | 36 | ad7antlr 738 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β π:βͺ πβΆπ΅) |
38 | | cnvimass 6034 |
. . . . . . . . . . . . . . . . 17
β’ (β‘π β {π}) β dom π |
39 | | fdm 6678 |
. . . . . . . . . . . . . . . . 17
β’ (π:βͺ
πβΆπ β dom π = βͺ π) |
40 | 38, 39 | sseqtrid 3997 |
. . . . . . . . . . . . . . . 16
β’ (π:βͺ
πβΆπ β (β‘π β {π}) β βͺ π) |
41 | 40 | ad3antlr 730 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (β‘π β {π}) β βͺ π) |
42 | 41 | sselda 3945 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β π β βͺ π) |
43 | 37, 42 | ffvelcdmd 7037 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β (πβπ) β π΅) |
44 | 13 | ad7antr 737 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β βͺ π β π΅) |
45 | 44, 42 | sseldd 3946 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β π β π΅) |
46 | 2, 4 | ringcl 19986 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ (πβπ) β π΅ β§ π β π΅) β ((πβπ) Β· π) β π΅) |
47 | 35, 43, 45, 46 | syl3anc 1372 |
. . . . . . . . . . . 12
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β ((πβπ) Β· π) β π΅) |
48 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβπ) = (πβπ)) |
49 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π = π β π = π) |
50 | 48, 49 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (π = π β ((πβπ) Β· π) = ((πβπ) Β· π)) |
51 | 50 | cbvmptv 5219 |
. . . . . . . . . . . 12
β’ (π β (β‘π β {π}) β¦ ((πβπ) Β· π)) = (π β (β‘π β {π}) β¦ ((πβπ) Β· π)) |
52 | 47, 51 | fmptd 7063 |
. . . . . . . . . . 11
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (π β (β‘π β {π}) β¦ ((πβπ) Β· π)):(β‘π β {π})βΆπ΅) |
53 | 34 | mptexd 7175 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (π β (β‘π β {π}) β¦ ((πβπ) Β· π)) β V) |
54 | 52 | ffund 6673 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β Fun (π β (β‘π β {π}) β¦ ((πβπ) Β· π))) |
55 | | simp-5r 785 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β π finSupp 0 ) |
56 | | nfv 1918 |
. . . . . . . . . . . . . . . . 17
β’
β²π((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0
) |
57 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . 19
β’
β²ππ
|
58 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π
Ξ£g |
59 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(π β βͺ π β¦ ((πβπ) Β· π)) |
60 | 57, 58, 59 | nfov 7388 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π))) |
61 | 60 | nfeq2 2921 |
. . . . . . . . . . . . . . . . 17
β’
β²π π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π))) |
62 | 56, 61 | nfan 1903 |
. . . . . . . . . . . . . . . 16
β’
β²π(((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) |
63 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
β’
β²π π:βͺ
πβΆπ |
64 | 62, 63 | nfan 1903 |
. . . . . . . . . . . . . . 15
β’
β²π((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) |
65 | | nfra1 3266 |
. . . . . . . . . . . . . . 15
β’
β²πβπ β βͺ ππ β (πβπ) |
66 | 64, 65 | nfan 1903 |
. . . . . . . . . . . . . 14
β’
β²π(((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) |
67 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π π β π |
68 | 66, 67 | nfan 1903 |
. . . . . . . . . . . . 13
β’
β²π((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) |
69 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π(β‘π β {π}) |
70 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π(π supp 0 ) |
71 | 36 | ad7antlr 738 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β π:βͺ
πβΆπ΅) |
72 | 71 | ffnd 6670 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β π Fn βͺ
π) |
73 | 26, 17 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β βͺ π β V) |
74 | 73 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β βͺ π
β V) |
75 | 3 | fvexi 6857 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
V |
76 | 75 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β 0 β
V) |
77 | 41 | ssdifd 4101 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β ((β‘π β {π}) β (π supp 0 )) β (βͺ π
β (π supp 0
))) |
78 | 77 | sselda 3945 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β π β (βͺ π
β (π supp 0
))) |
79 | 72, 74, 76, 78 | fvdifsupp 31645 |
. . . . . . . . . . . . . . 15
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β (πβπ) = 0 ) |
80 | 79 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β ((πβπ) Β· π) = ( 0 Β· π)) |
81 | 5 | ad7antr 737 |
. . . . . . . . . . . . . . 15
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β π
β Ring) |
82 | 13 | ad7antr 737 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β βͺ π
β π΅) |
83 | 78 | eldifad 3923 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β π β βͺ π) |
84 | 82, 83 | sseldd 3946 |
. . . . . . . . . . . . . . 15
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β π β π΅) |
85 | 2, 4, 3 | ringlz 20016 |
. . . . . . . . . . . . . . 15
β’ ((π
β Ring β§ π β π΅) β ( 0 Β· π) = 0 ) |
86 | 81, 84, 85 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β ( 0 Β· π) = 0 ) |
87 | 80, 86 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β ((πβπ) Β· π) = 0 ) |
88 | 68, 69, 70, 87, 34 | suppss2f 31599 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β ((π β (β‘π β {π}) β¦ ((πβπ) Β· π)) supp 0 ) β (π supp 0 )) |
89 | | fsuppsssupp 9326 |
. . . . . . . . . . . 12
β’ ((((π β (β‘π β {π}) β¦ ((πβπ) Β· π)) β V β§ Fun (π β (β‘π β {π}) β¦ ((πβπ) Β· π))) β§ (π finSupp 0 β§ ((π β (β‘π β {π}) β¦ ((πβπ) Β· π)) supp 0 ) β (π supp 0 ))) β (π β (β‘π β {π}) β¦ ((πβπ) Β· π)) finSupp 0 ) |
90 | 53, 54, 55, 88, 89 | syl22anc 838 |
. . . . . . . . . . 11
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (π β (β‘π β {π}) β¦ ((πβπ) Β· π)) finSupp 0 ) |
91 | 2, 3, 29, 34, 52, 90 | gsumcl 19697 |
. . . . . . . . . 10
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))) β π΅) |
92 | 91 | fmpttd 7064 |
. . . . . . . . 9
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))):πβΆπ΅) |
93 | 2 | fvexi 6857 |
. . . . . . . . . . . 12
β’ π΅ β V |
94 | 93 | a1i 11 |
. . . . . . . . . . 11
β’ (π β π΅ β V) |
95 | 94, 16 | elmapd 8782 |
. . . . . . . . . 10
β’ (π β ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β (π΅ βm π) β (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))):πβΆπ΅)) |
96 | 95 | biimpar 479 |
. . . . . . . . 9
β’ ((π β§ (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))):πβΆπ΅) β (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β (π΅ βm π)) |
97 | 26, 92, 96 | syl2anc 585 |
. . . . . . . 8
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β (π΅ βm π)) |
98 | | breq1 5109 |
. . . . . . . . . 10
β’ (π = (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β (π finSupp 0 β (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) finSupp 0 )) |
99 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π = (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β (π
Ξ£g π) = (π
Ξ£g (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))))) |
100 | 99 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (π = (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β (π = (π
Ξ£g π) β π = (π
Ξ£g (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))))) |
101 | | fveq1 6842 |
. . . . . . . . . . . 12
β’ (π = (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β (πβπ) = ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))βπ)) |
102 | 101 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π = (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β ((πβπ) β π β ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))βπ) β π)) |
103 | 102 | ralbidv 3171 |
. . . . . . . . . 10
β’ (π = (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β (βπ β π (πβπ) β π β βπ β π ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))βπ) β π)) |
104 | 98, 100, 103 | 3anbi123d 1437 |
. . . . . . . . 9
β’ (π = (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β ((π finSupp 0 β§ π = (π
Ξ£g π) β§ βπ β π (πβπ) β π) β ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) finSupp 0 β§ π = (π
Ξ£g (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))) β§ βπ β π ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))βπ) β π))) |
105 | 104 | adantl 483 |
. . . . . . . 8
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π = (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))) β ((π finSupp 0 β§ π = (π
Ξ£g π) β§ βπ β π (πβπ) β π) β ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) finSupp 0 β§ π = (π
Ξ£g (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))) β§ βπ β π ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))βπ) β π))) |
106 | 26, 16 | syl 17 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β π β V) |
107 | 106 | mptexd 7175 |
. . . . . . . . . 10
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β V) |
108 | 75 | a1i 11 |
. . . . . . . . . 10
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β 0 β V) |
109 | | funmpt 6540 |
. . . . . . . . . . 11
β’ Fun
(π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) |
110 | 109 | a1i 11 |
. . . . . . . . . 10
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β Fun (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))) |
111 | | simplr 768 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β π:βͺ πβΆπ) |
112 | 111 | ffund 6673 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β Fun π) |
113 | | simp-4r 783 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β π finSupp 0 ) |
114 | 113 | fsuppimpd 9316 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (π supp 0 ) β
Fin) |
115 | | imafi 9122 |
. . . . . . . . . . . 12
β’ ((Fun
π β§ (π supp 0 ) β Fin) β
(π β (π supp 0 )) β
Fin) |
116 | 112, 114,
115 | syl2anc 585 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (π β (π supp 0 )) β
Fin) |
117 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
β’
β²π π β (π β (π β (π supp 0 ))) |
118 | 66, 117 | nfan 1903 |
. . . . . . . . . . . . . . 15
β’
β²π((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) |
119 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β π:βͺ
πβΆπ) |
120 | 119 | ffund 6673 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β Fun π) |
121 | | snssi 4769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π β (π β (π supp 0 ))) β {π} β (π β (π β (π supp 0 )))) |
122 | 121 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β {π} β (π β (π β (π supp 0 )))) |
123 | | sspreima 7019 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((Fun
π β§ {π} β (π β (π β (π supp 0 )))) β (β‘π β {π}) β (β‘π β (π β (π β (π supp 0 ))))) |
124 | 120, 122,
123 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (β‘π β {π}) β (β‘π β (π β (π β (π supp 0 ))))) |
125 | | difpreima 7016 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Fun
π β (β‘π β (π β (π β (π supp 0 )))) = ((β‘π β π) β (β‘π β (π β (π supp 0 ))))) |
126 | 120, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (β‘π β (π β (π β (π supp 0 )))) = ((β‘π β π) β (β‘π β (π β (π supp 0 ))))) |
127 | 124, 126 | sseqtrd 3985 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (β‘π β {π}) β ((β‘π β π) β (β‘π β (π β (π supp 0 ))))) |
128 | | suppssdm 8109 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π supp 0 ) β dom π |
129 | 36 | ad6antlr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β π:βͺ
πβΆπ΅) |
130 | 128, 129 | fssdm 6689 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (π supp 0 ) β βͺ π) |
131 | 119 | fdmd 6680 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β dom π = βͺ
π) |
132 | 130, 131 | sseqtrrd 3986 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (π supp 0 ) β dom π) |
133 | | sseqin2 4176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π supp 0 ) β dom π β (dom π β© (π supp 0 )) = (π supp 0 )) |
134 | 133 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π supp 0 ) β dom π β (dom π β© (π supp 0 )) = (π supp 0 )) |
135 | | dminss 6106 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (dom
π β© (π supp 0 )) β (β‘π β (π β (π supp 0 ))) |
136 | 134, 135 | eqsstrrdi 4000 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π supp 0 ) β dom π β (π supp 0 ) β (β‘π β (π β (π supp 0 )))) |
137 | 132, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (π supp 0 ) β (β‘π β (π β (π supp 0 )))) |
138 | 137 | sscond 4102 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β ((β‘π β π) β (β‘π β (π β (π supp 0 )))) β ((β‘π β π) β (π supp 0 ))) |
139 | 127, 138 | sstrd 3955 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (β‘π β {π}) β ((β‘π β π) β (π supp 0 ))) |
140 | | fimacnv 6691 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π:βͺ
πβΆπ β (β‘π β π) = βͺ π) |
141 | 119, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (β‘π β π) = βͺ π) |
142 | 141 | difeq1d 4082 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β ((β‘π β π) β (π supp 0 )) = (βͺ π
β (π supp 0
))) |
143 | 139, 142 | sseqtrd 3985 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (β‘π β {π}) β (βͺ
π β (π supp 0 ))) |
144 | 143 | sselda 3945 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β§ π β (β‘π β {π})) β π β (βͺ π β (π supp 0 ))) |
145 | | ssidd 3968 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (π supp 0 ) β (π supp 0 )) |
146 | 73 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β βͺ π
β V) |
147 | 75 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β 0 β
V) |
148 | 129, 145,
146, 147 | suppssr 8128 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β§ π β (βͺ π
β (π supp 0 ))) β
(πβπ) = 0 ) |
149 | 144, 148 | syldan 592 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β§ π β (β‘π β {π})) β (πβπ) = 0 ) |
150 | 149 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β§ π β (β‘π β {π})) β ((πβπ) Β· π) = ( 0 Β· π)) |
151 | 5 | ad7antr 737 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β§ π β (β‘π β {π})) β π
β Ring) |
152 | 13 | ad7antr 737 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β§ π β (β‘π β {π})) β βͺ π β π΅) |
153 | 40 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (β‘π β {π}) β βͺ π) |
154 | 153 | sselda 3945 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β§ π β (β‘π β {π})) β π β βͺ π) |
155 | 152, 154 | sseldd 3946 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β§ π β (β‘π β {π})) β π β π΅) |
156 | 151, 155,
85 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β§ π β (β‘π β {π})) β ( 0 Β· π) = 0 ) |
157 | 150, 156 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β§ π β (β‘π β {π})) β ((πβπ) Β· π) = 0 ) |
158 | 118, 157 | mpteq2da 5204 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (π β (β‘π β {π}) β¦ ((πβπ) Β· π)) = (π β (β‘π β {π}) β¦ 0 )) |
159 | 158 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (π
Ξ£g
(π β (β‘π β {π}) β¦ ((πβπ) Β· π))) = (π
Ξ£g (π β (β‘π β {π}) β¦ 0 ))) |
160 | 5, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π
β CMnd) |
161 | 160 | cmnmndd 19591 |
. . . . . . . . . . . . . . 15
β’ (π β π
β Mnd) |
162 | 161 | ad6antr 735 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β π
β Mnd) |
163 | 3 | gsumz 18651 |
. . . . . . . . . . . . . 14
β’ ((π
β Mnd β§ (β‘π β {π}) β V) β (π
Ξ£g (π β (β‘π β {π}) β¦ 0 )) = 0 ) |
164 | 162, 33, 163 | sylancl 587 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (π
Ξ£g
(π β (β‘π β {π}) β¦ 0 )) = 0 ) |
165 | 159, 164 | eqtrd 2773 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (π β (π β (π supp 0 )))) β (π
Ξ£g
(π β (β‘π β {π}) β¦ ((πβπ) Β· π))) = 0 ) |
166 | 165, 106 | suppss2 8132 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) supp 0 ) β (π β (π supp 0 ))) |
167 | 116, 166 | ssfid 9214 |
. . . . . . . . . 10
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) supp 0 ) β
Fin) |
168 | | isfsupp 9312 |
. . . . . . . . . . 11
β’ (((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β V β§ 0 β V) β ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) finSupp 0 β (Fun (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β§ ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) supp 0 ) β
Fin))) |
169 | 168 | biimpar 479 |
. . . . . . . . . 10
β’ ((((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β V β§ 0 β V) β§ (Fun
(π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) β§ ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) supp 0 ) β Fin)) β
(π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) finSupp 0 ) |
170 | 107, 108,
110, 167, 169 | syl22anc 838 |
. . . . . . . . 9
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) finSupp 0 ) |
171 | | simpllr 775 |
. . . . . . . . . 10
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) |
172 | 26, 160 | syl 17 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β π
β CMnd) |
173 | 5 | ad6antr 735 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β βͺ π) β π
β Ring) |
174 | 36 | ad5antlr 734 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β π:βͺ πβΆπ΅) |
175 | 174 | ffvelcdmda 7036 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β βͺ π) β (πβπ) β π΅) |
176 | 26, 13 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β βͺ π β π΅) |
177 | 176 | sselda 3945 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β βͺ π) β π β π΅) |
178 | 2, 4 | ringcl 19986 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ (πβπ) β π΅ β§ π β π΅) β ((πβπ) Β· π) β π΅) |
179 | 173, 175,
177, 178 | syl3anc 1372 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β βͺ π) β ((πβπ) Β· π) β π΅) |
180 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π β βͺ π
β¦ ((πβπ) Β· π)) = (π β βͺ π β¦ ((πβπ) Β· π)) |
181 | 66, 179, 180 | fmptdf 7066 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (π β βͺ π β¦ ((πβπ) Β· π)):βͺ πβΆπ΅) |
182 | 73 | mptexd 7175 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (π β βͺ π β¦ ((πβπ) Β· π)) β V) |
183 | | funmpt 6540 |
. . . . . . . . . . . . 13
β’ Fun
(π β βͺ π
β¦ ((πβπ) Β· π)) |
184 | 183 | a1i 11 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β Fun (π β βͺ π β¦ ((πβπ) Β· π))) |
185 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²πβͺ π |
186 | 174 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β π:βͺ
πβΆπ΅) |
187 | 186 | ffnd 6670 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β π Fn βͺ
π) |
188 | 73 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β βͺ π
β V) |
189 | 75 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β 0 β
V) |
190 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β π β (βͺ π
β (π supp 0
))) |
191 | 187, 188,
189, 190 | fvdifsupp 31645 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β (πβπ) = 0 ) |
192 | 191 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β ((πβπ) Β· π) = ( 0 Β· π)) |
193 | 5 | ad6antr 735 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β π
β Ring) |
194 | 176 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β βͺ π
β π΅) |
195 | 190 | eldifad 3923 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β π β βͺ π) |
196 | 194, 195 | sseldd 3946 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β π β π΅) |
197 | 193, 196,
85 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β ( 0 Β· π) = 0 ) |
198 | 192, 197 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β (βͺ π β (π supp 0 ))) β ((πβπ) Β· π) = 0 ) |
199 | 66, 185, 70, 198, 73 | suppss2f 31599 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β ((π β βͺ π β¦ ((πβπ) Β· π)) supp 0 ) β (π supp 0 )) |
200 | | fsuppsssupp 9326 |
. . . . . . . . . . . 12
β’ ((((π β βͺ π
β¦ ((πβπ) Β· π)) β V β§ Fun (π β βͺ π β¦ ((πβπ) Β· π))) β§ (π finSupp 0 β§ ((π β βͺ π β¦ ((πβπ) Β· π)) supp 0 ) β (π supp 0 ))) β (π β βͺ π
β¦ ((πβπ) Β· π)) finSupp 0 ) |
201 | 182, 184,
113, 199, 200 | syl22anc 838 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (π β βͺ π β¦ ((πβπ) Β· π)) finSupp 0 ) |
202 | | sndisj 5097 |
. . . . . . . . . . . 12
β’
Disj π β
π {π} |
203 | | disjpreima 31548 |
. . . . . . . . . . . 12
β’ ((Fun
π β§ Disj π β π {π}) β Disj π β π (β‘π β {π})) |
204 | 112, 202,
203 | sylancl 587 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β Disj π β π (β‘π β {π})) |
205 | | iunid 5021 |
. . . . . . . . . . . . 13
β’ βͺ π β π {π} = π |
206 | 205 | imaeq2i 6012 |
. . . . . . . . . . . 12
β’ (β‘π β βͺ
π β π {π}) = (β‘π β π) |
207 | | iunpreima 31529 |
. . . . . . . . . . . . 13
β’ (Fun
π β (β‘π β βͺ
π β π {π}) = βͺ
π β π (β‘π β {π})) |
208 | 112, 207 | syl 17 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (β‘π β βͺ
π β π {π}) = βͺ
π β π (β‘π β {π})) |
209 | 140 | ad2antlr 726 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (β‘π β π) = βͺ π) |
210 | 206, 208,
209 | 3eqtr3a 2797 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β βͺ
π β π (β‘π β {π}) = βͺ π) |
211 | 2, 3, 172, 73, 106, 181, 201, 204, 210 | gsumpart 31946 |
. . . . . . . . . 10
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π))) = (π
Ξ£g (π β π β¦ (π
Ξ£g ((π β βͺ π
β¦ ((πβπ) Β· π)) βΎ (β‘π β {π})))))) |
212 | 41 | resmptd 5995 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β ((π β βͺ π β¦ ((πβπ) Β· π)) βΎ (β‘π β {π})) = (π β (β‘π β {π}) β¦ ((πβπ) Β· π))) |
213 | 212 | oveq2d 7374 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (π
Ξ£g ((π β βͺ π
β¦ ((πβπ) Β· π)) βΎ (β‘π β {π}))) = (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) |
214 | 213 | mpteq2dva 5206 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (π β π β¦ (π
Ξ£g ((π β βͺ π
β¦ ((πβπ) Β· π)) βΎ (β‘π β {π})))) = (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))) |
215 | 214 | oveq2d 7374 |
. . . . . . . . . 10
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β (π
Ξ£g (π β π β¦ (π
Ξ£g ((π β βͺ π
β¦ ((πβπ) Β· π)) βΎ (β‘π β {π}))))) = (π
Ξ£g (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))))) |
216 | 171, 211,
215 | 3eqtrd 2777 |
. . . . . . . . 9
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β π = (π
Ξ£g (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))))) |
217 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) = (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) |
218 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π = π) β π = π) |
219 | 218 | sneqd 4599 |
. . . . . . . . . . . . . . 15
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π = π) β {π} = {π}) |
220 | 219 | imaeq2d 6014 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π = π) β (β‘π β {π}) = (β‘π β {π})) |
221 | 220 | mpteq1d 5201 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π = π) β (π β (β‘π β {π}) β¦ ((πβπ) Β· π)) = (π β (β‘π β {π}) β¦ ((πβπ) Β· π))) |
222 | 221 | oveq2d 7374 |
. . . . . . . . . . . 12
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π = π) β (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))) = (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) |
223 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β π β π) |
224 | | ovexd 7393 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))) β V) |
225 | 217, 222,
223, 224 | fvmptd2 6957 |
. . . . . . . . . . 11
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))βπ) = (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) |
226 | 160 | ad6antr 735 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β π
β CMnd) |
227 | 30 | cnvex 7863 |
. . . . . . . . . . . . . 14
β’ β‘π β V |
228 | 227 | imaex 7854 |
. . . . . . . . . . . . 13
β’ (β‘π β {π}) β V |
229 | 228 | a1i 11 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (β‘π β {π}) β V) |
230 | 5 | ad6antr 735 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β π
β Ring) |
231 | 26, 6 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β π β (LIdealβπ
)) |
232 | 231 | sselda 3945 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β π β (LIdealβπ
)) |
233 | 8 | lidlsubg 20701 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ π β (LIdealβπ
)) β π β (SubGrpβπ
)) |
234 | | subgsubm 18955 |
. . . . . . . . . . . . . 14
β’ (π β (SubGrpβπ
) β π β (SubMndβπ
)) |
235 | 233, 234 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π β (LIdealβπ
)) β π β (SubMndβπ
)) |
236 | 230, 232,
235 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β π β (SubMndβπ
)) |
237 | 230 | adantr 482 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β π
β Ring) |
238 | 232 | adantr 482 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β π β (LIdealβπ
)) |
239 | 36 | ad7antlr 738 |
. . . . . . . . . . . . . . 15
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β π:βͺ πβΆπ΅) |
240 | | cnvimass 6034 |
. . . . . . . . . . . . . . . . . 18
β’ (β‘π β {π}) β dom π |
241 | 240, 39 | sseqtrid 3997 |
. . . . . . . . . . . . . . . . 17
β’ (π:βͺ
πβΆπ β (β‘π β {π}) β βͺ π) |
242 | 241 | ad3antlr 730 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (β‘π β {π}) β βͺ π) |
243 | 242 | sselda 3945 |
. . . . . . . . . . . . . . 15
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β π β βͺ π) |
244 | 239, 243 | ffvelcdmd 7037 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β (πβπ) β π΅) |
245 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πβπ) = (πβπ)) |
246 | 49, 245 | eleq12d 2828 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π β (πβπ) β π β (πβπ))) |
247 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β βπ β βͺ ππ β (πβπ)) |
248 | 246, 247,
243 | rspcdva 3581 |
. . . . . . . . . . . . . . 15
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β π β (πβπ)) |
249 | | simp-4r 783 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β π:βͺ πβΆπ) |
250 | 249 | ffnd 6670 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β π Fn βͺ π) |
251 | | elpreima 7009 |
. . . . . . . . . . . . . . . . . 18
β’ (π Fn βͺ
π β (π β (β‘π β {π}) β (π β βͺ π β§ (πβπ) β {π}))) |
252 | 251 | biimpa 478 |
. . . . . . . . . . . . . . . . 17
β’ ((π Fn βͺ
π β§ π β (β‘π β {π})) β (π β βͺ π β§ (πβπ) β {π})) |
253 | | elsni 4604 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ) β {π} β (πβπ) = π) |
254 | 252, 253 | simpl2im 505 |
. . . . . . . . . . . . . . . 16
β’ ((π Fn βͺ
π β§ π β (β‘π β {π})) β (πβπ) = π) |
255 | 250, 254 | sylancom 589 |
. . . . . . . . . . . . . . 15
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β (πβπ) = π) |
256 | 248, 255 | eleqtrd 2836 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β π β π) |
257 | 8, 2, 4 | lidlmcl 20703 |
. . . . . . . . . . . . . 14
β’ (((π
β Ring β§ π β (LIdealβπ
)) β§ ((πβπ) β π΅ β§ π β π)) β ((πβπ) Β· π) β π) |
258 | 237, 238,
244, 256, 257 | syl22anc 838 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β (β‘π β {π})) β ((πβπ) Β· π) β π) |
259 | 50 | cbvmptv 5219 |
. . . . . . . . . . . . 13
β’ (π β (β‘π β {π}) β¦ ((πβπ) Β· π)) = (π β (β‘π β {π}) β¦ ((πβπ) Β· π)) |
260 | 258, 259 | fmptd 7063 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (π β (β‘π β {π}) β¦ ((πβπ) Β· π)):(β‘π β {π})βΆπ) |
261 | 229 | mptexd 7175 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (π β (β‘π β {π}) β¦ ((πβπ) Β· π)) β V) |
262 | 260 | ffund 6673 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β Fun (π β (β‘π β {π}) β¦ ((πβπ) Β· π))) |
263 | | simp-5r 785 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β π finSupp 0 ) |
264 | | nfv 1918 |
. . . . . . . . . . . . . . 15
β’
β²π π β π |
265 | 66, 264 | nfan 1903 |
. . . . . . . . . . . . . 14
β’
β²π((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) |
266 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π(β‘π β {π}) |
267 | 36 | ad7antlr 738 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β π:βͺ
πβΆπ΅) |
268 | 267 | ffnd 6670 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β π Fn βͺ
π) |
269 | 73 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β βͺ π
β V) |
270 | 75 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β 0 β
V) |
271 | 242 | ssdifd 4101 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β ((β‘π β {π}) β (π supp 0 )) β (βͺ π
β (π supp 0
))) |
272 | 271 | sselda 3945 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β π β (βͺ π
β (π supp 0
))) |
273 | 268, 269,
270, 272 | fvdifsupp 31645 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β (πβπ) = 0 ) |
274 | 273 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β ((πβπ) Β· π) = ( 0 Β· π)) |
275 | 13 | ad7antr 737 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β βͺ π
β π΅) |
276 | 272 | eldifad 3923 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β π β βͺ π) |
277 | 275, 276 | sseldd 3946 |
. . . . . . . . . . . . . . . 16
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β π β π΅) |
278 | 230, 277,
85 | syl2an2r 684 |
. . . . . . . . . . . . . . 15
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β ( 0 Β· π) = 0 ) |
279 | 274, 278 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β§ π β ((β‘π β {π}) β (π supp 0 ))) β ((πβπ) Β· π) = 0 ) |
280 | 265, 266,
70, 279, 229 | suppss2f 31599 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β ((π β (β‘π β {π}) β¦ ((πβπ) Β· π)) supp 0 ) β (π supp 0 )) |
281 | | fsuppsssupp 9326 |
. . . . . . . . . . . . 13
β’ ((((π β (β‘π β {π}) β¦ ((πβπ) Β· π)) β V β§ Fun (π β (β‘π β {π}) β¦ ((πβπ) Β· π))) β§ (π finSupp 0 β§ ((π β (β‘π β {π}) β¦ ((πβπ) Β· π)) supp 0 ) β (π supp 0 ))) β (π β (β‘π β {π}) β¦ ((πβπ) Β· π)) finSupp 0 ) |
282 | 261, 262,
263, 280, 281 | syl22anc 838 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (π β (β‘π β {π}) β¦ ((πβπ) Β· π)) finSupp 0 ) |
283 | 3, 226, 229, 236, 260, 282 | gsumsubmcl 19701 |
. . . . . . . . . . 11
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))) β π) |
284 | 225, 283 | eqeltrd 2834 |
. . . . . . . . . 10
β’
(((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β§ π β π) β ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))βπ) β π) |
285 | 284 | ralrimiva 3140 |
. . . . . . . . 9
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β βπ β π ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))βπ) β π) |
286 | 170, 216,
285 | 3jca 1129 |
. . . . . . . 8
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π)))) finSupp 0 β§ π = (π
Ξ£g (π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))) β§ βπ β π ((π β π β¦ (π
Ξ£g (π β (β‘π β {π}) β¦ ((πβπ) Β· π))))βπ) β π)) |
287 | 97, 105, 286 | rspcedvd 3582 |
. . . . . . 7
β’
((((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ π:βͺ πβΆπ) β§ βπ β βͺ ππ β (πβπ)) β βπ β (π΅ βm π)(π finSupp 0 β§ π = (π
Ξ£g π) β§ βπ β π (πβπ) β π)) |
288 | 287 | anasss 468 |
. . . . . 6
β’
(((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β§ (π:βͺ πβΆπ β§ βπ β βͺ ππ β (πβπ))) β βπ β (π΅ βm π)(π finSupp 0 β§ π = (π
Ξ£g π) β§ βπ β π (πβπ) β π)) |
289 | 25, 288 | exlimddv 1939 |
. . . . 5
β’ ((((π β§ π β (π΅ βm βͺ π))
β§ π finSupp 0 ) β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β βπ β (π΅ βm π)(π finSupp 0 β§ π = (π
Ξ£g π) β§ βπ β π (πβπ) β π)) |
290 | 289 | anasss 468 |
. . . 4
β’ (((π β§ π β (π΅ βm βͺ π))
β§ (π finSupp 0 β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π))))) β βπ β (π΅ βm π)(π finSupp 0 β§ π = (π
Ξ£g π) β§ βπ β π (πβπ) β π)) |
291 | 290 | r19.29an 3152 |
. . 3
β’ ((π β§ βπ β (π΅ βm βͺ π)(π finSupp 0 β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π))))) β βπ β (π΅ βm π)(π finSupp 0 β§ π = (π
Ξ£g π) β§ βπ β π (πβπ) β π)) |
292 | 5 | ad4antr 731 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β π
β Ring) |
293 | 292 | adantr 482 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β π
β Ring) |
294 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(β€RHomβπ
) = (β€RHomβπ
) |
295 | 294 | zrhrhm 20928 |
. . . . . . . . . . . . 13
β’ (π
β Ring β
(β€RHomβπ
)
β (β€ring RingHom π
)) |
296 | | zringbas 20891 |
. . . . . . . . . . . . . 14
β’ β€ =
(Baseββ€ring) |
297 | 296, 2 | rhmf 20165 |
. . . . . . . . . . . . 13
β’
((β€RHomβπ
) β (β€ring RingHom
π
) β
(β€RHomβπ
):β€βΆπ΅) |
298 | 293, 295,
297 | 3syl 18 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β
(β€RHomβπ
):β€βΆπ΅) |
299 | | simp-5r 785 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β π β (π΅ βm π)) |
300 | 75 | a1i 11 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β 0 β
V) |
301 | | ssv 3969 |
. . . . . . . . . . . . . . . . . 18
β’ ran π β V |
302 | | ssdif 4100 |
. . . . . . . . . . . . . . . . . 18
β’ (ran
π β V β (ran
π β { 0 }) β (V
β { 0 })) |
303 | 301, 302 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ (ran
π β { 0 }) β (V
β { 0 }) |
304 | 303 | sseli 3941 |
. . . . . . . . . . . . . . . 16
β’ (π β (ran π β { 0 }) β π β (V β { 0
})) |
305 | 304 | adantl 483 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β π β (V β { 0
})) |
306 | | simp-4r 783 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β π finSupp 0 ) |
307 | 299, 300,
305, 306 | fsuppinisegfi 31648 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β (β‘π β {π}) β Fin) |
308 | | hashcl 14262 |
. . . . . . . . . . . . . 14
β’ ((β‘π β {π}) β Fin β (β―β(β‘π β {π})) β
β0) |
309 | 307, 308 | syl 17 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β
(β―β(β‘π β {π})) β
β0) |
310 | 309 | nn0zd 12530 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β
(β―β(β‘π β {π})) β β€) |
311 | 298, 310 | ffvelcdmd 7037 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β
((β€RHomβπ
)β(β―β(β‘π β {π}))) β π΅) |
312 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) = (π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) |
313 | 311, 312 | fmptd 7063 |
. . . . . . . . . 10
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))):(ran π β { 0 })βΆπ΅) |
314 | 2, 3 | ring0cl 19995 |
. . . . . . . . . . 11
β’ (π
β Ring β 0 β π΅) |
315 | | fconst6g 6732 |
. . . . . . . . . . 11
β’ ( 0 β π΅ β ((βͺ π
β (ran π β {
0 }))
Γ { 0 }):(βͺ π
β (ran π β {
0
}))βΆπ΅) |
316 | 292, 314,
315 | 3syl 18 |
. . . . . . . . . 10
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β ((βͺ π β (ran π β { 0 })) Γ { 0 }):(βͺ π
β (ran π β {
0
}))βΆπ΅) |
317 | | disjdif 4432 |
. . . . . . . . . . 11
β’ ((ran
π β { 0 }) β©
(βͺ π β (ran π β { 0 }))) =
β
|
318 | 317 | a1i 11 |
. . . . . . . . . 10
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β ((ran π β { 0 }) β© (βͺ π
β (ran π β {
0 }))) =
β
) |
319 | 313, 316,
318 | fun2d 6707 |
. . . . . . . . 9
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })):((ran
π β { 0 }) βͺ
(βͺ π β (ran π β { 0 })))βΆπ΅) |
320 | | simplll 774 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (π β§ π β (π΅ βm π))) |
321 | 94, 16 | elmapd 8782 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β (π΅ βm π) β π:πβΆπ΅)) |
322 | 321 | biimpa 478 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΅ βm π)) β π:πβΆπ΅) |
323 | 320, 322 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β π:πβΆπ΅) |
324 | 323 | ffnd 6670 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β π Fn π) |
325 | | elssuni 4899 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β π β βͺ π) |
326 | 325 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ π β π) β π β βͺ π) |
327 | 326 | sseld 3944 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ π β π) β ((πβπ) β π β (πβπ) β βͺ π)) |
328 | 327 | ralimdva 3161 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β (βπ β π (πβπ) β π β βπ β π (πβπ) β βͺ π)) |
329 | 328 | imp 408 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β βπ β π (πβπ) β βͺ π) |
330 | | fnfvrnss 7069 |
. . . . . . . . . . . . 13
β’ ((π Fn π β§ βπ β π (πβπ) β βͺ π) β ran π β βͺ π) |
331 | 324, 329,
330 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β ran π β βͺ π) |
332 | 331 | ssdifssd 4103 |
. . . . . . . . . . 11
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (ran π β { 0 }) β βͺ π) |
333 | | undif 4442 |
. . . . . . . . . . 11
β’ ((ran
π β { 0 }) β
βͺ π β ((ran π β { 0 }) βͺ (βͺ π
β (ran π β {
0 }))) =
βͺ π) |
334 | 332, 333 | sylib 217 |
. . . . . . . . . 10
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β ((ran π β { 0 }) βͺ (βͺ π
β (ran π β {
0 }))) =
βͺ π) |
335 | 334 | feq2d 6655 |
. . . . . . . . 9
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })):((ran
π β { 0 }) βͺ
(βͺ π β (ran π β { 0 })))βΆπ΅ β ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })):βͺ πβΆπ΅)) |
336 | 319, 335 | mpbid 231 |
. . . . . . . 8
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })):βͺ πβΆπ΅) |
337 | 93 | a1i 11 |
. . . . . . . . 9
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β π΅ β V) |
338 | 17 | ad4antr 731 |
. . . . . . . . 9
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β βͺ π β V) |
339 | 337, 338 | elmapd 8782 |
. . . . . . . 8
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β
(π΅ βm βͺ π)
β ((π β (ran
π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })):βͺ πβΆπ΅)) |
340 | 336, 339 | mpbird 257 |
. . . . . . 7
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β
(π΅ βm βͺ π)) |
341 | | breq1 5109 |
. . . . . . . . 9
β’ (π = ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β
(π finSupp 0 β
((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) finSupp
0
)) |
342 | | fveq1 6842 |
. . . . . . . . . . . . 13
β’ (π = ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β
(πβπ) = (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ)) |
343 | 342 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (π = ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β
((πβπ) Β· π) = ((((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π)) |
344 | 343 | mpteq2dv 5208 |
. . . . . . . . . . 11
β’ (π = ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β
(π β βͺ π
β¦ ((πβπ) Β· π)) = (π β βͺ π β¦ ((((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π))) |
345 | 344 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π = ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β
(π
Ξ£g (π β βͺ π β¦ ((πβπ) Β· π))) = (π
Ξ£g (π β βͺ π
β¦ ((((π β (ran
π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π)))) |
346 | 345 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β
(π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π))) β π = (π
Ξ£g (π β βͺ π
β¦ ((((π β (ran
π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π))))) |
347 | 341, 346 | anbi12d 632 |
. . . . . . . 8
β’ (π = ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β
((π finSupp 0 β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) finSupp
0 β§
π = (π
Ξ£g (π β βͺ π
β¦ ((((π β (ran
π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π)))))) |
348 | 347 | adantl 483 |
. . . . . . 7
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π = ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 }))) β
((π finSupp 0 β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) finSupp
0 β§
π = (π
Ξ£g (π β βͺ π
β¦ ((((π β (ran
π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π)))))) |
349 | 319 | ffund 6673 |
. . . . . . . . 9
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β Fun ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))) |
350 | 340 | elexd 3464 |
. . . . . . . . 9
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β
V) |
351 | 75 | a1i 11 |
. . . . . . . . 9
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β 0 β V) |
352 | 323 | ffund 6673 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β Fun π) |
353 | 320 | simprd 497 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β π β (π΅ βm π)) |
354 | | simpllr 775 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β π finSupp 0 ) |
355 | | fsupprnfi 31653 |
. . . . . . . . . . . . 13
β’ (((Fun
π β§ π β (π΅ βm π)) β§ ( 0 β V β§ π finSupp 0 )) β ran π β Fin) |
356 | | diffi 9126 |
. . . . . . . . . . . . 13
β’ (ran
π β Fin β (ran
π β { 0 }) β
Fin) |
357 | 355, 356 | syl 17 |
. . . . . . . . . . . 12
β’ (((Fun
π β§ π β (π΅ βm π)) β§ ( 0 β V β§ π finSupp 0 )) β (ran π β { 0 }) β
Fin) |
358 | 352, 353,
351, 354, 357 | syl22anc 838 |
. . . . . . . . . . 11
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (ran π β { 0 }) β
Fin) |
359 | 313, 358,
351 | fdmfifsupp 9320 |
. . . . . . . . . 10
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) finSupp 0 ) |
360 | 13 | ssdifssd 4103 |
. . . . . . . . . . . . 13
β’ (π β (βͺ π
β (ran π β {
0 }))
β π΅) |
361 | 360 | ad4antr 731 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (βͺ π β (ran π β { 0 })) β π΅) |
362 | 337, 361 | ssexd 5282 |
. . . . . . . . . . 11
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (βͺ π β (ran π β { 0 })) β
V) |
363 | 362, 351 | fczfsuppd 9328 |
. . . . . . . . . 10
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β ((βͺ π β (ran π β { 0 })) Γ { 0 }) finSupp
0
) |
364 | 359, 363 | fsuppun 9329 |
. . . . . . . . 9
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) supp
0 )
β Fin) |
365 | | funisfsupp 9314 |
. . . . . . . . . 10
β’ ((Fun
((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β§
((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β V
β§ 0
β V) β (((π
β (ran π β {
0 })
β¦ ((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) finSupp
0 β
(((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) supp
0 )
β Fin)) |
366 | 365 | biimpar 479 |
. . . . . . . . 9
β’ (((Fun
((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β§
((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) β V
β§ 0
β V) β§ (((π β
(ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) supp
0 )
β Fin) β ((π
β (ran π β {
0 })
β¦ ((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) finSupp
0
) |
367 | 349, 350,
351, 364, 366 | syl31anc 1374 |
. . . . . . . 8
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) finSupp
0
) |
368 | | fvex 6856 |
. . . . . . . . . . . . . . . 16
β’
((β€RHomβπ
)β(β―β(β‘π β {π}))) β V |
369 | 368, 312 | fnmpti 6645 |
. . . . . . . . . . . . . . 15
β’ (π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) Fn (ran π β { 0 }) |
370 | 369 | a1i 11 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β (π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) Fn (ran π β { 0 })) |
371 | | fnconstg 6731 |
. . . . . . . . . . . . . . . 16
β’ ( 0 β V
β ((βͺ π β (ran π β { 0 })) Γ { 0 }) Fn (βͺ π
β (ran π β {
0
}))) |
372 | 75, 371 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ ((βͺ π
β (ran π β {
0 }))
Γ { 0 }) Fn (βͺ π
β (ran π β {
0
})) |
373 | 372 | a1i 11 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β ((βͺ π
β (ran π β {
0 }))
Γ { 0 }) Fn (βͺ π
β (ran π β {
0
}))) |
374 | 317 | a1i 11 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β ((ran π β { 0 }) β© (βͺ π
β (ran π β {
0 }))) =
β
) |
375 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β π β (ran π β { 0 })) |
376 | 370, 373,
374, 375 | fvun1d 6935 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) = ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π}))))βπ)) |
377 | | sneq 4597 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β {π} = {π}) |
378 | 377 | imaeq2d 6014 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (β‘π β {π}) = (β‘π β {π})) |
379 | 378 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β (β―β(β‘π β {π})) = (β―β(β‘π β {π}))) |
380 | 379 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ (π = π β ((β€RHomβπ
)β(β―β(β‘π β {π}))) = ((β€RHomβπ
)β(β―β(β‘π β {π})))) |
381 | | fvexd 6858 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β
((β€RHomβπ
)β(β―β(β‘π β {π}))) β V) |
382 | 312, 380,
375, 381 | fvmptd3 6972 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β ((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π}))))βπ) = ((β€RHomβπ
)β(β―β(β‘π β {π})))) |
383 | 376, 382 | eqtrd 2773 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) =
((β€RHomβπ
)β(β―β(β‘π β {π})))) |
384 | 383 | oveq1d 7373 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β ((((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π) = (((β€RHomβπ
)β(β―β(β‘π β {π}))) Β· π)) |
385 | 384 | mpteq2dva 5206 |
. . . . . . . . . 10
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (π β (ran π β { 0 }) β¦ ((((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π)) = (π β (ran π β { 0 }) β¦
(((β€RHomβπ
)β(β―β(β‘π β {π}))) Β· π))) |
386 | 385 | oveq2d 7374 |
. . . . . . . . 9
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (π
Ξ£g (π β (ran π β { 0 }) β¦ ((((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π))) = (π
Ξ£g (π β (ran π β { 0 }) β¦
(((β€RHomβπ
)β(β―β(β‘π β {π}))) Β· π)))) |
387 | 292, 28 | syl 17 |
. . . . . . . . . 10
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β π
β CMnd) |
388 | 317 | a1i 11 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (βͺ π β (ran π β { 0 }))) β ((ran π β { 0 }) β© (βͺ π
β (ran π β {
0 }))) =
β
) |
389 | | fvun2 6934 |
. . . . . . . . . . . . . . 15
β’ (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) Fn (ran π β { 0 }) β§ ((βͺ π
β (ran π β {
0 }))
Γ { 0 }) Fn (βͺ π
β (ran π β {
0 }))
β§ (((ran π β {
0 })
β© (βͺ π β (ran π β { 0 }))) = β
β§ π β (βͺ π
β (ran π β {
0 }))))
β (((π β (ran
π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) = (((βͺ π
β (ran π β {
0 }))
Γ { 0 })βπ)) |
390 | 369, 372,
389 | mp3an12 1452 |
. . . . . . . . . . . . . 14
β’ ((((ran
π β { 0 }) β©
(βͺ π β (ran π β { 0 }))) = β
β§ π β (βͺ π
β (ran π β {
0 })))
β (((π β (ran
π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) = (((βͺ π
β (ran π β {
0 }))
Γ { 0 })βπ)) |
391 | 388, 390 | sylancom 589 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (βͺ π β (ran π β { 0 }))) β (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) = (((βͺ π
β (ran π β {
0 }))
Γ { 0 })βπ)) |
392 | 75 | fvconst2 7154 |
. . . . . . . . . . . . . 14
β’ (π β (βͺ π
β (ran π β {
0 }))
β (((βͺ π β (ran π β { 0 })) Γ { 0
})βπ) = 0
) |
393 | 392 | adantl 483 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (βͺ π β (ran π β { 0 }))) β (((βͺ π
β (ran π β {
0 }))
Γ { 0 })βπ) = 0 ) |
394 | 391, 393 | eqtrd 2773 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (βͺ π β (ran π β { 0 }))) β (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) = 0
) |
395 | 394 | oveq1d 7373 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (βͺ π β (ran π β { 0 }))) β ((((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π) = ( 0 Β· π)) |
396 | 361 | sselda 3945 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (βͺ π β (ran π β { 0 }))) β π β π΅) |
397 | 292, 396,
85 | syl2an2r 684 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (βͺ π β (ran π β { 0 }))) β ( 0 Β· π) = 0 ) |
398 | 395, 397 | eqtrd 2773 |
. . . . . . . . . 10
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (βͺ π β (ran π β { 0 }))) β ((((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π) = 0 ) |
399 | 292 | adantr 482 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β βͺ π) β π
β Ring) |
400 | 336 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β βͺ π) β (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) β π΅) |
401 | 13 | ad4antr 731 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β βͺ π β π΅) |
402 | 401 | sselda 3945 |
. . . . . . . . . . 11
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β βͺ π) β π β π΅) |
403 | 2, 4 | ringcl 19986 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) β π΅ β§ π β π΅) β ((((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π) β π΅) |
404 | 399, 400,
402, 403 | syl3anc 1372 |
. . . . . . . . . 10
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β βͺ π) β ((((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π) β π΅) |
405 | 2, 3, 387, 338, 398, 358, 404, 332 | gsummptres2 31944 |
. . . . . . . . 9
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (π
Ξ£g (π β βͺ π
β¦ ((((π β (ran
π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π))) = (π
Ξ£g (π β (ran π β { 0 }) β¦ ((((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π)))) |
406 | | eqid 2733 |
. . . . . . . . . . 11
β’
(.gβπ
) = (.gβπ
) |
407 | 2, 3, 406, 387, 323, 354 | gsumhashmul 31947 |
. . . . . . . . . 10
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (π
Ξ£g π) = (π
Ξ£g (π β (ran π β { 0 }) β¦
((β―β(β‘π β {π}))(.gβπ
)π)))) |
408 | | simplr 768 |
. . . . . . . . . 10
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β π = (π
Ξ£g π)) |
409 | 292 | adantr 482 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β π
β Ring) |
410 | 353 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β π β (π΅ βm π)) |
411 | 75 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β 0 β
V) |
412 | 303, 375 | sselid 3943 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β π β (V β { 0
})) |
413 | 354 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β π finSupp 0 ) |
414 | 410, 411,
412, 413 | fsuppinisegfi 31648 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β (β‘π β {π}) β Fin) |
415 | | hashcl 14262 |
. . . . . . . . . . . . . . 15
β’ ((β‘π β {π}) β Fin β (β―β(β‘π β {π})) β
β0) |
416 | 414, 415 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β
(β―β(β‘π β {π})) β
β0) |
417 | 416 | nn0zd 12530 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β
(β―β(β‘π β {π})) β β€) |
418 | 332, 401 | sstrd 3955 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (ran π β { 0 }) β π΅) |
419 | 418 | sselda 3945 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β π β π΅) |
420 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(1rβπ
) = (1rβπ
) |
421 | 294, 406,
420 | zrhmulg 20926 |
. . . . . . . . . . . . . . . 16
β’ ((π
β Ring β§
(β―β(β‘π β {π})) β β€) β
((β€RHomβπ
)β(β―β(β‘π β {π}))) = ((β―β(β‘π β {π}))(.gβπ
)(1rβπ
))) |
422 | 421 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π
β Ring β§
(β―β(β‘π β {π})) β β€) β§ π β π΅) β ((β€RHomβπ
)β(β―β(β‘π β {π}))) = ((β―β(β‘π β {π}))(.gβπ
)(1rβπ
))) |
423 | 422 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (((π
β Ring β§
(β―β(β‘π β {π})) β β€) β§ π β π΅) β (((β€RHomβπ
)β(β―β(β‘π β {π}))) Β· π) = (((β―β(β‘π β {π}))(.gβπ
)(1rβπ
)) Β· π)) |
424 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’ (((π
β Ring β§
(β―β(β‘π β {π})) β β€) β§ π β π΅) β π
β Ring) |
425 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’ (((π
β Ring β§
(β―β(β‘π β {π})) β β€) β§ π β π΅) β (β―β(β‘π β {π})) β β€) |
426 | 2, 420 | ringidcl 19994 |
. . . . . . . . . . . . . . . 16
β’ (π
β Ring β
(1rβπ
)
β π΅) |
427 | 426 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π
β Ring β§
(β―β(β‘π β {π})) β β€) β§ π β π΅) β (1rβπ
) β π΅) |
428 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π
β Ring β§
(β―β(β‘π β {π})) β β€) β§ π β π΅) β π β π΅) |
429 | 2, 406, 4 | mulgass2 20030 |
. . . . . . . . . . . . . . 15
β’ ((π
β Ring β§
((β―β(β‘π β {π})) β β€ β§
(1rβπ
)
β π΅ β§ π β π΅)) β (((β―β(β‘π β {π}))(.gβπ
)(1rβπ
)) Β· π) = ((β―β(β‘π β {π}))(.gβπ
)((1rβπ
) Β· π))) |
430 | 424, 425,
427, 428, 429 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ (((π
β Ring β§
(β―β(β‘π β {π})) β β€) β§ π β π΅) β (((β―β(β‘π β {π}))(.gβπ
)(1rβπ
)) Β· π) = ((β―β(β‘π β {π}))(.gβπ
)((1rβπ
) Β· π))) |
431 | 2, 4, 420 | ringlidm 19997 |
. . . . . . . . . . . . . . . 16
β’ ((π
β Ring β§ π β π΅) β ((1rβπ
) Β· π) = π) |
432 | 424, 431 | sylancom 589 |
. . . . . . . . . . . . . . 15
β’ (((π
β Ring β§
(β―β(β‘π β {π})) β β€) β§ π β π΅) β ((1rβπ
) Β· π) = π) |
433 | 432 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ (((π
β Ring β§
(β―β(β‘π β {π})) β β€) β§ π β π΅) β ((β―β(β‘π β {π}))(.gβπ
)((1rβπ
) Β· π)) = ((β―β(β‘π β {π}))(.gβπ
)π)) |
434 | 423, 430,
433 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π
β Ring β§
(β―β(β‘π β {π})) β β€) β§ π β π΅) β (((β€RHomβπ
)β(β―β(β‘π β {π}))) Β· π) = ((β―β(β‘π β {π}))(.gβπ
)π)) |
435 | 409, 417,
419, 434 | syl21anc 837 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β§ π β (ran π β { 0 })) β
(((β€RHomβπ
)β(β―β(β‘π β {π}))) Β· π) = ((β―β(β‘π β {π}))(.gβπ
)π)) |
436 | 435 | mpteq2dva 5206 |
. . . . . . . . . . 11
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (π β (ran π β { 0 }) β¦
(((β€RHomβπ
)β(β―β(β‘π β {π}))) Β· π)) = (π β (ran π β { 0 }) β¦
((β―β(β‘π β {π}))(.gβπ
)π))) |
437 | 436 | oveq2d 7374 |
. . . . . . . . . 10
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (π
Ξ£g (π β (ran π β { 0 }) β¦
(((β€RHomβπ
)β(β―β(β‘π β {π}))) Β· π))) = (π
Ξ£g (π β (ran π β { 0 }) β¦
((β―β(β‘π β {π}))(.gβπ
)π)))) |
438 | 407, 408,
437 | 3eqtr4d 2783 |
. . . . . . . . 9
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β π = (π
Ξ£g (π β (ran π β { 0 }) β¦
(((β€RHomβπ
)β(β―β(β‘π β {π}))) Β· π)))) |
439 | 386, 405,
438 | 3eqtr4rd 2784 |
. . . . . . . 8
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β π = (π
Ξ£g (π β βͺ π
β¦ ((((π β (ran
π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π)))) |
440 | 367, 439 | jca 513 |
. . . . . . 7
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β (((π β (ran π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0 })) finSupp
0 β§
π = (π
Ξ£g (π β βͺ π
β¦ ((((π β (ran
π β { 0 }) β¦
((β€RHomβπ
)β(β―β(β‘π β {π})))) βͺ ((βͺ
π β (ran π β { 0 })) Γ { 0
}))βπ) Β· π))))) |
441 | 340, 348,
440 | rspcedvd 3582 |
. . . . . 6
β’
(((((π β§ π β (π΅ βm π)) β§ π finSupp 0 ) β§ π = (π
Ξ£g π)) β§ βπ β π (πβπ) β π) β βπ β (π΅ βm βͺ π)(π finSupp 0 β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π))))) |
442 | 441 | exp41 436 |
. . . . 5
β’ ((π β§ π β (π΅ βm π)) β (π finSupp 0 β (π = (π
Ξ£g π) β (βπ β π (πβπ) β π β βπ β (π΅ βm βͺ π)(π finSupp 0 β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))))))) |
443 | 442 | 3imp2 1350 |
. . . 4
β’ (((π β§ π β (π΅ βm π)) β§ (π finSupp 0 β§ π = (π
Ξ£g π) β§ βπ β π (πβπ) β π)) β βπ β (π΅ βm βͺ π)(π finSupp 0 β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π))))) |
444 | 443 | r19.29an 3152 |
. . 3
β’ ((π β§ βπ β (π΅ βm π)(π finSupp 0 β§ π = (π
Ξ£g π) β§ βπ β π (πβπ) β π)) β βπ β (π΅ βm βͺ π)(π finSupp 0 β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π))))) |
445 | 291, 444 | impbida 800 |
. 2
β’ (π β (βπ β (π΅ βm βͺ π)(π finSupp 0 β§ π = (π
Ξ£g (π β βͺ π
β¦ ((πβπ) Β· π)))) β βπ β (π΅ βm π)(π finSupp 0 β§ π = (π
Ξ£g π) β§ βπ β π (πβπ) β π))) |
446 | 14, 445 | bitrd 279 |
1
β’ (π β (π β (πββͺ π) β βπ β (π΅ βm π)(π finSupp 0 β§ π = (π
Ξ£g π) β§ βπ β π (πβπ) β π))) |