Step | Hyp | Ref
| Expression |
1 | | inss1 4189 |
. . . . . . . . . . . 12
β’ (π΄ β© π) β π΄ |
2 | 1 | sspwi 4573 |
. . . . . . . . . . 11
β’ π«
(π΄ β© π) β π« π΄ |
3 | | ssrin 4194 |
. . . . . . . . . . 11
β’
(π« (π΄ β©
π) β π« π΄ β (π« (π΄ β© π) β© Fin) β (π« π΄ β© Fin)) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . . 10
β’
(π« (π΄ β©
π) β© Fin) β
(π« π΄ β©
Fin) |
5 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β (π« (π΄ β© π) β© Fin)) β π β (π« (π΄ β© π) β© Fin)) |
6 | 4, 5 | sselid 3943 |
. . . . . . . . 9
β’ ((π β§ π β (π« (π΄ β© π) β© Fin)) β π β (π« π΄ β© Fin)) |
7 | | elfpw 9301 |
. . . . . . . . . . . . . . . 16
β’ (π§ β (π« π΄ β© Fin) β (π§ β π΄ β§ π§ β Fin)) |
8 | 7 | simplbi 499 |
. . . . . . . . . . . . . . 15
β’ (π§ β (π« π΄ β© Fin) β π§ β π΄) |
9 | 8 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β π§ β π΄) |
10 | 9 | ssrind 4196 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β (π§ β© π) β (π΄ β© π)) |
11 | | elinel2 4157 |
. . . . . . . . . . . . . . 15
β’ (π§ β (π« π΄ β© Fin) β π§ β Fin) |
12 | 11 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β π§ β Fin) |
13 | | inss1 4189 |
. . . . . . . . . . . . . 14
β’ (π§ β© π) β π§ |
14 | | ssfi 9120 |
. . . . . . . . . . . . . 14
β’ ((π§ β Fin β§ (π§ β© π) β π§) β (π§ β© π) β Fin) |
15 | 12, 13, 14 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β (π§ β© π) β Fin) |
16 | | elfpw 9301 |
. . . . . . . . . . . . 13
β’ ((π§ β© π) β (π« (π΄ β© π) β© Fin) β ((π§ β© π) β (π΄ β© π) β§ (π§ β© π) β Fin)) |
17 | 10, 15, 16 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β (π§ β© π) β (π« (π΄ β© π) β© Fin)) |
18 | | sseq2 3971 |
. . . . . . . . . . . . . . 15
β’ (π = (π§ β© π) β (π β π β π β (π§ β© π))) |
19 | | ssin 4191 |
. . . . . . . . . . . . . . 15
β’ ((π β π§ β§ π β π) β π β (π§ β© π)) |
20 | 18, 19 | bitr4di 289 |
. . . . . . . . . . . . . 14
β’ (π = (π§ β© π) β (π β π β (π β π§ β§ π β π))) |
21 | | reseq2 5933 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π§ β© π) β ((πΉ βΎ π) βΎ π) = ((πΉ βΎ π) βΎ (π§ β© π))) |
22 | | inss2 4190 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β© π) β π |
23 | | resabs1 5968 |
. . . . . . . . . . . . . . . . . 18
β’ ((π§ β© π) β π β ((πΉ βΎ π) βΎ (π§ β© π)) = (πΉ βΎ (π§ β© π))) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ βΎ π) βΎ (π§ β© π)) = (πΉ βΎ (π§ β© π)) |
25 | 21, 24 | eqtrdi 2789 |
. . . . . . . . . . . . . . . 16
β’ (π = (π§ β© π) β ((πΉ βΎ π) βΎ π) = (πΉ βΎ (π§ β© π))) |
26 | 25 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (π = (π§ β© π) β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) = (πΊ Ξ£g (πΉ βΎ (π§ β© π)))) |
27 | 26 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π = (π§ β© π) β ((πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’ β (πΊ Ξ£g (πΉ βΎ (π§ β© π))) β π’)) |
28 | 20, 27 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = (π§ β© π) β ((π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’) β ((π β π§ β§ π β π) β (πΊ Ξ£g (πΉ βΎ (π§ β© π))) β π’))) |
29 | 28 | rspcv 3576 |
. . . . . . . . . . . 12
β’ ((π§ β© π) β (π« (π΄ β© π) β© Fin) β (βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’) β ((π β π§ β§ π β π) β (πΊ Ξ£g (πΉ βΎ (π§ β© π))) β π’))) |
30 | 17, 29 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β (βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’) β ((π β π§ β§ π β π) β (πΊ Ξ£g (πΉ βΎ (π§ β© π))) β π’))) |
31 | | elfpw 9301 |
. . . . . . . . . . . . . . . 16
β’ (π β (π« (π΄ β© π) β© Fin) β (π β (π΄ β© π) β§ π β Fin)) |
32 | 31 | simplbi 499 |
. . . . . . . . . . . . . . 15
β’ (π β (π« (π΄ β© π) β© Fin) β π β (π΄ β© π)) |
33 | 32 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β π β (π΄ β© π)) |
34 | | inss2 4190 |
. . . . . . . . . . . . . 14
β’ (π΄ β© π) β π |
35 | 33, 34 | sstrdi 3957 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β π β π) |
36 | 35 | biantrud 533 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β (π β π§ β (π β π§ β§ π β π))) |
37 | | tsmsres.b |
. . . . . . . . . . . . . . 15
β’ π΅ = (BaseβπΊ) |
38 | | tsmsres.z |
. . . . . . . . . . . . . . 15
β’ 0 =
(0gβπΊ) |
39 | | tsmsres.1 |
. . . . . . . . . . . . . . . 16
β’ (π β πΊ β CMnd) |
40 | 39 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β πΊ β CMnd) |
41 | | tsmsres.f |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ:π΄βΆπ΅) |
42 | 41 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β πΉ:π΄βΆπ΅) |
43 | 42, 9 | fssresd 6710 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β (πΉ βΎ π§):π§βΆπ΅) |
44 | | tsmsres.a |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΄ β π) |
45 | 41, 44 | fexd 7178 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΉ β V) |
46 | 45 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β πΉ β V) |
47 | 38 | fvexi 6857 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
V |
48 | | ressuppss 8115 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ β V β§ 0 β V)
β ((πΉ βΎ π§) supp 0 ) β (πΉ supp 0 )) |
49 | 46, 47, 48 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β ((πΉ βΎ π§) supp 0 ) β (πΉ supp 0 )) |
50 | | tsmsres.s |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΉ supp 0 ) β π) |
51 | 50 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β (πΉ supp 0 ) β π) |
52 | 49, 51 | sstrd 3955 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β ((πΉ βΎ π§) supp 0 ) β π) |
53 | 47 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β 0 β V) |
54 | 43, 12, 53 | fdmfifsupp 9320 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β (πΉ βΎ π§) finSupp 0 ) |
55 | 37, 38, 40, 12, 43, 52, 54 | gsumres 19695 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β (πΊ Ξ£g ((πΉ βΎ π§) βΎ π)) = (πΊ Ξ£g (πΉ βΎ π§))) |
56 | | resres 5951 |
. . . . . . . . . . . . . . 15
β’ ((πΉ βΎ π§) βΎ π) = (πΉ βΎ (π§ β© π)) |
57 | 56 | oveq2i 7369 |
. . . . . . . . . . . . . 14
β’ (πΊ Ξ£g
((πΉ βΎ π§) βΎ π)) = (πΊ Ξ£g (πΉ βΎ (π§ β© π))) |
58 | 55, 57 | eqtr3di 2788 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ π§)) = (πΊ Ξ£g (πΉ βΎ (π§ β© π)))) |
59 | 58 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β ((πΊ Ξ£g (πΉ βΎ π§)) β π’ β (πΊ Ξ£g (πΉ βΎ (π§ β© π))) β π’)) |
60 | 36, 59 | imbi12d 345 |
. . . . . . . . . . 11
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β ((π β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β ((π β π§ β§ π β π) β (πΊ Ξ£g (πΉ βΎ (π§ β© π))) β π’))) |
61 | 30, 60 | sylibrd 259 |
. . . . . . . . . 10
β’ (((π β§ π β (π« (π΄ β© π) β© Fin)) β§ π§ β (π« π΄ β© Fin)) β (βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’) β (π β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
62 | 61 | ralrimdva 3148 |
. . . . . . . . 9
β’ ((π β§ π β (π« (π΄ β© π) β© Fin)) β (βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’) β βπ§ β (π« π΄ β© Fin)(π β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
63 | | sseq1 3970 |
. . . . . . . . . 10
β’ (π¦ = π β (π¦ β π§ β π β π§)) |
64 | 63 | rspceaimv 3584 |
. . . . . . . . 9
β’ ((π β (π« π΄ β© Fin) β§ βπ§ β (π« π΄ β© Fin)(π β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
65 | 6, 62, 64 | syl6an 683 |
. . . . . . . 8
β’ ((π β§ π β (π« (π΄ β© π) β© Fin)) β (βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’) β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
66 | 65 | rexlimdva 3149 |
. . . . . . 7
β’ (π β (βπ β (π« (π΄ β© π) β© Fin)βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’) β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
67 | | elfpw 9301 |
. . . . . . . . . . . . 13
β’ (π¦ β (π« π΄ β© Fin) β (π¦ β π΄ β§ π¦ β Fin)) |
68 | 67 | simplbi 499 |
. . . . . . . . . . . 12
β’ (π¦ β (π« π΄ β© Fin) β π¦ β π΄) |
69 | 68 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π« π΄ β© Fin)) β π¦ β π΄) |
70 | 69 | ssrind 4196 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π« π΄ β© Fin)) β (π¦ β© π) β (π΄ β© π)) |
71 | | elinel2 4157 |
. . . . . . . . . . . 12
β’ (π¦ β (π« π΄ β© Fin) β π¦ β Fin) |
72 | 71 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π« π΄ β© Fin)) β π¦ β Fin) |
73 | | inss1 4189 |
. . . . . . . . . . 11
β’ (π¦ β© π) β π¦ |
74 | | ssfi 9120 |
. . . . . . . . . . 11
β’ ((π¦ β Fin β§ (π¦ β© π) β π¦) β (π¦ β© π) β Fin) |
75 | 72, 73, 74 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π« π΄ β© Fin)) β (π¦ β© π) β Fin) |
76 | | elfpw 9301 |
. . . . . . . . . 10
β’ ((π¦ β© π) β (π« (π΄ β© π) β© Fin) β ((π¦ β© π) β (π΄ β© π) β§ (π¦ β© π) β Fin)) |
77 | 70, 75, 76 | sylanbrc 584 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π« π΄ β© Fin)) β (π¦ β© π) β (π« (π΄ β© π) β© Fin)) |
78 | 68 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ π β (π« (π΄ β© π) β© Fin)) β π¦ β π΄) |
79 | | elfpw 9301 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π« (π΄ β© π) β© Fin) β (π β (π΄ β© π) β§ π β Fin)) |
80 | 79 | simplbi 499 |
. . . . . . . . . . . . . . . 16
β’ (π β (π« (π΄ β© π) β© Fin) β π β (π΄ β© π)) |
81 | 80 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ π β (π« (π΄ β© π) β© Fin)) β π β (π΄ β© π)) |
82 | 81, 1 | sstrdi 3957 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ π β (π« (π΄ β© π) β© Fin)) β π β π΄) |
83 | 78, 82 | unssd 4147 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ π β (π« (π΄ β© π) β© Fin)) β (π¦ βͺ π) β π΄) |
84 | | elinel2 4157 |
. . . . . . . . . . . . . 14
β’ (π β (π« (π΄ β© π) β© Fin) β π β Fin) |
85 | | unfi 9119 |
. . . . . . . . . . . . . 14
β’ ((π¦ β Fin β§ π β Fin) β (π¦ βͺ π) β Fin) |
86 | 72, 84, 85 | syl2an 597 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ π β (π« (π΄ β© π) β© Fin)) β (π¦ βͺ π) β Fin) |
87 | | elfpw 9301 |
. . . . . . . . . . . . 13
β’ ((π¦ βͺ π) β (π« π΄ β© Fin) β ((π¦ βͺ π) β π΄ β§ (π¦ βͺ π) β Fin)) |
88 | 83, 86, 87 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ π β (π« (π΄ β© π) β© Fin)) β (π¦ βͺ π) β (π« π΄ β© Fin)) |
89 | | ssun1 4133 |
. . . . . . . . . . . . . . . 16
β’ π¦ β (π¦ βͺ π) |
90 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π¦ βͺ π) β π§ = (π¦ βͺ π)) |
91 | 89, 90 | sseqtrrid 3998 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π¦ βͺ π) β π¦ β π§) |
92 | | pm5.5 362 |
. . . . . . . . . . . . . . 15
β’ (π¦ β π§ β ((π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π§ = (π¦ βͺ π) β ((π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ π§)) β π’)) |
94 | | reseq2 5933 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π¦ βͺ π) β (πΉ βΎ π§) = (πΉ βΎ (π¦ βͺ π))) |
95 | 94 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π¦ βͺ π) β (πΊ Ξ£g (πΉ βΎ π§)) = (πΊ Ξ£g (πΉ βΎ (π¦ βͺ π)))) |
96 | 95 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π§ = (π¦ βͺ π) β ((πΊ Ξ£g (πΉ βΎ π§)) β π’ β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ π))) β π’)) |
97 | 93, 96 | bitrd 279 |
. . . . . . . . . . . . 13
β’ (π§ = (π¦ βͺ π) β ((π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ π))) β π’)) |
98 | 97 | rspcv 3576 |
. . . . . . . . . . . 12
β’ ((π¦ βͺ π) β (π« π΄ β© Fin) β (βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ π))) β π’)) |
99 | 88, 98 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ π β (π« (π΄ β© π) β© Fin)) β (βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ π))) β π’)) |
100 | 39 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β πΊ β CMnd) |
101 | 86 | adantrr 716 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β (π¦ βͺ π) β Fin) |
102 | 41 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β πΉ:π΄βΆπ΅) |
103 | 83 | adantrr 716 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β (π¦ βͺ π) β π΄) |
104 | 102, 103 | fssresd 6710 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β (πΉ βΎ (π¦ βͺ π)):(π¦ βͺ π)βΆπ΅) |
105 | 45, 47 | jctir 522 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΉ β V β§ 0 β
V)) |
106 | 105 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β (πΉ β V β§ 0 β
V)) |
107 | | ressuppss 8115 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ β V β§ 0 β V)
β ((πΉ βΎ (π¦ βͺ π)) supp 0 ) β (πΉ supp 0 )) |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β ((πΉ βΎ (π¦ βͺ π)) supp 0 ) β (πΉ supp 0 )) |
109 | 50 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β (πΉ supp 0 ) β π) |
110 | 108, 109 | sstrd 3955 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β ((πΉ βΎ (π¦ βͺ π)) supp 0 ) β π) |
111 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β 0 β V) |
112 | 104, 101,
111 | fdmfifsupp 9320 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β (πΉ βΎ (π¦ βͺ π)) finSupp 0 ) |
113 | 37, 38, 100, 101, 104, 110, 112 | gsumres 19695 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β (πΊ Ξ£g ((πΉ βΎ (π¦ βͺ π)) βΎ π)) = (πΊ Ξ£g (πΉ βΎ (π¦ βͺ π)))) |
114 | | resres 5951 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ βΎ (π¦ βͺ π)) βΎ π) = (πΉ βΎ ((π¦ βͺ π) β© π)) |
115 | | indir 4236 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ βͺ π) β© π) = ((π¦ β© π) βͺ (π β© π)) |
116 | 81, 34 | sstrdi 3957 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ π β (π« (π΄ β© π) β© Fin)) β π β π) |
117 | 116 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β π β π) |
118 | | df-ss 3928 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β (π β© π) = π) |
119 | 117, 118 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β (π β© π) = π) |
120 | 119 | uneq2d 4124 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β ((π¦ β© π) βͺ (π β© π)) = ((π¦ β© π) βͺ π)) |
121 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β (π¦ β© π) β π) |
122 | | ssequn1 4141 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ β© π) β π β ((π¦ β© π) βͺ π) = π) |
123 | 121, 122 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β ((π¦ β© π) βͺ π) = π) |
124 | 120, 123 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β ((π¦ β© π) βͺ (π β© π)) = π) |
125 | 115, 124 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β ((π¦ βͺ π) β© π) = π) |
126 | 125 | reseq2d 5938 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β (πΉ βΎ ((π¦ βͺ π) β© π)) = (πΉ βΎ π)) |
127 | 114, 126 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β ((πΉ βΎ (π¦ βͺ π)) βΎ π) = (πΉ βΎ π)) |
128 | 117 | resabs1d 5969 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β ((πΉ βΎ π) βΎ π) = (πΉ βΎ π)) |
129 | 127, 128 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β ((πΉ βΎ (π¦ βͺ π)) βΎ π) = ((πΉ βΎ π) βΎ π)) |
130 | 129 | oveq2d 7374 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β (πΊ Ξ£g ((πΉ βΎ (π¦ βͺ π)) βΎ π)) = (πΊ Ξ£g ((πΉ βΎ π) βΎ π))) |
131 | 113, 130 | eqtr3d 2775 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β (πΊ Ξ£g (πΉ βΎ (π¦ βͺ π))) = (πΊ Ξ£g ((πΉ βΎ π) βΎ π))) |
132 | 131 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β ((πΊ Ξ£g (πΉ βΎ (π¦ βͺ π))) β π’ β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’)) |
133 | 132 | biimpd 228 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ (π β (π« (π΄ β© π) β© Fin) β§ (π¦ β© π) β π)) β ((πΊ Ξ£g (πΉ βΎ (π¦ βͺ π))) β π’ β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’)) |
134 | 133 | expr 458 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ π β (π« (π΄ β© π) β© Fin)) β ((π¦ β© π) β π β ((πΊ Ξ£g (πΉ βΎ (π¦ βͺ π))) β π’ β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’))) |
135 | 134 | com23 86 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ π β (π« (π΄ β© π) β© Fin)) β ((πΊ Ξ£g (πΉ βΎ (π¦ βͺ π))) β π’ β ((π¦ β© π) β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’))) |
136 | 99, 135 | syld 47 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π« π΄ β© Fin)) β§ π β (π« (π΄ β© π) β© Fin)) β (βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β ((π¦ β© π) β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’))) |
137 | 136 | ralrimdva 3148 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π« π΄ β© Fin)) β (βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ β (π« (π΄ β© π) β© Fin)((π¦ β© π) β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’))) |
138 | | sseq1 3970 |
. . . . . . . . . 10
β’ (π = (π¦ β© π) β (π β π β (π¦ β© π) β π)) |
139 | 138 | rspceaimv 3584 |
. . . . . . . . 9
β’ (((π¦ β© π) β (π« (π΄ β© π) β© Fin) β§ βπ β (π« (π΄ β© π) β© Fin)((π¦ β© π) β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’)) β βπ β (π« (π΄ β© π) β© Fin)βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’)) |
140 | 77, 137, 139 | syl6an 683 |
. . . . . . . 8
β’ ((π β§ π¦ β (π« π΄ β© Fin)) β (βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ β (π« (π΄ β© π) β© Fin)βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’))) |
141 | 140 | rexlimdva 3149 |
. . . . . . 7
β’ (π β (βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’) β βπ β (π« (π΄ β© π) β© Fin)βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’))) |
142 | 66, 141 | impbid 211 |
. . . . . 6
β’ (π β (βπ β (π« (π΄ β© π) β© Fin)βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’) β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))) |
143 | 142 | imbi2d 341 |
. . . . 5
β’ (π β ((π₯ β π’ β βπ β (π« (π΄ β© π) β© Fin)βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’)) β (π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)))) |
144 | 143 | ralbidv 3171 |
. . . 4
β’ (π β (βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ β (π« (π΄ β© π) β© Fin)βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’)) β βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’)))) |
145 | 144 | anbi2d 630 |
. . 3
β’ (π β ((π₯ β π΅ β§ βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ β (π« (π΄ β© π) β© Fin)βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’))) β (π₯ β π΅ β§ βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))))) |
146 | | eqid 2733 |
. . . 4
β’
(TopOpenβπΊ) =
(TopOpenβπΊ) |
147 | | eqid 2733 |
. . . 4
β’
(π« (π΄ β©
π) β© Fin) = (π«
(π΄ β© π) β© Fin) |
148 | | tsmsres.2 |
. . . 4
β’ (π β πΊ β TopSp) |
149 | | inex1g 5277 |
. . . . 5
β’ (π΄ β π β (π΄ β© π) β V) |
150 | 44, 149 | syl 17 |
. . . 4
β’ (π β (π΄ β© π) β V) |
151 | | fssres 6709 |
. . . . . 6
β’ ((πΉ:π΄βΆπ΅ β§ (π΄ β© π) β π΄) β (πΉ βΎ (π΄ β© π)):(π΄ β© π)βΆπ΅) |
152 | 41, 1, 151 | sylancl 587 |
. . . . 5
β’ (π β (πΉ βΎ (π΄ β© π)):(π΄ β© π)βΆπ΅) |
153 | | resres 5951 |
. . . . . . 7
β’ ((πΉ βΎ π΄) βΎ π) = (πΉ βΎ (π΄ β© π)) |
154 | | ffn 6669 |
. . . . . . . . 9
β’ (πΉ:π΄βΆπ΅ β πΉ Fn π΄) |
155 | | fnresdm 6621 |
. . . . . . . . 9
β’ (πΉ Fn π΄ β (πΉ βΎ π΄) = πΉ) |
156 | 41, 154, 155 | 3syl 18 |
. . . . . . . 8
β’ (π β (πΉ βΎ π΄) = πΉ) |
157 | 156 | reseq1d 5937 |
. . . . . . 7
β’ (π β ((πΉ βΎ π΄) βΎ π) = (πΉ βΎ π)) |
158 | 153, 157 | eqtr3id 2787 |
. . . . . 6
β’ (π β (πΉ βΎ (π΄ β© π)) = (πΉ βΎ π)) |
159 | 158 | feq1d 6654 |
. . . . 5
β’ (π β ((πΉ βΎ (π΄ β© π)):(π΄ β© π)βΆπ΅ β (πΉ βΎ π):(π΄ β© π)βΆπ΅)) |
160 | 152, 159 | mpbid 231 |
. . . 4
β’ (π β (πΉ βΎ π):(π΄ β© π)βΆπ΅) |
161 | 37, 146, 147, 39, 148, 150, 160 | eltsms 23500 |
. . 3
β’ (π β (π₯ β (πΊ tsums (πΉ βΎ π)) β (π₯ β π΅ β§ βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ β (π« (π΄ β© π) β© Fin)βπ β (π« (π΄ β© π) β© Fin)(π β π β (πΊ Ξ£g ((πΉ βΎ π) βΎ π)) β π’))))) |
162 | | eqid 2733 |
. . . 4
β’
(π« π΄ β©
Fin) = (π« π΄ β©
Fin) |
163 | 37, 146, 162, 39, 148, 44, 41 | eltsms 23500 |
. . 3
β’ (π β (π₯ β (πΊ tsums πΉ) β (π₯ β π΅ β§ βπ’ β (TopOpenβπΊ)(π₯ β π’ β βπ¦ β (π« π΄ β© Fin)βπ§ β (π« π΄ β© Fin)(π¦ β π§ β (πΊ Ξ£g (πΉ βΎ π§)) β π’))))) |
164 | 145, 161,
163 | 3bitr4d 311 |
. 2
β’ (π β (π₯ β (πΊ tsums (πΉ βΎ π)) β π₯ β (πΊ tsums πΉ))) |
165 | 164 | eqrdv 2731 |
1
β’ (π β (πΊ tsums (πΉ βΎ π)) = (πΊ tsums πΉ)) |