Step | Hyp | Ref
| Expression |
1 | | gsumpt.f |
. . . 4
β’ (π β πΉ:π΄βΆπ΅) |
2 | | gsumpt.x |
. . . . 5
β’ (π β π β π΄) |
3 | 2 | snssd 4773 |
. . . 4
β’ (π β {π} β π΄) |
4 | 1, 3 | feqresmpt 6915 |
. . 3
β’ (π β (πΉ βΎ {π}) = (π β {π} β¦ (πΉβπ))) |
5 | 4 | oveq2d 7377 |
. 2
β’ (π β (πΊ Ξ£g (πΉ βΎ {π})) = (πΊ Ξ£g (π β {π} β¦ (πΉβπ)))) |
6 | | gsumpt.b |
. . 3
β’ π΅ = (BaseβπΊ) |
7 | | gsumpt.z |
. . 3
β’ 0 =
(0gβπΊ) |
8 | | eqid 2733 |
. . 3
β’
(CntzβπΊ) =
(CntzβπΊ) |
9 | | gsumpt.g |
. . 3
β’ (π β πΊ β Mnd) |
10 | | gsumpt.a |
. . 3
β’ (π β π΄ β π) |
11 | 1, 2 | ffvelcdmd 7040 |
. . . . . . . 8
β’ (π β (πΉβπ) β π΅) |
12 | | eqidd 2734 |
. . . . . . . 8
β’ (π β ((πΉβπ)(+gβπΊ)(πΉβπ)) = ((πΉβπ)(+gβπΊ)(πΉβπ))) |
13 | | eqid 2733 |
. . . . . . . . . 10
β’
(+gβπΊ) = (+gβπΊ) |
14 | 6, 13, 8 | elcntzsn 19113 |
. . . . . . . . 9
β’ ((πΉβπ) β π΅ β ((πΉβπ) β ((CntzβπΊ)β{(πΉβπ)}) β ((πΉβπ) β π΅ β§ ((πΉβπ)(+gβπΊ)(πΉβπ)) = ((πΉβπ)(+gβπΊ)(πΉβπ))))) |
15 | 11, 14 | syl 17 |
. . . . . . . 8
β’ (π β ((πΉβπ) β ((CntzβπΊ)β{(πΉβπ)}) β ((πΉβπ) β π΅ β§ ((πΉβπ)(+gβπΊ)(πΉβπ)) = ((πΉβπ)(+gβπΊ)(πΉβπ))))) |
16 | 11, 12, 15 | mpbir2and 712 |
. . . . . . 7
β’ (π β (πΉβπ) β ((CntzβπΊ)β{(πΉβπ)})) |
17 | 16 | snssd 4773 |
. . . . . 6
β’ (π β {(πΉβπ)} β ((CntzβπΊ)β{(πΉβπ)})) |
18 | | eqid 2733 |
. . . . . . 7
β’
(mrClsβ(SubMndβπΊ)) = (mrClsβ(SubMndβπΊ)) |
19 | | eqid 2733 |
. . . . . . 7
β’ (πΊ βΎs
((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) = (πΊ βΎs
((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
20 | 8, 18, 19 | cntzspan 19630 |
. . . . . 6
β’ ((πΊ β Mnd β§ {(πΉβπ)} β ((CntzβπΊ)β{(πΉβπ)})) β (πΊ βΎs
((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) β CMnd) |
21 | 9, 17, 20 | syl2anc 585 |
. . . . 5
β’ (π β (πΊ βΎs
((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) β CMnd) |
22 | 6 | submacs 18645 |
. . . . . . . 8
β’ (πΊ β Mnd β
(SubMndβπΊ) β
(ACSβπ΅)) |
23 | | acsmre 17540 |
. . . . . . . 8
β’
((SubMndβπΊ)
β (ACSβπ΅) β
(SubMndβπΊ) β
(Mooreβπ΅)) |
24 | 9, 22, 23 | 3syl 18 |
. . . . . . 7
β’ (π β (SubMndβπΊ) β (Mooreβπ΅)) |
25 | 11 | snssd 4773 |
. . . . . . 7
β’ (π β {(πΉβπ)} β π΅) |
26 | 18 | mrccl 17499 |
. . . . . . 7
β’
(((SubMndβπΊ)
β (Mooreβπ΅)
β§ {(πΉβπ)} β π΅) β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)}) β (SubMndβπΊ)) |
27 | 24, 25, 26 | syl2anc 585 |
. . . . . 6
β’ (π β
((mrClsβ(SubMndβπΊ))β{(πΉβπ)}) β (SubMndβπΊ)) |
28 | 19, 8 | submcmn2 19625 |
. . . . . 6
β’
(((mrClsβ(SubMndβπΊ))β{(πΉβπ)}) β (SubMndβπΊ) β ((πΊ βΎs
((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) β CMnd β
((mrClsβ(SubMndβπΊ))β{(πΉβπ)}) β ((CntzβπΊ)β((mrClsβ(SubMndβπΊ))β{(πΉβπ)})))) |
29 | 27, 28 | syl 17 |
. . . . 5
β’ (π β ((πΊ βΎs
((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) β CMnd β
((mrClsβ(SubMndβπΊ))β{(πΉβπ)}) β ((CntzβπΊ)β((mrClsβ(SubMndβπΊ))β{(πΉβπ)})))) |
30 | 21, 29 | mpbid 231 |
. . . 4
β’ (π β
((mrClsβ(SubMndβπΊ))β{(πΉβπ)}) β ((CntzβπΊ)β((mrClsβ(SubMndβπΊ))β{(πΉβπ)}))) |
31 | 1 | ffnd 6673 |
. . . . . 6
β’ (π β πΉ Fn π΄) |
32 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ π = π) β π = π) |
33 | 32 | fveq2d 6850 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π = π) β (πΉβπ) = (πΉβπ)) |
34 | 24, 18, 25 | mrcssidd 17513 |
. . . . . . . . . . 11
β’ (π β {(πΉβπ)} β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
35 | | fvex 6859 |
. . . . . . . . . . . 12
β’ (πΉβπ) β V |
36 | 35 | snss 4750 |
. . . . . . . . . . 11
β’ ((πΉβπ) β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)}) β {(πΉβπ)} β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
37 | 34, 36 | sylibr 233 |
. . . . . . . . . 10
β’ (π β (πΉβπ) β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
38 | 37 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π = π) β (πΉβπ) β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
39 | 33, 38 | eqeltrd 2834 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π = π) β (πΉβπ) β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
40 | | eldifsn 4751 |
. . . . . . . . . . 11
β’ (π β (π΄ β {π}) β (π β π΄ β§ π β π)) |
41 | | gsumpt.s |
. . . . . . . . . . . 12
β’ (π β (πΉ supp 0 ) β {π}) |
42 | 7 | fvexi 6860 |
. . . . . . . . . . . . 13
β’ 0 β
V |
43 | 42 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 0 β V) |
44 | 1, 41, 10, 43 | suppssr 8131 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄ β {π})) β (πΉβπ) = 0 ) |
45 | 40, 44 | sylan2br 596 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ π β π)) β (πΉβπ) = 0 ) |
46 | 7 | subm0cl 18630 |
. . . . . . . . . . . 12
β’
(((mrClsβ(SubMndβπΊ))β{(πΉβπ)}) β (SubMndβπΊ) β 0 β
((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
47 | 27, 46 | syl 17 |
. . . . . . . . . . 11
β’ (π β 0 β
((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
48 | 47 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ π β π)) β 0 β
((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
49 | 45, 48 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ π β π)) β (πΉβπ) β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
50 | 49 | anassrs 469 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π β π) β (πΉβπ) β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
51 | 39, 50 | pm2.61dane 3029 |
. . . . . . 7
β’ ((π β§ π β π΄) β (πΉβπ) β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
52 | 51 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ β π΄ (πΉβπ) β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
53 | | ffnfv 7070 |
. . . . . 6
β’ (πΉ:π΄βΆ((mrClsβ(SubMndβπΊ))β{(πΉβπ)}) β (πΉ Fn π΄ β§ βπ β π΄ (πΉβπ) β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)}))) |
54 | 31, 52, 53 | sylanbrc 584 |
. . . . 5
β’ (π β πΉ:π΄βΆ((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
55 | 54 | frnd 6680 |
. . . 4
β’ (π β ran πΉ β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) |
56 | 8 | cntzidss 19126 |
. . . 4
β’
((((mrClsβ(SubMndβπΊ))β{(πΉβπ)}) β ((CntzβπΊ)β((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) β§ ran πΉ β ((mrClsβ(SubMndβπΊ))β{(πΉβπ)})) β ran πΉ β ((CntzβπΊ)βran πΉ)) |
57 | 30, 55, 56 | syl2anc 585 |
. . 3
β’ (π β ran πΉ β ((CntzβπΊ)βran πΉ)) |
58 | 1 | ffund 6676 |
. . . 4
β’ (π β Fun πΉ) |
59 | | snfi 8994 |
. . . . 5
β’ {π} β Fin |
60 | | ssfi 9123 |
. . . . 5
β’ (({π} β Fin β§ (πΉ supp 0 ) β {π}) β (πΉ supp 0 ) β
Fin) |
61 | 59, 41, 60 | sylancr 588 |
. . . 4
β’ (π β (πΉ supp 0 ) β
Fin) |
62 | 1, 10 | fexd 7181 |
. . . . 5
β’ (π β πΉ β V) |
63 | | isfsupp 9315 |
. . . . 5
β’ ((πΉ β V β§ 0 β V)
β (πΉ finSupp 0 β (Fun
πΉ β§ (πΉ supp 0 ) β
Fin))) |
64 | 62, 43, 63 | syl2anc 585 |
. . . 4
β’ (π β (πΉ finSupp 0 β (Fun πΉ β§ (πΉ supp 0 ) β
Fin))) |
65 | 58, 61, 64 | mpbir2and 712 |
. . 3
β’ (π β πΉ finSupp 0 ) |
66 | 6, 7, 8, 9, 10, 1,
57, 41, 65 | gsumzres 19694 |
. 2
β’ (π β (πΊ Ξ£g (πΉ βΎ {π})) = (πΊ Ξ£g πΉ)) |
67 | | fveq2 6846 |
. . . 4
β’ (π = π β (πΉβπ) = (πΉβπ)) |
68 | 6, 67 | gsumsn 19739 |
. . 3
β’ ((πΊ β Mnd β§ π β π΄ β§ (πΉβπ) β π΅) β (πΊ Ξ£g (π β {π} β¦ (πΉβπ))) = (πΉβπ)) |
69 | 9, 2, 11, 68 | syl3anc 1372 |
. 2
β’ (π β (πΊ Ξ£g (π β {π} β¦ (πΉβπ))) = (πΉβπ)) |
70 | 5, 66, 69 | 3eqtr3d 2781 |
1
β’ (π β (πΊ Ξ£g πΉ) = (πΉβπ)) |