Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’ dom π = dom π |
2 | | eqid 2733 |
. . . . 5
β’
(0gβπΊ) = (0gβπΊ) |
3 | | eqid 2733 |
. . . . 5
β’ {β β Xπ β
dom π(πβπ) β£ β finSupp (0gβπΊ)} = {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)} |
4 | 2, 3 | eldprd 19869 |
. . . 4
β’ (dom
π = dom π β (π₯ β (πΊ DProd π) β (πΊdom DProd π β§ βπ β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}π₯ = (πΊ Ξ£g π)))) |
5 | 1, 4 | ax-mp 5 |
. . 3
β’ (π₯ β (πΊ DProd π) β (πΊdom DProd π β§ βπ β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}π₯ = (πΊ Ξ£g π))) |
6 | | dprdssv.b |
. . . . . . 7
β’ π΅ = (BaseβπΊ) |
7 | | eqid 2733 |
. . . . . . 7
β’
(CntzβπΊ) =
(CntzβπΊ) |
8 | | dprdgrp 19870 |
. . . . . . . . 9
β’ (πΊdom DProd π β πΊ β Grp) |
9 | 8 | grpmndd 18829 |
. . . . . . . 8
β’ (πΊdom DProd π β πΊ β Mnd) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((πΊdom DProd π β§ π β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}) β πΊ β Mnd) |
11 | | reldmdprd 19862 |
. . . . . . . . . 10
β’ Rel dom
DProd |
12 | 11 | brrelex2i 5732 |
. . . . . . . . 9
β’ (πΊdom DProd π β π β V) |
13 | 12 | dmexd 7893 |
. . . . . . . 8
β’ (πΊdom DProd π β dom π β V) |
14 | 13 | adantr 482 |
. . . . . . 7
β’ ((πΊdom DProd π β§ π β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}) β dom π β V) |
15 | | simpl 484 |
. . . . . . . 8
β’ ((πΊdom DProd π β§ π β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}) β πΊdom DProd π) |
16 | | eqidd 2734 |
. . . . . . . 8
β’ ((πΊdom DProd π β§ π β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}) β dom π = dom π) |
17 | | simpr 486 |
. . . . . . . 8
β’ ((πΊdom DProd π β§ π β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}) β π β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}) |
18 | 3, 15, 16, 17, 6 | dprdff 19877 |
. . . . . . 7
β’ ((πΊdom DProd π β§ π β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}) β π:dom πβΆπ΅) |
19 | 3, 15, 16, 17, 7 | dprdfcntz 19880 |
. . . . . . 7
β’ ((πΊdom DProd π β§ π β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}) β ran π β ((CntzβπΊ)βran π)) |
20 | 3, 15, 16, 17 | dprdffsupp 19879 |
. . . . . . 7
β’ ((πΊdom DProd π β§ π β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}) β π finSupp (0gβπΊ)) |
21 | 6, 2, 7, 10, 14, 18, 19, 20 | gsumzcl 19774 |
. . . . . 6
β’ ((πΊdom DProd π β§ π β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}) β (πΊ Ξ£g π) β π΅) |
22 | | eleq1 2822 |
. . . . . 6
β’ (π₯ = (πΊ Ξ£g π) β (π₯ β π΅ β (πΊ Ξ£g π) β π΅)) |
23 | 21, 22 | syl5ibrcom 246 |
. . . . 5
β’ ((πΊdom DProd π β§ π β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}) β (π₯ = (πΊ Ξ£g π) β π₯ β π΅)) |
24 | 23 | rexlimdva 3156 |
. . . 4
β’ (πΊdom DProd π β (βπ β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}π₯ = (πΊ Ξ£g π) β π₯ β π΅)) |
25 | 24 | imp 408 |
. . 3
β’ ((πΊdom DProd π β§ βπ β {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπΊ)}π₯ = (πΊ Ξ£g π)) β π₯ β π΅) |
26 | 5, 25 | sylbi 216 |
. 2
β’ (π₯ β (πΊ DProd π) β π₯ β π΅) |
27 | 26 | ssriv 3986 |
1
β’ (πΊ DProd π) β π΅ |