Step | Hyp | Ref
| Expression |
1 | | gsumbagdiag.d |
. . . 4
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
2 | | gsumbagdiag.s |
. . . 4
β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} |
3 | | gsumbagdiag.f |
. . . 4
β’ (π β πΉ β π·) |
4 | | gsumbagdiag.b |
. . . 4
β’ π΅ = (BaseβπΊ) |
5 | | gsumbagdiag.g |
. . . 4
β’ (π β πΊ β CMnd) |
6 | 1, 2, 3 | gsumbagdiaglem 21359 |
. . . . 5
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) |
7 | | gsumbagdiag.x |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π΅) |
8 | 7 | anassrs 469 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β π β π΅) |
9 | 8 | fmpttd 7068 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π):{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}βΆπ΅) |
10 | 2 | ssrab3 4045 |
. . . . . . . . . . . 12
β’ π β π· |
11 | 1, 2 | psrbagconcl 21352 |
. . . . . . . . . . . . 13
β’ ((πΉ β π· β§ π β π) β (πΉ βf β π) β π) |
12 | 3, 11 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉ βf β π) β π) |
13 | 10, 12 | sselid 3947 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉ βf β π) β π·) |
14 | | eqid 2737 |
. . . . . . . . . . . 12
β’ {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} = {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} |
15 | 1, 14 | psrbagconf1o 21354 |
. . . . . . . . . . 11
β’ ((πΉ βf β
π) β π· β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ ((πΉ βf β π) βf β
π)):{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}β1-1-ontoβ{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
16 | 13, 15 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ ((πΉ βf β π) βf β
π)):{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}β1-1-ontoβ{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
17 | | f1of 6789 |
. . . . . . . . . 10
β’ ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ ((πΉ βf β π) βf β
π)):{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}β1-1-ontoβ{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ ((πΉ βf β π) βf β
π)):{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}βΆ{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ ((πΉ βf β π) βf β
π)):{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}βΆ{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
19 | 9, 18 | fcod 6699 |
. . . . . . . 8
β’ ((π β§ π β π) β ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ ((πΉ βf β π) βf β
π))):{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}βΆπ΅) |
20 | 3 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β πΉ β π·) |
21 | 20 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β πΉ β π·) |
22 | 1 | psrbagf 21336 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β π· β πΉ:πΌβΆβ0) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β πΉ:πΌβΆβ0) |
24 | 23 | ffvelcdmda 7040 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β§ π§ β πΌ) β (πΉβπ§) β
β0) |
25 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β π β π) |
26 | 10, 25 | sselid 3947 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β π β π·) |
27 | 1 | psrbagf 21336 |
. . . . . . . . . . . . . . . 16
β’ (π β π· β π:πΌβΆβ0) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β π:πΌβΆβ0) |
29 | 28 | ffvelcdmda 7040 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β§ π§ β πΌ) β (πβπ§) β
β0) |
30 | | ssrab2 4042 |
. . . . . . . . . . . . . . . . 17
β’ {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β π· |
31 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
32 | 30, 31 | sselid 3947 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β π β π·) |
33 | 1 | psrbagf 21336 |
. . . . . . . . . . . . . . . 16
β’ (π β π· β π:πΌβΆβ0) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β π:πΌβΆβ0) |
35 | 34 | ffvelcdmda 7040 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β§ π§ β πΌ) β (πβπ§) β
β0) |
36 | | nn0cn 12430 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ§) β β0 β (πΉβπ§) β β) |
37 | | nn0cn 12430 |
. . . . . . . . . . . . . . 15
β’ ((πβπ§) β β0 β (πβπ§) β β) |
38 | | nn0cn 12430 |
. . . . . . . . . . . . . . 15
β’ ((πβπ§) β β0 β (πβπ§) β β) |
39 | | sub32 11442 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ§) β β β§ (πβπ§) β β β§ (πβπ§) β β) β (((πΉβπ§) β (πβπ§)) β (πβπ§)) = (((πΉβπ§) β (πβπ§)) β (πβπ§))) |
40 | 36, 37, 38, 39 | syl3an 1161 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ§) β β0 β§ (πβπ§) β β0 β§ (πβπ§) β β0) β (((πΉβπ§) β (πβπ§)) β (πβπ§)) = (((πΉβπ§) β (πβπ§)) β (πβπ§))) |
41 | 24, 29, 35, 40 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β§ π§ β πΌ) β (((πΉβπ§) β (πβπ§)) β (πβπ§)) = (((πΉβπ§) β (πβπ§)) β (πβπ§))) |
42 | 41 | mpteq2dva 5210 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β (π§ β πΌ β¦ (((πΉβπ§) β (πβπ§)) β (πβπ§))) = (π§ β πΌ β¦ (((πΉβπ§) β (πβπ§)) β (πβπ§)))) |
43 | 34 | ffnd 6674 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β π Fn πΌ) |
44 | 31, 43 | fndmexd 7848 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β πΌ β V) |
45 | | ovexd 7397 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β§ π§ β πΌ) β ((πΉβπ§) β (πβπ§)) β V) |
46 | 23 | feqmptd 6915 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β πΉ = (π§ β πΌ β¦ (πΉβπ§))) |
47 | 28 | feqmptd 6915 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β π = (π§ β πΌ β¦ (πβπ§))) |
48 | 44, 24, 29, 46, 47 | offval2 7642 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β (πΉ βf β π) = (π§ β πΌ β¦ ((πΉβπ§) β (πβπ§)))) |
49 | 34 | feqmptd 6915 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β π = (π§ β πΌ β¦ (πβπ§))) |
50 | 44, 45, 35, 48, 49 | offval2 7642 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β ((πΉ βf β π) βf β
π) = (π§ β πΌ β¦ (((πΉβπ§) β (πβπ§)) β (πβπ§)))) |
51 | | ovexd 7397 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β§ π§ β πΌ) β ((πΉβπ§) β (πβπ§)) β V) |
52 | 44, 24, 35, 46, 49 | offval2 7642 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β (πΉ βf β π) = (π§ β πΌ β¦ ((πΉβπ§) β (πβπ§)))) |
53 | 44, 51, 29, 52, 47 | offval2 7642 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β ((πΉ βf β π) βf β
π) = (π§ β πΌ β¦ (((πΉβπ§) β (πβπ§)) β (πβπ§)))) |
54 | 42, 50, 53 | 3eqtr4d 2787 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β ((πΉ βf β π) βf β
π) = ((πΉ βf β π) βf β
π)) |
55 | 1, 14 | psrbagconcl 21352 |
. . . . . . . . . . . 12
β’ (((πΉ βf β
π) β π· β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β ((πΉ βf β π) βf β
π) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
56 | 13, 55 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β ((πΉ βf β π) βf β
π) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
57 | 54, 56 | eqeltrrd 2839 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β ((πΉ βf β π) βf β
π) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
58 | 54 | mpteq2dva 5210 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ ((πΉ βf β π) βf β
π)) = (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ ((πΉ βf β π) βf β
π))) |
59 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²ππ |
60 | | nfcsb1v 3885 |
. . . . . . . . . . . 12
β’
β²πβ¦π / πβ¦π |
61 | | csbeq1a 3874 |
. . . . . . . . . . . 12
β’ (π = π β π = β¦π / πβ¦π) |
62 | 59, 60, 61 | cbvmpt 5221 |
. . . . . . . . . . 11
β’ (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) = (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ β¦π / πβ¦π) |
63 | 62 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) = (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ β¦π / πβ¦π)) |
64 | | csbeq1 3863 |
. . . . . . . . . 10
β’ (π = ((πΉ βf β π) βf β
π) β
β¦π / πβ¦π = β¦((πΉ βf β π) βf β
π) / πβ¦π) |
65 | 57, 58, 63, 64 | fmptco 7080 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ ((πΉ βf β π) βf β
π))) = (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π)) |
66 | 65 | feq1d 6658 |
. . . . . . . 8
β’ ((π β§ π β π) β (((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ ((πΉ βf β π) βf β
π))):{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}βΆπ΅ β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π):{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}βΆπ΅)) |
67 | 19, 66 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π β π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π):{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}βΆπ΅) |
68 | 67 | fvmptelcdm 7066 |
. . . . . 6
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β
β¦((πΉ
βf β π) βf β π) / πβ¦π β π΅) |
69 | 68 | anasss 468 |
. . . . 5
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β
β¦((πΉ
βf β π) βf β π) / πβ¦π β π΅) |
70 | 6, 69 | syldan 592 |
. . . 4
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β
β¦((πΉ
βf β π) βf β π) / πβ¦π β π΅) |
71 | 1, 2, 3, 4, 5, 70 | gsumbagdiag 21360 |
. . 3
β’ (π β (πΊ Ξ£g (π β π, π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π)) = (πΊ Ξ£g (π β π, π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))) |
72 | | eqid 2737 |
. . . 4
β’
(0gβπΊ) = (0gβπΊ) |
73 | 1 | psrbaglefi 21350 |
. . . . . 6
β’ (πΉ β π· β {π¦ β π· β£ π¦ βr β€ πΉ} β Fin) |
74 | 3, 73 | syl 17 |
. . . . 5
β’ (π β {π¦ β π· β£ π¦ βr β€ πΉ} β Fin) |
75 | 2, 74 | eqeltrid 2842 |
. . . 4
β’ (π β π β Fin) |
76 | 1, 2 | psrbagconcl 21352 |
. . . . . . 7
β’ ((πΉ β π· β§ π β π) β (πΉ βf β π) β π) |
77 | 3, 76 | sylan 581 |
. . . . . 6
β’ ((π β§ π β π) β (πΉ βf β π) β π) |
78 | 10, 77 | sselid 3947 |
. . . . 5
β’ ((π β§ π β π) β (πΉ βf β π) β π·) |
79 | 1 | psrbaglefi 21350 |
. . . . 5
β’ ((πΉ βf β
π) β π· β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β Fin) |
80 | 78, 79 | syl 17 |
. . . 4
β’ ((π β§ π β π) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β Fin) |
81 | | xpfi 9268 |
. . . . 5
β’ ((π β Fin β§ π β Fin) β (π Γ π) β Fin) |
82 | 75, 75, 81 | syl2anc 585 |
. . . 4
β’ (π β (π Γ π) β Fin) |
83 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π) |
84 | 6 | simpld 496 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π) |
85 | | brxp 5686 |
. . . . . . 7
β’ (π(π Γ π)π β (π β π β§ π β π)) |
86 | 83, 84, 85 | sylanbrc 584 |
. . . . . 6
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π(π Γ π)π) |
87 | 86 | pm2.24d 151 |
. . . . 5
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (Β¬ π(π Γ π)π β β¦((πΉ βf β π) βf β
π) / πβ¦π = (0gβπΊ))) |
88 | 87 | impr 456 |
. . . 4
β’ ((π β§ ((π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β§ Β¬ π(π Γ π)π)) β β¦((πΉ βf β π) βf β
π) / πβ¦π = (0gβπΊ)) |
89 | 4, 72, 5, 75, 80, 70, 82, 88 | gsum2d2 19758 |
. . 3
β’ (π β (πΊ Ξ£g (π β π, π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π)) = (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))))) |
90 | 1 | psrbaglefi 21350 |
. . . . 5
β’ ((πΉ βf β
π) β π· β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β Fin) |
91 | 13, 90 | syl 17 |
. . . 4
β’ ((π β§ π β π) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β Fin) |
92 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π) |
93 | 1, 2, 3 | gsumbagdiaglem 21359 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) |
94 | 93 | simpld 496 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π) |
95 | | brxp 5686 |
. . . . . . 7
β’ (π(π Γ π)π β (π β π β§ π β π)) |
96 | 92, 94, 95 | sylanbrc 584 |
. . . . . 6
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π(π Γ π)π) |
97 | 96 | pm2.24d 151 |
. . . . 5
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (Β¬ π(π Γ π)π β β¦((πΉ βf β π) βf β
π) / πβ¦π = (0gβπΊ))) |
98 | 97 | impr 456 |
. . . 4
β’ ((π β§ ((π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β§ Β¬ π(π Γ π)π)) β β¦((πΉ βf β π) βf β
π) / πβ¦π = (0gβπΊ)) |
99 | 4, 72, 5, 75, 91, 69, 82, 98 | gsum2d2 19758 |
. . 3
β’ (π β (πΊ Ξ£g (π β π, π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π)) = (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))))) |
100 | 71, 89, 99 | 3eqtr3d 2785 |
. 2
β’ (π β (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π)))) = (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))))) |
101 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β πΊ β CMnd) |
102 | 70 | anassrs 469 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) β
β¦((πΉ
βf β π) βf β π) / πβ¦π β π΅) |
103 | 102 | fmpttd 7068 |
. . . . . . . 8
β’ ((π β§ π β π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π):{π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}βΆπ΅) |
104 | | ovex 7395 |
. . . . . . . . . . . 12
β’
(β0 βm πΌ) β V |
105 | 1, 104 | rabex2 5296 |
. . . . . . . . . . 11
β’ π· β V |
106 | 105 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π· β V) |
107 | | rabexg 5293 |
. . . . . . . . . 10
β’ (π· β V β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β V) |
108 | | mptexg 7176 |
. . . . . . . . . 10
β’ ({π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β V β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) β V) |
109 | 106, 107,
108 | 3syl 18 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) β V) |
110 | | funmpt 6544 |
. . . . . . . . . 10
β’ Fun
(π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) |
111 | 110 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β π) β Fun (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π)) |
112 | | fvexd 6862 |
. . . . . . . . 9
β’ ((π β§ π β π) β (0gβπΊ) β V) |
113 | | suppssdm 8113 |
. . . . . . . . . . 11
β’ ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) supp (0gβπΊ)) β dom (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) |
114 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) = (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) |
115 | 114 | dmmptss 6198 |
. . . . . . . . . . 11
β’ dom
(π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} |
116 | 113, 115 | sstri 3958 |
. . . . . . . . . 10
β’ ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) supp (0gβπΊ)) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} |
117 | 116 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) supp (0gβπΊ)) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
118 | | suppssfifsupp 9327 |
. . . . . . . . 9
β’ ((((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) β V β§ Fun (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) β§ (0gβπΊ) β V) β§ ({π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β Fin β§ ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) supp (0gβπΊ)) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) finSupp (0gβπΊ)) |
119 | 109, 111,
112, 80, 117, 118 | syl32anc 1379 |
. . . . . . . 8
β’ ((π β§ π β π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π) finSupp (0gβπΊ)) |
120 | 4, 72, 101, 80, 103, 119 | gsumcl 19699 |
. . . . . . 7
β’ ((π β§ π β π) β (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π)) β π΅) |
121 | 120 | fmpttd 7068 |
. . . . . 6
β’ (π β (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))):πβΆπ΅) |
122 | 1, 2 | psrbagconf1o 21354 |
. . . . . . . 8
β’ (πΉ β π· β (π β π β¦ (πΉ βf β π)):πβ1-1-ontoβπ) |
123 | 3, 122 | syl 17 |
. . . . . . 7
β’ (π β (π β π β¦ (πΉ βf β π)):πβ1-1-ontoβπ) |
124 | | f1ocnv 6801 |
. . . . . . 7
β’ ((π β π β¦ (πΉ βf β π)):πβ1-1-ontoβπ β β‘(π β π β¦ (πΉ βf β π)):πβ1-1-ontoβπ) |
125 | | f1of 6789 |
. . . . . . 7
β’ (β‘(π β π β¦ (πΉ βf β π)):πβ1-1-ontoβπ β β‘(π β π β¦ (πΉ βf β π)):πβΆπ) |
126 | 123, 124,
125 | 3syl 18 |
. . . . . 6
β’ (π β β‘(π β π β¦ (πΉ βf β π)):πβΆπ) |
127 | 121, 126 | fcod 6699 |
. . . . 5
β’ (π β ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))) β β‘(π β π β¦ (πΉ βf β π))):πβΆπ΅) |
128 | | coass 6222 |
. . . . . . . 8
β’ (((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β (π β π β¦ (πΉ βf β π))) β β‘(π β π β¦ (πΉ βf β π))) = ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β ((π β π β¦ (πΉ βf β π)) β β‘(π β π β¦ (πΉ βf β π)))) |
129 | | f1ococnv2 6816 |
. . . . . . . . . 10
β’ ((π β π β¦ (πΉ βf β π)):πβ1-1-ontoβπ β ((π β π β¦ (πΉ βf β π)) β β‘(π β π β¦ (πΉ βf β π))) = ( I βΎ π)) |
130 | 123, 129 | syl 17 |
. . . . . . . . 9
β’ (π β ((π β π β¦ (πΉ βf β π)) β β‘(π β π β¦ (πΉ βf β π))) = ( I βΎ π)) |
131 | 130 | coeq2d 5823 |
. . . . . . . 8
β’ (π β ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β ((π β π β¦ (πΉ βf β π)) β β‘(π β π β¦ (πΉ βf β π)))) = ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β ( I βΎ π))) |
132 | 128, 131 | eqtrid 2789 |
. . . . . . 7
β’ (π β (((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β (π β π β¦ (πΉ βf β π))) β β‘(π β π β¦ (πΉ βf β π))) = ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β ( I βΎ π))) |
133 | | eqidd 2738 |
. . . . . . . . 9
β’ (π β (π β π β¦ (πΉ βf β π)) = (π β π β¦ (πΉ βf β π))) |
134 | | eqidd 2738 |
. . . . . . . . 9
β’ (π β (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) = (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π)))) |
135 | | breq2 5114 |
. . . . . . . . . . . 12
β’ (π = (πΉ βf β π) β (π₯ βr β€ π β π₯ βr β€ (πΉ βf β π))) |
136 | 135 | rabbidv 3418 |
. . . . . . . . . . 11
β’ (π = (πΉ βf β π) β {π₯ β π· β£ π₯ βr β€ π} = {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
137 | | ovex 7395 |
. . . . . . . . . . . . 13
β’ (π βf β
π) β
V |
138 | | psrass1lem.y |
. . . . . . . . . . . . 13
β’ (π = (π βf β π) β π = π) |
139 | 137, 138 | csbie 3896 |
. . . . . . . . . . . 12
β’
β¦(π
βf β π) / πβ¦π = π |
140 | | oveq1 7369 |
. . . . . . . . . . . . 13
β’ (π = (πΉ βf β π) β (π βf β π) = ((πΉ βf β π) βf β
π)) |
141 | 140 | csbeq1d 3864 |
. . . . . . . . . . . 12
β’ (π = (πΉ βf β π) β β¦(π βf β
π) / πβ¦π = β¦((πΉ βf β π) βf β
π) / πβ¦π) |
142 | 139, 141 | eqtr3id 2791 |
. . . . . . . . . . 11
β’ (π = (πΉ βf β π) β π = β¦((πΉ βf β π) βf β
π) / πβ¦π) |
143 | 136, 142 | mpteq12dv 5201 |
. . . . . . . . . 10
β’ (π = (πΉ βf β π) β (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π) = (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π)) |
144 | 143 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = (πΉ βf β π) β (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π)) = (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))) |
145 | 77, 133, 134, 144 | fmptco 7080 |
. . . . . . . 8
β’ (π β ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β (π β π β¦ (πΉ βf β π))) = (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π)))) |
146 | 145 | coeq1d 5822 |
. . . . . . 7
β’ (π β (((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β (π β π β¦ (πΉ βf β π))) β β‘(π β π β¦ (πΉ βf β π))) = ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))) β β‘(π β π β¦ (πΉ βf β π)))) |
147 | | coires1 6221 |
. . . . . . . . 9
β’ ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β ( I βΎ π)) = ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) βΎ π) |
148 | | ssid 3971 |
. . . . . . . . . 10
β’ π β π |
149 | | resmpt 5996 |
. . . . . . . . . 10
β’ (π β π β ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) βΎ π) = (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π)))) |
150 | 148, 149 | ax-mp 5 |
. . . . . . . . 9
β’ ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) βΎ π) = (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) |
151 | 147, 150 | eqtri 2765 |
. . . . . . . 8
β’ ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β ( I βΎ π)) = (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) |
152 | 151 | a1i 11 |
. . . . . . 7
β’ (π β ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β ( I βΎ π)) = (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π)))) |
153 | 132, 146,
152 | 3eqtr3d 2785 |
. . . . . 6
β’ (π β ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))) β β‘(π β π β¦ (πΉ βf β π))) = (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π)))) |
154 | 153 | feq1d 6658 |
. . . . 5
β’ (π β (((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))) β β‘(π β π β¦ (πΉ βf β π))):πβΆπ΅ β (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))):πβΆπ΅)) |
155 | 127, 154 | mpbid 231 |
. . . 4
β’ (π β (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))):πβΆπ΅) |
156 | | rabexg 5293 |
. . . . . . . 8
β’ (π· β V β {π¦ β π· β£ π¦ βr β€ πΉ} β V) |
157 | 105, 156 | mp1i 13 |
. . . . . . 7
β’ (π β {π¦ β π· β£ π¦ βr β€ πΉ} β V) |
158 | 2, 157 | eqeltrid 2842 |
. . . . . 6
β’ (π β π β V) |
159 | 158 | mptexd 7179 |
. . . . 5
β’ (π β (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β V) |
160 | | funmpt 6544 |
. . . . . 6
β’ Fun
(π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) |
161 | 160 | a1i 11 |
. . . . 5
β’ (π β Fun (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π)))) |
162 | | fvexd 6862 |
. . . . 5
β’ (π β (0gβπΊ) β V) |
163 | | suppssdm 8113 |
. . . . . . 7
β’ ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) supp (0gβπΊ)) β dom (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) |
164 | | eqid 2737 |
. . . . . . . 8
β’ (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) = (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) |
165 | 164 | dmmptss 6198 |
. . . . . . 7
β’ dom
(π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β π |
166 | 163, 165 | sstri 3958 |
. . . . . 6
β’ ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) supp (0gβπΊ)) β π |
167 | 166 | a1i 11 |
. . . . 5
β’ (π β ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) supp (0gβπΊ)) β π) |
168 | | suppssfifsupp 9327 |
. . . . 5
β’ ((((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β V β§ Fun (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β§ (0gβπΊ) β V) β§ (π β Fin β§ ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) supp (0gβπΊ)) β π)) β (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) finSupp (0gβπΊ)) |
169 | 159, 161,
162, 75, 167, 168 | syl32anc 1379 |
. . . 4
β’ (π β (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) finSupp (0gβπΊ)) |
170 | 4, 72, 5, 75, 155, 169, 123 | gsumf1o 19700 |
. . 3
β’ (π β (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π)))) = (πΊ Ξ£g ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β (π β π β¦ (πΉ βf β π))))) |
171 | 145 | oveq2d 7378 |
. . 3
β’ (π β (πΊ Ξ£g ((π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π))) β (π β π β¦ (πΉ βf β π)))) = (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))))) |
172 | 170, 171 | eqtrd 2777 |
. 2
β’ (π β (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π)))) = (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))))) |
173 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π) β πΊ β CMnd) |
174 | 105 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β π) β π· β V) |
175 | | rabexg 5293 |
. . . . . . . 8
β’ (π· β V β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β V) |
176 | | mptexg 7176 |
. . . . . . . 8
β’ ({π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β V β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) β V) |
177 | 174, 175,
176 | 3syl 18 |
. . . . . . 7
β’ ((π β§ π β π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) β V) |
178 | | funmpt 6544 |
. . . . . . . 8
β’ Fun
(π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) |
179 | 178 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π) β Fun (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π)) |
180 | | fvexd 6862 |
. . . . . . 7
β’ ((π β§ π β π) β (0gβπΊ) β V) |
181 | | suppssdm 8113 |
. . . . . . . . 9
β’ ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) supp (0gβπΊ)) β dom (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) |
182 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) = (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) |
183 | 182 | dmmptss 6198 |
. . . . . . . . 9
β’ dom
(π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} |
184 | 181, 183 | sstri 3958 |
. . . . . . . 8
β’ ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) supp (0gβπΊ)) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} |
185 | 184 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π) β ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) supp (0gβπΊ)) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
186 | | suppssfifsupp 9327 |
. . . . . . 7
β’ ((((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) β V β§ Fun (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) β§ (0gβπΊ) β V) β§ ({π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β Fin β§ ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) supp (0gβπΊ)) β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) finSupp (0gβπΊ)) |
187 | 177, 179,
180, 91, 185, 186 | syl32anc 1379 |
. . . . . 6
β’ ((π β§ π β π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) finSupp (0gβπΊ)) |
188 | 4, 72, 173, 91, 9, 187, 16 | gsumf1o 19700 |
. . . . 5
β’ ((π β§ π β π) β (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π)) = (πΊ Ξ£g ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ ((πΉ βf β π) βf β
π))))) |
189 | 65 | oveq2d 7378 |
. . . . 5
β’ ((π β§ π β π) β (πΊ Ξ£g ((π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π) β (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ ((πΉ βf β π) βf β
π)))) = (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))) |
190 | 188, 189 | eqtrd 2777 |
. . . 4
β’ ((π β§ π β π) β (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π)) = (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))) |
191 | 190 | mpteq2dva 5210 |
. . 3
β’ (π β (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π))) = (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π)))) |
192 | 191 | oveq2d 7378 |
. 2
β’ (π β (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π)))) = (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦
β¦((πΉ
βf β π) βf β π) / πβ¦π))))) |
193 | 100, 172,
192 | 3eqtr4d 2787 |
1
β’ (π β (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π)))) = (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π))))) |