Step | Hyp | Ref
| Expression |
1 | | dvcmul.s |
. . 3
β’ (π β π β {β, β}) |
2 | | dvcmul.a |
. . . . 5
β’ (π β π΄ β β) |
3 | | fconstg 6779 |
. . . . 5
β’ (π΄ β β β (π Γ {π΄}):πβΆ{π΄}) |
4 | 2, 3 | syl 17 |
. . . 4
β’ (π β (π Γ {π΄}):πβΆ{π΄}) |
5 | 2 | snssd 4813 |
. . . 4
β’ (π β {π΄} β β) |
6 | 4, 5 | fssd 6736 |
. . 3
β’ (π β (π Γ {π΄}):πβΆβ) |
7 | | dvcmul.f |
. . 3
β’ (π β πΉ:πβΆβ) |
8 | | c0ex 11208 |
. . . . . 6
β’ 0 β
V |
9 | 8 | fconst 6778 |
. . . . 5
β’ (π Γ {0}):πβΆ{0} |
10 | | recnprss 25421 |
. . . . . . . . 9
β’ (π β {β, β}
β π β
β) |
11 | 1, 10 | syl 17 |
. . . . . . . 8
β’ (π β π β β) |
12 | | fconstg 6779 |
. . . . . . . . . 10
β’ (π΄ β β β (π Γ {π΄}):πβΆ{π΄}) |
13 | 2, 12 | syl 17 |
. . . . . . . . 9
β’ (π β (π Γ {π΄}):πβΆ{π΄}) |
14 | 13, 5 | fssd 6736 |
. . . . . . . 8
β’ (π β (π Γ {π΄}):πβΆβ) |
15 | | ssidd 4006 |
. . . . . . . 8
β’ (π β π β π) |
16 | | dvcmulf.df |
. . . . . . . . 9
β’ (π β dom (π D πΉ) = π) |
17 | | dvbsss 25419 |
. . . . . . . . . 10
β’ dom
(π D πΉ) β π |
18 | 17 | a1i 11 |
. . . . . . . . 9
β’ (π β dom (π D πΉ) β π) |
19 | 16, 18 | eqsstrrd 4022 |
. . . . . . . 8
β’ (π β π β π) |
20 | | eqid 2733 |
. . . . . . . . 9
β’
(TopOpenββfld) =
(TopOpenββfld) |
21 | | eqid 2733 |
. . . . . . . . 9
β’
((TopOpenββfld) βΎt π) =
((TopOpenββfld) βΎt π) |
22 | 20, 21 | dvres 25428 |
. . . . . . . 8
β’ (((π β β β§ (π Γ {π΄}):πβΆβ) β§ (π β π β§ π β π)) β (π D ((π Γ {π΄}) βΎ π)) = ((π D (π Γ {π΄})) βΎ
((intβ((TopOpenββfld) βΎt π))βπ))) |
23 | 11, 14, 15, 19, 22 | syl22anc 838 |
. . . . . . 7
β’ (π β (π D ((π Γ {π΄}) βΎ π)) = ((π D (π Γ {π΄})) βΎ
((intβ((TopOpenββfld) βΎt π))βπ))) |
24 | 19 | resmptd 6041 |
. . . . . . . . 9
β’ (π β ((π₯ β π β¦ π΄) βΎ π) = (π₯ β π β¦ π΄)) |
25 | | fconstmpt 5739 |
. . . . . . . . . 10
β’ (π Γ {π΄}) = (π₯ β π β¦ π΄) |
26 | 25 | reseq1i 5978 |
. . . . . . . . 9
β’ ((π Γ {π΄}) βΎ π) = ((π₯ β π β¦ π΄) βΎ π) |
27 | | fconstmpt 5739 |
. . . . . . . . 9
β’ (π Γ {π΄}) = (π₯ β π β¦ π΄) |
28 | 24, 26, 27 | 3eqtr4g 2798 |
. . . . . . . 8
β’ (π β ((π Γ {π΄}) βΎ π) = (π Γ {π΄})) |
29 | 28 | oveq2d 7425 |
. . . . . . 7
β’ (π β (π D ((π Γ {π΄}) βΎ π)) = (π D (π Γ {π΄}))) |
30 | 19 | resmptd 6041 |
. . . . . . . 8
β’ (π β ((π₯ β π β¦ 0) βΎ π) = (π₯ β π β¦ 0)) |
31 | | fconstg 6779 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β (β
Γ {π΄}):ββΆ{π΄}) |
32 | 2, 31 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (β Γ {π΄}):ββΆ{π΄}) |
33 | 32, 5 | fssd 6736 |
. . . . . . . . . . . 12
β’ (π β (β Γ {π΄}):ββΆβ) |
34 | | ssidd 4006 |
. . . . . . . . . . . 12
β’ (π β β β
β) |
35 | | dvconst 25434 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β (β
D (β Γ {π΄})) =
(β Γ {0})) |
36 | 2, 35 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (β D (β
Γ {π΄})) = (β
Γ {0})) |
37 | 36 | dmeqd 5906 |
. . . . . . . . . . . . . 14
β’ (π β dom (β D (β
Γ {π΄})) = dom
(β Γ {0})) |
38 | 8 | fconst 6778 |
. . . . . . . . . . . . . . 15
β’ (β
Γ {0}):ββΆ{0} |
39 | 38 | fdmi 6730 |
. . . . . . . . . . . . . 14
β’ dom
(β Γ {0}) = β |
40 | 37, 39 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ (π β dom (β D (β
Γ {π΄})) =
β) |
41 | 11, 40 | sseqtrrd 4024 |
. . . . . . . . . . . 12
β’ (π β π β dom (β D (β Γ
{π΄}))) |
42 | | dvres3 25430 |
. . . . . . . . . . . 12
β’ (((π β {β, β} β§
(β Γ {π΄}):ββΆβ) β§ (β
β β β§ π
β dom (β D (β Γ {π΄})))) β (π D ((β Γ {π΄}) βΎ π)) = ((β D (β Γ {π΄})) βΎ π)) |
43 | 1, 33, 34, 41, 42 | syl22anc 838 |
. . . . . . . . . . 11
β’ (π β (π D ((β Γ {π΄}) βΎ π)) = ((β D (β Γ {π΄})) βΎ π)) |
44 | | xpssres 6019 |
. . . . . . . . . . . . 13
β’ (π β β β
((β Γ {π΄})
βΎ π) = (π Γ {π΄})) |
45 | 11, 44 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((β Γ {π΄}) βΎ π) = (π Γ {π΄})) |
46 | 45 | oveq2d 7425 |
. . . . . . . . . . 11
β’ (π β (π D ((β Γ {π΄}) βΎ π)) = (π D (π Γ {π΄}))) |
47 | 36 | reseq1d 5981 |
. . . . . . . . . . . 12
β’ (π β ((β D (β
Γ {π΄})) βΎ π) = ((β Γ {0})
βΎ π)) |
48 | | xpssres 6019 |
. . . . . . . . . . . . 13
β’ (π β β β
((β Γ {0}) βΎ π) = (π Γ {0})) |
49 | 11, 48 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((β Γ {0})
βΎ π) = (π Γ {0})) |
50 | 47, 49 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β ((β D (β
Γ {π΄})) βΎ π) = (π Γ {0})) |
51 | 43, 46, 50 | 3eqtr3d 2781 |
. . . . . . . . . 10
β’ (π β (π D (π Γ {π΄})) = (π Γ {0})) |
52 | | fconstmpt 5739 |
. . . . . . . . . 10
β’ (π Γ {0}) = (π₯ β π β¦ 0) |
53 | 51, 52 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π β (π D (π Γ {π΄})) = (π₯ β π β¦ 0)) |
54 | 20 | cnfldtopon 24299 |
. . . . . . . . . . . . 13
β’
(TopOpenββfld) β
(TopOnββ) |
55 | | resttopon 22665 |
. . . . . . . . . . . . 13
β’
(((TopOpenββfld) β (TopOnββ)
β§ π β β)
β ((TopOpenββfld) βΎt π) β (TopOnβπ)) |
56 | 54, 11, 55 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β
((TopOpenββfld) βΎt π) β (TopOnβπ)) |
57 | | topontop 22415 |
. . . . . . . . . . . 12
β’
(((TopOpenββfld) βΎt π) β (TopOnβπ) β
((TopOpenββfld) βΎt π) β Top) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
β’ (π β
((TopOpenββfld) βΎt π) β Top) |
59 | | toponuni 22416 |
. . . . . . . . . . . . 13
β’
(((TopOpenββfld) βΎt π) β (TopOnβπ) β π = βͺ
((TopOpenββfld) βΎt π)) |
60 | 56, 59 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π = βͺ
((TopOpenββfld) βΎt π)) |
61 | 19, 60 | sseqtrd 4023 |
. . . . . . . . . . 11
β’ (π β π β βͺ
((TopOpenββfld) βΎt π)) |
62 | | eqid 2733 |
. . . . . . . . . . . 12
β’ βͺ ((TopOpenββfld)
βΎt π) =
βͺ ((TopOpenββfld)
βΎt π) |
63 | 62 | ntrss2 22561 |
. . . . . . . . . . 11
β’
((((TopOpenββfld) βΎt π) β Top β§ π β βͺ ((TopOpenββfld)
βΎt π))
β ((intβ((TopOpenββfld) βΎt
π))βπ) β π) |
64 | 58, 61, 63 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β
((intβ((TopOpenββfld) βΎt π))βπ) β π) |
65 | 11, 7, 19, 21, 20 | dvbssntr 25417 |
. . . . . . . . . . 11
β’ (π β dom (π D πΉ) β
((intβ((TopOpenββfld) βΎt π))βπ)) |
66 | 16, 65 | eqsstrrd 4022 |
. . . . . . . . . 10
β’ (π β π β
((intβ((TopOpenββfld) βΎt π))βπ)) |
67 | 64, 66 | eqssd 4000 |
. . . . . . . . 9
β’ (π β
((intβ((TopOpenββfld) βΎt π))βπ) = π) |
68 | 53, 67 | reseq12d 5983 |
. . . . . . . 8
β’ (π β ((π D (π Γ {π΄})) βΎ
((intβ((TopOpenββfld) βΎt π))βπ)) = ((π₯ β π β¦ 0) βΎ π)) |
69 | | fconstmpt 5739 |
. . . . . . . . 9
β’ (π Γ {0}) = (π₯ β π β¦ 0) |
70 | 69 | a1i 11 |
. . . . . . . 8
β’ (π β (π Γ {0}) = (π₯ β π β¦ 0)) |
71 | 30, 68, 70 | 3eqtr4d 2783 |
. . . . . . 7
β’ (π β ((π D (π Γ {π΄})) βΎ
((intβ((TopOpenββfld) βΎt π))βπ)) = (π Γ {0})) |
72 | 23, 29, 71 | 3eqtr3d 2781 |
. . . . . 6
β’ (π β (π D (π Γ {π΄})) = (π Γ {0})) |
73 | 72 | feq1d 6703 |
. . . . 5
β’ (π β ((π D (π Γ {π΄})):πβΆ{0} β (π Γ {0}):πβΆ{0})) |
74 | 9, 73 | mpbiri 258 |
. . . 4
β’ (π β (π D (π Γ {π΄})):πβΆ{0}) |
75 | 74 | fdmd 6729 |
. . 3
β’ (π β dom (π D (π Γ {π΄})) = π) |
76 | 1, 6, 7, 75, 16 | dvmulf 25460 |
. 2
β’ (π β (π D ((π Γ {π΄}) βf Β· πΉ)) = (((π D (π Γ {π΄})) βf Β· πΉ) βf + ((π D πΉ) βf Β· (π Γ {π΄})))) |
77 | | sseqin2 4216 |
. . . . . 6
β’ (π β π β (π β© π) = π) |
78 | 19, 77 | sylib 217 |
. . . . 5
β’ (π β (π β© π) = π) |
79 | 78 | mpteq1d 5244 |
. . . 4
β’ (π β (π₯ β (π β© π) β¦ (π΄ Β· (πΉβπ₯))) = (π₯ β π β¦ (π΄ Β· (πΉβπ₯)))) |
80 | 13 | ffnd 6719 |
. . . . 5
β’ (π β (π Γ {π΄}) Fn π) |
81 | 7 | ffnd 6719 |
. . . . 5
β’ (π β πΉ Fn π) |
82 | 1, 19 | ssexd 5325 |
. . . . 5
β’ (π β π β V) |
83 | | eqid 2733 |
. . . . 5
β’ (π β© π) = (π β© π) |
84 | | fvconst2g 7203 |
. . . . . 6
β’ ((π΄ β β β§ π₯ β π) β ((π Γ {π΄})βπ₯) = π΄) |
85 | 2, 84 | sylan 581 |
. . . . 5
β’ ((π β§ π₯ β π) β ((π Γ {π΄})βπ₯) = π΄) |
86 | | eqidd 2734 |
. . . . 5
β’ ((π β§ π₯ β π) β (πΉβπ₯) = (πΉβπ₯)) |
87 | 80, 81, 1, 82, 83, 85, 86 | offval 7679 |
. . . 4
β’ (π β ((π Γ {π΄}) βf Β· πΉ) = (π₯ β (π β© π) β¦ (π΄ Β· (πΉβπ₯)))) |
88 | 4 | ffnd 6719 |
. . . . 5
β’ (π β (π Γ {π΄}) Fn π) |
89 | | inidm 4219 |
. . . . 5
β’ (π β© π) = π |
90 | | fvconst2g 7203 |
. . . . . 6
β’ ((π΄ β β β§ π₯ β π) β ((π Γ {π΄})βπ₯) = π΄) |
91 | 2, 90 | sylan 581 |
. . . . 5
β’ ((π β§ π₯ β π) β ((π Γ {π΄})βπ₯) = π΄) |
92 | 88, 81, 82, 82, 89, 91, 86 | offval 7679 |
. . . 4
β’ (π β ((π Γ {π΄}) βf Β· πΉ) = (π₯ β π β¦ (π΄ Β· (πΉβπ₯)))) |
93 | 79, 87, 92 | 3eqtr4d 2783 |
. . 3
β’ (π β ((π Γ {π΄}) βf Β· πΉ) = ((π Γ {π΄}) βf Β· πΉ)) |
94 | 93 | oveq2d 7425 |
. 2
β’ (π β (π D ((π Γ {π΄}) βf Β· πΉ)) = (π D ((π Γ {π΄}) βf Β· πΉ))) |
95 | 78 | mpteq1d 5244 |
. . 3
β’ (π β (π₯ β (π β© π) β¦ (π΄ Β· ((π D πΉ)βπ₯))) = (π₯ β π β¦ (π΄ Β· ((π D πΉ)βπ₯)))) |
96 | | dvfg 25423 |
. . . . . . 7
β’ (π β {β, β}
β (π D πΉ):dom (π D πΉ)βΆβ) |
97 | 1, 96 | syl 17 |
. . . . . 6
β’ (π β (π D πΉ):dom (π D πΉ)βΆβ) |
98 | 16 | feq2d 6704 |
. . . . . 6
β’ (π β ((π D πΉ):dom (π D πΉ)βΆβ β (π D πΉ):πβΆβ)) |
99 | 97, 98 | mpbid 231 |
. . . . 5
β’ (π β (π D πΉ):πβΆβ) |
100 | 99 | ffnd 6719 |
. . . 4
β’ (π β (π D πΉ) Fn π) |
101 | | eqidd 2734 |
. . . 4
β’ ((π β§ π₯ β π) β ((π D πΉ)βπ₯) = ((π D πΉ)βπ₯)) |
102 | 80, 100, 1, 82, 83, 85, 101 | offval 7679 |
. . 3
β’ (π β ((π Γ {π΄}) βf Β· (π D πΉ)) = (π₯ β (π β© π) β¦ (π΄ Β· ((π D πΉ)βπ₯)))) |
103 | | 0cnd 11207 |
. . . . 5
β’ ((π β§ π₯ β π) β 0 β β) |
104 | | ovexd 7444 |
. . . . 5
β’ ((π β§ π₯ β π) β (((π D πΉ)βπ₯) Β· π΄) β V) |
105 | 72 | oveq1d 7424 |
. . . . . . 7
β’ (π β ((π D (π Γ {π΄})) βf Β· πΉ) = ((π Γ {0}) βf Β·
πΉ)) |
106 | | 0cnd 11207 |
. . . . . . . 8
β’ (π β 0 β
β) |
107 | | mul02 11392 |
. . . . . . . . 9
β’ (π₯ β β β (0
Β· π₯) =
0) |
108 | 107 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (0 Β· π₯) = 0) |
109 | 82, 7, 106, 106, 108 | caofid2 7704 |
. . . . . . 7
β’ (π β ((π Γ {0}) βf Β·
πΉ) = (π Γ {0})) |
110 | 105, 109 | eqtrd 2773 |
. . . . . 6
β’ (π β ((π D (π Γ {π΄})) βf Β· πΉ) = (π Γ {0})) |
111 | 110, 69 | eqtrdi 2789 |
. . . . 5
β’ (π β ((π D (π Γ {π΄})) βf Β· πΉ) = (π₯ β π β¦ 0)) |
112 | | fvexd 6907 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((π D πΉ)βπ₯) β V) |
113 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π) β π΄ β β) |
114 | 99 | feqmptd 6961 |
. . . . . 6
β’ (π β (π D πΉ) = (π₯ β π β¦ ((π D πΉ)βπ₯))) |
115 | 27 | a1i 11 |
. . . . . 6
β’ (π β (π Γ {π΄}) = (π₯ β π β¦ π΄)) |
116 | 82, 112, 113, 114, 115 | offval2 7690 |
. . . . 5
β’ (π β ((π D πΉ) βf Β· (π Γ {π΄})) = (π₯ β π β¦ (((π D πΉ)βπ₯) Β· π΄))) |
117 | 82, 103, 104, 111, 116 | offval2 7690 |
. . . 4
β’ (π β (((π D (π Γ {π΄})) βf Β· πΉ) βf + ((π D πΉ) βf Β· (π Γ {π΄}))) = (π₯ β π β¦ (0 + (((π D πΉ)βπ₯) Β· π΄)))) |
118 | 99 | ffvelcdmda 7087 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β ((π D πΉ)βπ₯) β β) |
119 | 118, 113 | mulcld 11234 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (((π D πΉ)βπ₯) Β· π΄) β β) |
120 | 119 | addlidd 11415 |
. . . . . 6
β’ ((π β§ π₯ β π) β (0 + (((π D πΉ)βπ₯) Β· π΄)) = (((π D πΉ)βπ₯) Β· π΄)) |
121 | 118, 113 | mulcomd 11235 |
. . . . . 6
β’ ((π β§ π₯ β π) β (((π D πΉ)βπ₯) Β· π΄) = (π΄ Β· ((π D πΉ)βπ₯))) |
122 | 120, 121 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π₯ β π) β (0 + (((π D πΉ)βπ₯) Β· π΄)) = (π΄ Β· ((π D πΉ)βπ₯))) |
123 | 122 | mpteq2dva 5249 |
. . . 4
β’ (π β (π₯ β π β¦ (0 + (((π D πΉ)βπ₯) Β· π΄))) = (π₯ β π β¦ (π΄ Β· ((π D πΉ)βπ₯)))) |
124 | 117, 123 | eqtrd 2773 |
. . 3
β’ (π β (((π D (π Γ {π΄})) βf Β· πΉ) βf + ((π D πΉ) βf Β· (π Γ {π΄}))) = (π₯ β π β¦ (π΄ Β· ((π D πΉ)βπ₯)))) |
125 | 95, 102, 124 | 3eqtr4d 2783 |
. 2
β’ (π β ((π Γ {π΄}) βf Β· (π D πΉ)) = (((π D (π Γ {π΄})) βf Β· πΉ) βf + ((π D πΉ) βf Β· (π Γ {π΄})))) |
126 | 76, 94, 125 | 3eqtr4d 2783 |
1
β’ (π β (π D ((π Γ {π΄}) βf Β· πΉ)) = ((π Γ {π΄}) βf Β· (π D πΉ))) |