Step | Hyp | Ref
| Expression |
1 | | tsmsxp.k |
. . . 4
β’ (π β πΎ β (π« π΄ β© Fin)) |
2 | 1 | elin2d 4160 |
. . 3
β’ (π β πΎ β Fin) |
3 | | elfpw 9301 |
. . . . . . . 8
β’ (πΎ β (π« π΄ β© Fin) β (πΎ β π΄ β§ πΎ β Fin)) |
4 | 3 | simplbi 499 |
. . . . . . 7
β’ (πΎ β (π« π΄ β© Fin) β πΎ β π΄) |
5 | 1, 4 | syl 17 |
. . . . . 6
β’ (π β πΎ β π΄) |
6 | 5 | sselda 3945 |
. . . . 5
β’ ((π β§ π β πΎ) β π β π΄) |
7 | | tsmsxp.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
8 | | tsmsxp.j |
. . . . . 6
β’ π½ = (TopOpenβπΊ) |
9 | | eqid 2733 |
. . . . . 6
β’
(π« πΆ β©
Fin) = (π« πΆ β©
Fin) |
10 | | tsmsxp.g |
. . . . . . 7
β’ (π β πΊ β CMnd) |
11 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΄) β πΊ β CMnd) |
12 | | tsmsxp.2 |
. . . . . . . 8
β’ (π β πΊ β TopGrp) |
13 | | tgptps 23447 |
. . . . . . . 8
β’ (πΊ β TopGrp β πΊ β TopSp) |
14 | 12, 13 | syl 17 |
. . . . . . 7
β’ (π β πΊ β TopSp) |
15 | 14 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΄) β πΊ β TopSp) |
16 | | tsmsxp.c |
. . . . . . 7
β’ (π β πΆ β π) |
17 | 16 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΄) β πΆ β π) |
18 | | tsmsxp.f |
. . . . . . . . 9
β’ (π β πΉ:(π΄ Γ πΆ)βΆπ΅) |
19 | | fovcdm 7525 |
. . . . . . . . 9
β’ ((πΉ:(π΄ Γ πΆ)βΆπ΅ β§ π β π΄ β§ π β πΆ) β (ππΉπ) β π΅) |
20 | 18, 19 | syl3an1 1164 |
. . . . . . . 8
β’ ((π β§ π β π΄ β§ π β πΆ) β (ππΉπ) β π΅) |
21 | 20 | 3expa 1119 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ π β πΆ) β (ππΉπ) β π΅) |
22 | 21 | fmpttd 7064 |
. . . . . 6
β’ ((π β§ π β π΄) β (π β πΆ β¦ (ππΉπ)):πΆβΆπ΅) |
23 | | tsmsxp.1 |
. . . . . 6
β’ ((π β§ π β π΄) β (π»βπ) β (πΊ tsums (π β πΆ β¦ (ππΉπ)))) |
24 | | df-ima 5647 |
. . . . . . . 8
β’ ((π β π΅ β¦ ((π»βπ) β π)) β πΏ) = ran ((π β π΅ β¦ ((π»βπ) β π)) βΎ πΏ) |
25 | 8, 7 | tgptopon 23449 |
. . . . . . . . . . . . 13
β’ (πΊ β TopGrp β π½ β (TopOnβπ΅)) |
26 | 12, 25 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π½ β (TopOnβπ΅)) |
27 | | tsmsxp.l |
. . . . . . . . . . . 12
β’ (π β πΏ β π½) |
28 | | toponss 22292 |
. . . . . . . . . . . 12
β’ ((π½ β (TopOnβπ΅) β§ πΏ β π½) β πΏ β π΅) |
29 | 26, 27, 28 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β πΏ β π΅) |
30 | 29 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β πΏ β π΅) |
31 | 30 | resmptd 5995 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β ((π β π΅ β¦ ((π»βπ) β π)) βΎ πΏ) = (π β πΏ β¦ ((π»βπ) β π))) |
32 | 31 | rneqd 5894 |
. . . . . . . 8
β’ ((π β§ π β π΄) β ran ((π β π΅ β¦ ((π»βπ) β π)) βΎ πΏ) = ran (π β πΏ β¦ ((π»βπ) β π))) |
33 | 24, 32 | eqtrid 2785 |
. . . . . . 7
β’ ((π β§ π β π΄) β ((π β π΅ β¦ ((π»βπ) β π)) β πΏ) = ran (π β πΏ β¦ ((π»βπ) β π))) |
34 | | tsmsxp.h |
. . . . . . . . . . . . 13
β’ (π β π»:π΄βΆπ΅) |
35 | 34 | ffvelcdmda 7036 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β (π»βπ) β π΅) |
36 | | tsmsxp.p |
. . . . . . . . . . . . 13
β’ + =
(+gβπΊ) |
37 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(invgβπΊ) = (invgβπΊ) |
38 | | tsmsxp.m |
. . . . . . . . . . . . 13
β’ β =
(-gβπΊ) |
39 | 7, 36, 37, 38 | grpsubval 18801 |
. . . . . . . . . . . 12
β’ (((π»βπ) β π΅ β§ π β π΅) β ((π»βπ) β π) = ((π»βπ) +
((invgβπΊ)βπ))) |
40 | 35, 39 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ π β π΅) β ((π»βπ) β π) = ((π»βπ) +
((invgβπΊ)βπ))) |
41 | 40 | mpteq2dva 5206 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β (π β π΅ β¦ ((π»βπ) β π)) = (π β π΅ β¦ ((π»βπ) +
((invgβπΊ)βπ)))) |
42 | | tgpgrp 23445 |
. . . . . . . . . . . . . 14
β’ (πΊ β TopGrp β πΊ β Grp) |
43 | 12, 42 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β πΊ β Grp) |
44 | 43 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β πΊ β Grp) |
45 | 7, 37 | grpinvcl 18803 |
. . . . . . . . . . . 12
β’ ((πΊ β Grp β§ π β π΅) β ((invgβπΊ)βπ) β π΅) |
46 | 44, 45 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ π β π΅) β ((invgβπΊ)βπ) β π΅) |
47 | 7, 37 | grpinvf 18802 |
. . . . . . . . . . . . 13
β’ (πΊ β Grp β
(invgβπΊ):π΅βΆπ΅) |
48 | 44, 47 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β (invgβπΊ):π΅βΆπ΅) |
49 | 48 | feqmptd 6911 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (invgβπΊ) = (π β π΅ β¦ ((invgβπΊ)βπ))) |
50 | | eqidd 2734 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (π¦ β π΅ β¦ ((π»βπ) + π¦)) = (π¦ β π΅ β¦ ((π»βπ) + π¦))) |
51 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π¦ = ((invgβπΊ)βπ) β ((π»βπ) + π¦) = ((π»βπ) +
((invgβπΊ)βπ))) |
52 | 46, 49, 50, 51 | fmptco 7076 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β ((π¦ β π΅ β¦ ((π»βπ) + π¦)) β (invgβπΊ)) = (π β π΅ β¦ ((π»βπ) +
((invgβπΊ)βπ)))) |
53 | 41, 52 | eqtr4d 2776 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β (π β π΅ β¦ ((π»βπ) β π)) = ((π¦ β π΅ β¦ ((π»βπ) + π¦)) β (invgβπΊ))) |
54 | 12 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β πΊ β TopGrp) |
55 | 8, 37 | grpinvhmeo 23453 |
. . . . . . . . . . 11
β’ (πΊ β TopGrp β
(invgβπΊ)
β (π½Homeoπ½)) |
56 | 54, 55 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β (invgβπΊ) β (π½Homeoπ½)) |
57 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π¦ β π΅ β¦ ((π»βπ) + π¦)) = (π¦ β π΅ β¦ ((π»βπ) + π¦)) |
58 | 57, 7, 36, 8 | tgplacthmeo 23470 |
. . . . . . . . . . 11
β’ ((πΊ β TopGrp β§ (π»βπ) β π΅) β (π¦ β π΅ β¦ ((π»βπ) + π¦)) β (π½Homeoπ½)) |
59 | 54, 35, 58 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β (π¦ β π΅ β¦ ((π»βπ) + π¦)) β (π½Homeoπ½)) |
60 | | hmeoco 23139 |
. . . . . . . . . 10
β’
(((invgβπΊ) β (π½Homeoπ½) β§ (π¦ β π΅ β¦ ((π»βπ) + π¦)) β (π½Homeoπ½)) β ((π¦ β π΅ β¦ ((π»βπ) + π¦)) β (invgβπΊ)) β (π½Homeoπ½)) |
61 | 56, 59, 60 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β ((π¦ β π΅ β¦ ((π»βπ) + π¦)) β (invgβπΊ)) β (π½Homeoπ½)) |
62 | 53, 61 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π β§ π β π΄) β (π β π΅ β¦ ((π»βπ) β π)) β (π½Homeoπ½)) |
63 | 27 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π΄) β πΏ β π½) |
64 | | hmeoima 23132 |
. . . . . . . 8
β’ (((π β π΅ β¦ ((π»βπ) β π)) β (π½Homeoπ½) β§ πΏ β π½) β ((π β π΅ β¦ ((π»βπ) β π)) β πΏ) β π½) |
65 | 62, 63, 64 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β π΄) β ((π β π΅ β¦ ((π»βπ) β π)) β πΏ) β π½) |
66 | 33, 65 | eqeltrrd 2835 |
. . . . . 6
β’ ((π β§ π β π΄) β ran (π β πΏ β¦ ((π»βπ) β π)) β π½) |
67 | | tsmsxp.z |
. . . . . . . . 9
β’ 0 =
(0gβπΊ) |
68 | 7, 67, 38 | grpsubid1 18837 |
. . . . . . . 8
β’ ((πΊ β Grp β§ (π»βπ) β π΅) β ((π»βπ) β 0 ) = (π»βπ)) |
69 | 44, 35, 68 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β π΄) β ((π»βπ) β 0 ) = (π»βπ)) |
70 | | tsmsxp.3 |
. . . . . . . . 9
β’ (π β 0 β πΏ) |
71 | 70 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π΄) β 0 β πΏ) |
72 | | ovex 7391 |
. . . . . . . 8
β’ ((π»βπ) β 0 ) β
V |
73 | | eqid 2733 |
. . . . . . . . 9
β’ (π β πΏ β¦ ((π»βπ) β π)) = (π β πΏ β¦ ((π»βπ) β π)) |
74 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = 0 β ((π»βπ) β π) = ((π»βπ) β 0 )) |
75 | 73, 74 | elrnmpt1s 5913 |
. . . . . . . 8
β’ (( 0 β πΏ β§ ((π»βπ) β 0 ) β V) β ((π»βπ) β 0 ) β ran (π β πΏ β¦ ((π»βπ) β π))) |
76 | 71, 72, 75 | sylancl 587 |
. . . . . . 7
β’ ((π β§ π β π΄) β ((π»βπ) β 0 ) β ran (π β πΏ β¦ ((π»βπ) β π))) |
77 | 69, 76 | eqeltrrd 2835 |
. . . . . 6
β’ ((π β§ π β π΄) β (π»βπ) β ran (π β πΏ β¦ ((π»βπ) β π))) |
78 | 7, 8, 9, 11, 15, 17, 22, 23, 66, 77 | tsmsi 23501 |
. . . . 5
β’ ((π β§ π β π΄) β βπ¦ β (π« πΆ β© Fin)βπ§ β (π« πΆ β© Fin)(π¦ β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π)))) |
79 | 6, 78 | syldan 592 |
. . . 4
β’ ((π β§ π β πΎ) β βπ¦ β (π« πΆ β© Fin)βπ§ β (π« πΆ β© Fin)(π¦ β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π)))) |
80 | 79 | ralrimiva 3140 |
. . 3
β’ (π β βπ β πΎ βπ¦ β (π« πΆ β© Fin)βπ§ β (π« πΆ β© Fin)(π¦ β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π)))) |
81 | | sseq1 3970 |
. . . . . 6
β’ (π¦ = (πβπ) β (π¦ β π§ β (πβπ) β π§)) |
82 | 81 | imbi1d 342 |
. . . . 5
β’ (π¦ = (πβπ) β ((π¦ β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))) β ((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))))) |
83 | 82 | ralbidv 3171 |
. . . 4
β’ (π¦ = (πβπ) β (βπ§ β (π« πΆ β© Fin)(π¦ β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))) β βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))))) |
84 | 83 | ac6sfi 9234 |
. . 3
β’ ((πΎ β Fin β§ βπ β πΎ βπ¦ β (π« πΆ β© Fin)βπ§ β (π« πΆ β© Fin)(π¦ β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π)))) β βπ(π:πΎβΆ(π« πΆ β© Fin) β§ βπ β πΎ βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))))) |
85 | 2, 80, 84 | syl2anc 585 |
. 2
β’ (π β βπ(π:πΎβΆ(π« πΆ β© Fin) β§ βπ β πΎ βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))))) |
86 | | frn 6676 |
. . . . . . . . 9
β’ (π:πΎβΆ(π« πΆ β© Fin) β ran π β (π« πΆ β© Fin)) |
87 | 86 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β ran π β (π« πΆ β© Fin)) |
88 | | inss1 4189 |
. . . . . . . 8
β’
(π« πΆ β©
Fin) β π« πΆ |
89 | 87, 88 | sstrdi 3957 |
. . . . . . 7
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β ran π β π« πΆ) |
90 | | sspwuni 5061 |
. . . . . . 7
β’ (ran
π β π« πΆ β βͺ ran π β πΆ) |
91 | 89, 90 | sylib 217 |
. . . . . 6
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β βͺ ran π β πΆ) |
92 | | tsmsxp.d |
. . . . . . . . 9
β’ (π β π· β (π« (π΄ Γ πΆ) β© Fin)) |
93 | | elfpw 9301 |
. . . . . . . . . 10
β’ (π· β (π« (π΄ Γ πΆ) β© Fin) β (π· β (π΄ Γ πΆ) β§ π· β Fin)) |
94 | 93 | simplbi 499 |
. . . . . . . . 9
β’ (π· β (π« (π΄ Γ πΆ) β© Fin) β π· β (π΄ Γ πΆ)) |
95 | | rnss 5895 |
. . . . . . . . 9
β’ (π· β (π΄ Γ πΆ) β ran π· β ran (π΄ Γ πΆ)) |
96 | 92, 94, 95 | 3syl 18 |
. . . . . . . 8
β’ (π β ran π· β ran (π΄ Γ πΆ)) |
97 | | rnxpss 6125 |
. . . . . . . 8
β’ ran
(π΄ Γ πΆ) β πΆ |
98 | 96, 97 | sstrdi 3957 |
. . . . . . 7
β’ (π β ran π· β πΆ) |
99 | 98 | adantr 482 |
. . . . . 6
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β ran π· β πΆ) |
100 | 91, 99 | unssd 4147 |
. . . . 5
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β (βͺ ran π βͺ ran π·) β πΆ) |
101 | 2 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β πΎ β Fin) |
102 | | ffn 6669 |
. . . . . . . . . 10
β’ (π:πΎβΆ(π« πΆ β© Fin) β π Fn πΎ) |
103 | 102 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β π Fn πΎ) |
104 | | dffn4 6763 |
. . . . . . . . 9
β’ (π Fn πΎ β π:πΎβontoβran π) |
105 | 103, 104 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β π:πΎβontoβran π) |
106 | | fofi 9285 |
. . . . . . . 8
β’ ((πΎ β Fin β§ π:πΎβontoβran π) β ran π β Fin) |
107 | 101, 105,
106 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β ran π β Fin) |
108 | | inss2 4190 |
. . . . . . . 8
β’
(π« πΆ β©
Fin) β Fin |
109 | 87, 108 | sstrdi 3957 |
. . . . . . 7
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β ran π β Fin) |
110 | | unifi 9288 |
. . . . . . 7
β’ ((ran
π β Fin β§ ran
π β Fin) β βͺ ran π β Fin) |
111 | 107, 109,
110 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β βͺ ran π β Fin) |
112 | | elinel2 4157 |
. . . . . . . 8
β’ (π· β (π« (π΄ Γ πΆ) β© Fin) β π· β Fin) |
113 | | rnfi 9282 |
. . . . . . . 8
β’ (π· β Fin β ran π· β Fin) |
114 | 92, 112, 113 | 3syl 18 |
. . . . . . 7
β’ (π β ran π· β Fin) |
115 | 114 | adantr 482 |
. . . . . 6
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β ran π· β Fin) |
116 | | unfi 9119 |
. . . . . 6
β’ ((βͺ ran π β Fin β§ ran π· β Fin) β (βͺ ran π βͺ ran π·) β Fin) |
117 | 111, 115,
116 | syl2anc 585 |
. . . . 5
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β (βͺ ran π βͺ ran π·) β Fin) |
118 | | elfpw 9301 |
. . . . 5
β’ ((βͺ ran π βͺ ran π·) β (π« πΆ β© Fin) β ((βͺ ran π βͺ ran π·) β πΆ β§ (βͺ ran
π βͺ ran π·) β Fin)) |
119 | 100, 117,
118 | sylanbrc 584 |
. . . 4
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β (βͺ ran π βͺ ran π·) β (π« πΆ β© Fin)) |
120 | 119 | adantrr 716 |
. . 3
β’ ((π β§ (π:πΎβΆ(π« πΆ β© Fin) β§ βπ β πΎ βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))))) β (βͺ
ran π βͺ ran π·) β (π« πΆ β© Fin)) |
121 | | ssun2 4134 |
. . . 4
β’ ran π· β (βͺ ran π βͺ ran π·) |
122 | 121 | a1i 11 |
. . 3
β’ ((π β§ (π:πΎβΆ(π« πΆ β© Fin) β§ βπ β πΎ βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))))) β ran π· β (βͺ ran
π βͺ ran π·)) |
123 | 119 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (βͺ ran π βͺ ran π·) β (π« πΆ β© Fin)) |
124 | | fvssunirn 6876 |
. . . . . . . . . . . . . 14
β’ (πβπ) β βͺ ran
π |
125 | | ssun1 4133 |
. . . . . . . . . . . . . 14
β’ βͺ ran π β (βͺ ran
π βͺ ran π·) |
126 | 124, 125 | sstri 3954 |
. . . . . . . . . . . . 13
β’ (πβπ) β (βͺ ran
π βͺ ran π·) |
127 | | id 22 |
. . . . . . . . . . . . 13
β’ (π§ = (βͺ
ran π βͺ ran π·) β π§ = (βͺ ran π βͺ ran π·)) |
128 | 126, 127 | sseqtrrid 3998 |
. . . . . . . . . . . 12
β’ (π§ = (βͺ
ran π βͺ ran π·) β (πβπ) β π§) |
129 | | pm5.5 362 |
. . . . . . . . . . . 12
β’ ((πβπ) β π§ β (((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))) β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π)))) |
130 | 128, 129 | syl 17 |
. . . . . . . . . . 11
β’ (π§ = (βͺ
ran π βͺ ran π·) β (((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))) β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π)))) |
131 | | reseq2 5933 |
. . . . . . . . . . . . 13
β’ (π§ = (βͺ
ran π βͺ ran π·) β ((π β πΆ β¦ (ππΉπ)) βΎ π§) = ((π β πΆ β¦ (ππΉπ)) βΎ (βͺ ran
π βͺ ran π·))) |
132 | 131 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π§ = (βͺ
ran π βͺ ran π·) β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) = (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ (βͺ ran
π βͺ ran π·)))) |
133 | 132 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π§ = (βͺ
ran π βͺ ran π·) β ((πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π)) β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ (βͺ ran
π βͺ ran π·))) β ran (π β πΏ β¦ ((π»βπ) β π)))) |
134 | 130, 133 | bitrd 279 |
. . . . . . . . . 10
β’ (π§ = (βͺ
ran π βͺ ran π·) β (((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))) β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ (βͺ ran
π βͺ ran π·))) β ran (π β πΏ β¦ ((π»βπ) β π)))) |
135 | 134 | rspcv 3576 |
. . . . . . . . 9
β’ ((βͺ ran π βͺ ran π·) β (π« πΆ β© Fin) β (βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))) β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ (βͺ ran
π βͺ ran π·))) β ran (π β πΏ β¦ ((π»βπ) β π)))) |
136 | 123, 135 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))) β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ (βͺ ran
π βͺ ran π·))) β ran (π β πΏ β¦ ((π»βπ) β π)))) |
137 | 10 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β πΊ β CMnd) |
138 | | cmnmnd 19584 |
. . . . . . . . . . . . 13
β’ (πΊ β CMnd β πΊ β Mnd) |
139 | 137, 138 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β πΊ β Mnd) |
140 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β π β πΎ) |
141 | 117 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (βͺ ran π βͺ ran π·) β Fin) |
142 | 100 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (βͺ ran π βͺ ran π·) β πΆ) |
143 | 142 | sselda 3945 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β§ π β (βͺ ran
π βͺ ran π·)) β π β πΆ) |
144 | 18 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β πΎ) β πΉ:(π΄ Γ πΆ)βΆπ΅) |
145 | 144, 6 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β πΎ) β (πΉ:(π΄ Γ πΆ)βΆπ΅ β§ π β π΄)) |
146 | 19 | 3expa 1119 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ:(π΄ Γ πΆ)βΆπ΅ β§ π β π΄) β§ π β πΆ) β (ππΉπ) β π΅) |
147 | 145, 146 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β πΎ) β§ π β πΆ) β (ππΉπ) β π΅) |
148 | 147 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β§ π β πΆ) β (ππΉπ) β π΅) |
149 | 143, 148 | syldan 592 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β§ π β (βͺ ran
π βͺ ran π·)) β (ππΉπ) β π΅) |
150 | 149 | fmpttd 7064 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (π β (βͺ ran
π βͺ ran π·) β¦ (ππΉπ)):(βͺ ran π βͺ ran π·)βΆπ΅) |
151 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π β (βͺ ran π βͺ ran π·) β¦ (ππΉπ)) = (π β (βͺ ran
π βͺ ran π·) β¦ (ππΉπ)) |
152 | | ovexd 7393 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β§ π β (βͺ ran
π βͺ ran π·)) β (ππΉπ) β V) |
153 | 67 | fvexi 6857 |
. . . . . . . . . . . . . . 15
β’ 0 β
V |
154 | 153 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β 0 β V) |
155 | 151, 141,
152, 154 | fsuppmptdm 9321 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (π β (βͺ ran
π βͺ ran π·) β¦ (ππΉπ)) finSupp 0 ) |
156 | 7, 67, 137, 141, 150, 155 | gsumcl 19697 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (πΊ Ξ£g (π β (βͺ ran π βͺ ran π·) β¦ (ππΉπ))) β π΅) |
157 | | velsn 4603 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β {π} β π¦ = π) |
158 | | ovres 7521 |
. . . . . . . . . . . . . . . . 17
β’ ((π¦ β {π} β§ π β (βͺ ran
π βͺ ran π·)) β (π¦(πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))π) = (π¦πΉπ)) |
159 | 157, 158 | sylanbr 583 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ = π β§ π β (βͺ ran
π βͺ ran π·)) β (π¦(πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))π) = (π¦πΉπ)) |
160 | | oveq1 7365 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π β (π¦πΉπ) = (ππΉπ)) |
161 | 160 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ = π β§ π β (βͺ ran
π βͺ ran π·)) β (π¦πΉπ) = (ππΉπ)) |
162 | 159, 161 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((π¦ = π β§ π β (βͺ ran
π βͺ ran π·)) β (π¦(πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))π) = (ππΉπ)) |
163 | 162 | mpteq2dva 5206 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β (π β (βͺ ran
π βͺ ran π·) β¦ (π¦(πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))π)) = (π β (βͺ ran
π βͺ ran π·) β¦ (ππΉπ))) |
164 | 163 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π¦ = π β (πΊ Ξ£g (π β (βͺ ran π βͺ ran π·) β¦ (π¦(πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))π))) = (πΊ Ξ£g (π β (βͺ ran π βͺ ran π·) β¦ (ππΉπ)))) |
165 | 7, 164 | gsumsn 19736 |
. . . . . . . . . . . 12
β’ ((πΊ β Mnd β§ π β πΎ β§ (πΊ Ξ£g (π β (βͺ ran π βͺ ran π·) β¦ (ππΉπ))) β π΅) β (πΊ Ξ£g (π¦ β {π} β¦ (πΊ Ξ£g (π β (βͺ ran π βͺ ran π·) β¦ (π¦(πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))π))))) = (πΊ Ξ£g (π β (βͺ ran π βͺ ran π·) β¦ (ππΉπ)))) |
166 | 139, 140,
156, 165 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (πΊ Ξ£g (π¦ β {π} β¦ (πΊ Ξ£g (π β (βͺ ran π βͺ ran π·) β¦ (π¦(πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))π))))) = (πΊ Ξ£g (π β (βͺ ran π βͺ ran π·) β¦ (ππΉπ)))) |
167 | | snfi 8991 |
. . . . . . . . . . . . 13
β’ {π} β Fin |
168 | 167 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β {π} β Fin) |
169 | 18 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β πΉ:(π΄ Γ πΆ)βΆπ΅) |
170 | 6 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β π β π΄) |
171 | 170 | snssd 4770 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β {π} β π΄) |
172 | | xpss12 5649 |
. . . . . . . . . . . . . 14
β’ (({π} β π΄ β§ (βͺ ran
π βͺ ran π·) β πΆ) β ({π} Γ (βͺ ran
π βͺ ran π·)) β (π΄ Γ πΆ)) |
173 | 171, 142,
172 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β ({π} Γ (βͺ ran
π βͺ ran π·)) β (π΄ Γ πΆ)) |
174 | 169, 173 | fssresd 6710 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))):({π} Γ (βͺ ran
π βͺ ran π·))βΆπ΅) |
175 | | xpfi 9264 |
. . . . . . . . . . . . . 14
β’ (({π} β Fin β§ (βͺ ran π βͺ ran π·) β Fin) β ({π} Γ (βͺ ran
π βͺ ran π·)) β Fin) |
176 | 167, 141,
175 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β ({π} Γ (βͺ ran
π βͺ ran π·)) β Fin) |
177 | 174, 176,
154 | fdmfifsupp 9320 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))) finSupp 0 ) |
178 | 7, 67, 137, 168, 141, 174, 177 | gsumxp 19758 |
. . . . . . . . . . 11
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))) = (πΊ Ξ£g (π¦ β {π} β¦ (πΊ Ξ£g (π β (βͺ ran π βͺ ran π·) β¦ (π¦(πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))π)))))) |
179 | 142 | resmptd 5995 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β ((π β πΆ β¦ (ππΉπ)) βΎ (βͺ ran
π βͺ ran π·)) = (π β (βͺ ran
π βͺ ran π·) β¦ (ππΉπ))) |
180 | 179 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ (βͺ ran
π βͺ ran π·))) = (πΊ Ξ£g (π β (βͺ ran π βͺ ran π·) β¦ (ππΉπ)))) |
181 | 166, 178,
180 | 3eqtr4rd 2784 |
. . . . . . . . . 10
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ (βͺ ran
π βͺ ran π·))) = (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) |
182 | 181 | eleq1d 2819 |
. . . . . . . . 9
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β ((πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ (βͺ ran
π βͺ ran π·))) β ran (π β πΏ β¦ ((π»βπ) β π)) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))) β ran (π β πΏ β¦ ((π»βπ) β π)))) |
183 | | ovex 7391 |
. . . . . . . . . . 11
β’ ((π»βπ) β π) β V |
184 | 73, 183 | elrnmpti 5916 |
. . . . . . . . . 10
β’ ((πΊ Ξ£g
(πΉ βΎ ({π} Γ (βͺ ran π βͺ ran π·)))) β ran (π β πΏ β¦ ((π»βπ) β π)) β βπ β πΏ (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))) = ((π»βπ) β π)) |
185 | | isabl 19571 |
. . . . . . . . . . . . . . . 16
β’ (πΊ β Abel β (πΊ β Grp β§ πΊ β CMnd)) |
186 | 43, 10, 185 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ (π β πΊ β Abel) |
187 | 186 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β§ π β πΏ) β πΊ β Abel) |
188 | 6, 35 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β πΎ) β (π»βπ) β π΅) |
189 | 188 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β§ π β πΏ) β (π»βπ) β π΅) |
190 | 29 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β πΏ β π΅) |
191 | 190 | sselda 3945 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β§ π β πΏ) β π β π΅) |
192 | 7, 38, 187, 189, 191 | ablnncan 19604 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β§ π β πΏ) β ((π»βπ) β ((π»βπ) β π)) = π) |
193 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β§ π β πΏ) β π β πΏ) |
194 | 192, 193 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ ((((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β§ π β πΏ) β ((π»βπ) β ((π»βπ) β π)) β πΏ) |
195 | | oveq2 7366 |
. . . . . . . . . . . . 13
β’ ((πΊ Ξ£g
(πΉ βΎ ({π} Γ (βͺ ran π βͺ ran π·)))) = ((π»βπ) β π) β ((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) = ((π»βπ) β ((π»βπ) β π))) |
196 | 195 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ ((πΊ Ξ£g
(πΉ βΎ ({π} Γ (βͺ ran π βͺ ran π·)))) = ((π»βπ) β π) β (((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) β πΏ β ((π»βπ) β ((π»βπ) β π)) β πΏ)) |
197 | 194, 196 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ ((((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β§ π β πΏ) β ((πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))) = ((π»βπ) β π) β ((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) β πΏ)) |
198 | 197 | rexlimdva 3149 |
. . . . . . . . . 10
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (βπ β πΏ (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))) = ((π»βπ) β π) β ((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) β πΏ)) |
199 | 184, 198 | biimtrid 241 |
. . . . . . . . 9
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β ((πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))) β ran (π β πΏ β¦ ((π»βπ) β π)) β ((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) β πΏ)) |
200 | 182, 199 | sylbid 239 |
. . . . . . . 8
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β ((πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ (βͺ ran
π βͺ ran π·))) β ran (π β πΏ β¦ ((π»βπ) β π)) β ((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) β πΏ)) |
201 | 136, 200 | syld 47 |
. . . . . . 7
β’ (((π β§ π β πΎ) β§ π:πΎβΆ(π« πΆ β© Fin)) β (βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))) β ((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) β πΏ)) |
202 | 201 | an32s 651 |
. . . . . 6
β’ (((π β§ π:πΎβΆ(π« πΆ β© Fin)) β§ π β πΎ) β (βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))) β ((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) β πΏ)) |
203 | 202 | ralimdva 3161 |
. . . . 5
β’ ((π β§ π:πΎβΆ(π« πΆ β© Fin)) β (βπ β πΎ βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))) β βπ β πΎ ((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) β πΏ)) |
204 | 203 | impr 456 |
. . . 4
β’ ((π β§ (π:πΎβΆ(π« πΆ β© Fin) β§ βπ β πΎ βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))))) β βπ β πΎ ((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) β πΏ) |
205 | | fveq2 6843 |
. . . . . . 7
β’ (π = π₯ β (π»βπ) = (π»βπ₯)) |
206 | | sneq 4597 |
. . . . . . . . . 10
β’ (π = π₯ β {π} = {π₯}) |
207 | 206 | xpeq1d 5663 |
. . . . . . . . 9
β’ (π = π₯ β ({π} Γ (βͺ ran
π βͺ ran π·)) = ({π₯} Γ (βͺ ran
π βͺ ran π·))) |
208 | 207 | reseq2d 5938 |
. . . . . . . 8
β’ (π = π₯ β (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))) = (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·)))) |
209 | 208 | oveq2d 7374 |
. . . . . . 7
β’ (π = π₯ β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·)))) = (πΊ Ξ£g (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·))))) |
210 | 205, 209 | oveq12d 7376 |
. . . . . 6
β’ (π = π₯ β ((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) = ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·)))))) |
211 | 210 | eleq1d 2819 |
. . . . 5
β’ (π = π₯ β (((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) β πΏ β ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·))))) β πΏ)) |
212 | 211 | cbvralvw 3224 |
. . . 4
β’
(βπ β
πΎ ((π»βπ) β (πΊ Ξ£g (πΉ βΎ ({π} Γ (βͺ ran
π βͺ ran π·))))) β πΏ β βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·))))) β πΏ) |
213 | 204, 212 | sylib 217 |
. . 3
β’ ((π β§ (π:πΎβΆ(π« πΆ β© Fin) β§ βπ β πΎ βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))))) β βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·))))) β πΏ) |
214 | | sseq2 3971 |
. . . . 5
β’ (π = (βͺ
ran π βͺ ran π·) β (ran π· β π β ran π· β (βͺ ran
π βͺ ran π·))) |
215 | | xpeq2 5655 |
. . . . . . . . . 10
β’ (π = (βͺ
ran π βͺ ran π·) β ({π₯} Γ π) = ({π₯} Γ (βͺ ran
π βͺ ran π·))) |
216 | 215 | reseq2d 5938 |
. . . . . . . . 9
β’ (π = (βͺ
ran π βͺ ran π·) β (πΉ βΎ ({π₯} Γ π)) = (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·)))) |
217 | 216 | oveq2d 7374 |
. . . . . . . 8
β’ (π = (βͺ
ran π βͺ ran π·) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π))) = (πΊ Ξ£g (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·))))) |
218 | 217 | oveq2d 7374 |
. . . . . . 7
β’ (π = (βͺ
ran π βͺ ran π·) β ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) = ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·)))))) |
219 | 218 | eleq1d 2819 |
. . . . . 6
β’ (π = (βͺ
ran π βͺ ran π·) β (((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) β πΏ β ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·))))) β πΏ)) |
220 | 219 | ralbidv 3171 |
. . . . 5
β’ (π = (βͺ
ran π βͺ ran π·) β (βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) β πΏ β βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·))))) β πΏ)) |
221 | 214, 220 | anbi12d 632 |
. . . 4
β’ (π = (βͺ
ran π βͺ ran π·) β ((ran π· β π β§ βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) β πΏ) β (ran π· β (βͺ ran
π βͺ ran π·) β§ βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·))))) β πΏ))) |
222 | 221 | rspcev 3580 |
. . 3
β’ (((βͺ ran π βͺ ran π·) β (π« πΆ β© Fin) β§ (ran π· β (βͺ ran
π βͺ ran π·) β§ βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ (βͺ ran
π βͺ ran π·))))) β πΏ)) β βπ β (π« πΆ β© Fin)(ran π· β π β§ βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) β πΏ)) |
223 | 120, 122,
213, 222 | syl12anc 836 |
. 2
β’ ((π β§ (π:πΎβΆ(π« πΆ β© Fin) β§ βπ β πΎ βπ§ β (π« πΆ β© Fin)((πβπ) β π§ β (πΊ Ξ£g ((π β πΆ β¦ (ππΉπ)) βΎ π§)) β ran (π β πΏ β¦ ((π»βπ) β π))))) β βπ β (π« πΆ β© Fin)(ran π· β π β§ βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) β πΏ)) |
224 | 85, 223 | exlimddv 1939 |
1
β’ (π β βπ β (π« πΆ β© Fin)(ran π· β π β§ βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) β πΏ)) |