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