Step | Hyp | Ref
| Expression |
1 | | dvfcn 25759 |
. . . . . . 7
β’ (β
D exp):dom (β D exp)βΆβ |
2 | | dvbsss 25753 |
. . . . . . . . 9
β’ dom
(β D exp) β β |
3 | | subcl 11456 |
. . . . . . . . . . . . . . . . . 18
β’ ((π§ β β β§ π₯ β β) β (π§ β π₯) β β) |
4 | 3 | ancoms 458 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π§ β β) β (π§ β π₯) β β) |
5 | | efadd 16034 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ (π§ β π₯) β β) β (expβ(π₯ + (π§ β π₯))) = ((expβπ₯) Β· (expβ(π§ β π₯)))) |
6 | 4, 5 | syldan 590 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π§ β β) β
(expβ(π₯ + (π§ β π₯))) = ((expβπ₯) Β· (expβ(π§ β π₯)))) |
7 | | pncan3 11465 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π§ β β) β (π₯ + (π§ β π₯)) = π§) |
8 | 7 | fveq2d 6885 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π§ β β) β
(expβ(π₯ + (π§ β π₯))) = (expβπ§)) |
9 | 6, 8 | eqtr3d 2766 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π§ β β) β
((expβπ₯) Β·
(expβ(π§ β π₯))) = (expβπ§)) |
10 | 9 | mpteq2dva 5238 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (π§ β β β¦
((expβπ₯) Β·
(expβ(π§ β π₯)))) = (π§ β β β¦ (expβπ§))) |
11 | | cnex 11187 |
. . . . . . . . . . . . . . . 16
β’ β
β V |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β β
β V) |
13 | | fvexd 6896 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π§ β β) β
(expβπ₯) β
V) |
14 | | fvexd 6896 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π§ β β) β
(expβ(π§ β π₯)) β V) |
15 | | fconstmpt 5728 |
. . . . . . . . . . . . . . . 16
β’ (β
Γ {(expβπ₯)}) =
(π§ β β β¦
(expβπ₯)) |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β (β
Γ {(expβπ₯)}) =
(π§ β β β¦
(expβπ₯))) |
17 | | eqidd 2725 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β (π§ β β β¦
(expβ(π§ β π₯))) = (π§ β β β¦ (expβ(π§ β π₯)))) |
18 | 12, 13, 14, 16, 17 | offval2 7683 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β ((β
Γ {(expβπ₯)})
βf Β· (π§ β β β¦ (expβ(π§ β π₯)))) = (π§ β β β¦ ((expβπ₯) Β· (expβ(π§ β π₯))))) |
19 | | eff 16022 |
. . . . . . . . . . . . . . . 16
β’
exp:ββΆβ |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β
exp:ββΆβ) |
21 | 20 | feqmptd 6950 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β exp =
(π§ β β β¦
(expβπ§))) |
22 | 10, 18, 21 | 3eqtr4d 2774 |
. . . . . . . . . . . . 13
β’ (π₯ β β β ((β
Γ {(expβπ₯)})
βf Β· (π§ β β β¦ (expβ(π§ β π₯)))) = exp) |
23 | 22 | oveq2d 7417 |
. . . . . . . . . . . 12
β’ (π₯ β β β (β
D ((β Γ {(expβπ₯)}) βf Β· (π§ β β β¦
(expβ(π§ β π₯))))) = (β D
exp)) |
24 | | efcl 16023 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β
(expβπ₯) β
β) |
25 | | fconstg 6768 |
. . . . . . . . . . . . . . . 16
β’
((expβπ₯)
β β β (β Γ {(expβπ₯)}):ββΆ{(expβπ₯)}) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β (β
Γ {(expβπ₯)}):ββΆ{(expβπ₯)}) |
27 | 24 | snssd 4804 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β
{(expβπ₯)} β
β) |
28 | 26, 27 | fssd 6725 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (β
Γ {(expβπ₯)}):ββΆβ) |
29 | | ssidd 3997 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β β
β β) |
30 | | efcl 16023 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β π₯) β β β (expβ(π§ β π₯)) β β) |
31 | 4, 30 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π§ β β) β
(expβ(π§ β π₯)) β
β) |
32 | 31 | fmpttd 7106 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (π§ β β β¦
(expβ(π§ β π₯))):ββΆβ) |
33 | | c0ex 11205 |
. . . . . . . . . . . . . . . . . 18
β’ 0 β
V |
34 | 33 | snid 4656 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
{0} |
35 | | opelxpi 5703 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ 0 β
{0}) β β¨π₯,
0β© β (β Γ {0})) |
36 | 34, 35 | mpan2 688 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β
β¨π₯, 0β© β
(β Γ {0})) |
37 | | dvconst 25768 |
. . . . . . . . . . . . . . . . 17
β’
((expβπ₯)
β β β (β D (β Γ {(expβπ₯)})) = (β Γ
{0})) |
38 | 24, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β (β
D (β Γ {(expβπ₯)})) = (β Γ
{0})) |
39 | 36, 38 | eleqtrrd 2828 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β
β¨π₯, 0β© β
(β D (β Γ {(expβπ₯)}))) |
40 | | df-br 5139 |
. . . . . . . . . . . . . . 15
β’ (π₯(β D (β Γ
{(expβπ₯)}))0 β
β¨π₯, 0β© β
(β D (β Γ {(expβπ₯)}))) |
41 | 39, 40 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β π₯(β D (β Γ
{(expβπ₯)}))0) |
42 | 20, 4 | cofmpt 7122 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β (exp
β (π§ β β
β¦ (π§ β π₯))) = (π§ β β β¦ (expβ(π§ β π₯)))) |
43 | 42 | oveq2d 7417 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β (β
D (exp β (π§ β
β β¦ (π§ β
π₯)))) = (β D (π§ β β β¦
(expβ(π§ β π₯))))) |
44 | 4 | fmpttd 7106 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β β (π§ β β β¦ (π§ β π₯)):ββΆβ) |
45 | | oveq1 7408 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = π₯ β (π§ β π₯) = (π₯ β π₯)) |
46 | | eqid 2724 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ β β β¦ (π§ β π₯)) = (π§ β β β¦ (π§ β π₯)) |
47 | | ovex 7434 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β π₯) β V |
48 | 45, 46, 47 | fvmpt 6988 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β ((π§ β β β¦ (π§ β π₯))βπ₯) = (π₯ β π₯)) |
49 | | subid 11476 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β (π₯ β π₯) = 0) |
50 | 48, 49 | eqtrd 2764 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β ((π§ β β β¦ (π§ β π₯))βπ₯) = 0) |
51 | | dveflem 25833 |
. . . . . . . . . . . . . . . . . 18
β’ 0(β
D exp)1 |
52 | 50, 51 | eqbrtrdi 5177 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β β ((π§ β β β¦ (π§ β π₯))βπ₯)(β D exp)1) |
53 | | 1ex 11207 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 1 β
V |
54 | 53 | snid 4656 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 β
{1} |
55 | | opelxpi 5703 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β β β§ 1 β
{1}) β β¨π₯,
1β© β (β Γ {1})) |
56 | 54, 55 | mpan2 688 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β
β¨π₯, 1β© β
(β Γ {1})) |
57 | | cnelprrecn 11199 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ β
β {β, β} |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β β β β
β {β, β}) |
59 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β β β§ π§ β β) β π§ β
β) |
60 | | 1cnd 11206 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β β β§ π§ β β) β 1 β
β) |
61 | 58 | dvmptid 25811 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β β β (β
D (π§ β β β¦
π§)) = (π§ β β β¦ 1)) |
62 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β β β§ π§ β β) β π₯ β
β) |
63 | | 0cnd 11204 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β β β§ π§ β β) β 0 β
β) |
64 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β β β π₯ β
β) |
65 | 58, 64 | dvmptc 25812 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β β β (β
D (π§ β β β¦
π₯)) = (π§ β β β¦ 0)) |
66 | 58, 59, 60, 61, 62, 63, 65 | dvmptsub 25821 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β β (β
D (π§ β β β¦
(π§ β π₯))) = (π§ β β β¦ (1 β
0))) |
67 | | 1m0e1 12330 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1
β 0) = 1 |
68 | 67 | mpteq2i 5243 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ β β β¦ (1
β 0)) = (π§ β
β β¦ 1) |
69 | | fconstmpt 5728 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β
Γ {1}) = (π§ β
β β¦ 1) |
70 | 68, 69 | eqtr4i 2755 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ β β β¦ (1
β 0)) = (β Γ {1}) |
71 | 66, 70 | eqtrdi 2780 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β (β
D (π§ β β β¦
(π§ β π₯))) = (β Γ
{1})) |
72 | 56, 71 | eleqtrrd 2828 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β
β¨π₯, 1β© β
(β D (π§ β
β β¦ (π§ β
π₯)))) |
73 | | df-br 5139 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯(β D (π§ β β β¦ (π§ β π₯)))1 β β¨π₯, 1β© β (β D (π§ β β β¦ (π§ β π₯)))) |
74 | 72, 73 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β β π₯(β D (π§ β β β¦ (π§ β π₯)))1) |
75 | | eqid 2724 |
. . . . . . . . . . . . . . . . 17
β’
(TopOpenββfld) =
(TopOpenββfld) |
76 | 20, 29, 44, 29, 29, 29, 52, 74, 75 | dvcobr 25799 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β π₯(β D (exp β (π§ β β β¦ (π§ β π₯))))(1 Β· 1)) |
77 | | 1t1e1 12371 |
. . . . . . . . . . . . . . . 16
β’ (1
Β· 1) = 1 |
78 | 76, 77 | breqtrdi 5179 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β π₯(β D (exp β (π§ β β β¦ (π§ β π₯))))1) |
79 | 43, 78 | breqdi 5153 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β π₯(β D (π§ β β β¦ (expβ(π§ β π₯))))1) |
80 | 28, 29, 32, 29, 29, 41, 79, 75 | dvmulbr 25791 |
. . . . . . . . . . . . 13
β’ (π₯ β β β π₯(β D ((β Γ
{(expβπ₯)})
βf Β· (π§ β β β¦ (expβ(π§ β π₯)))))((0 Β· ((π§ β β β¦ (expβ(π§ β π₯)))βπ₯)) + (1 Β· ((β Γ
{(expβπ₯)})βπ₯)))) |
81 | 32, 64 | ffvelcdmd 7077 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β ((π§ β β β¦
(expβ(π§ β π₯)))βπ₯) β β) |
82 | 81 | mul02d 11409 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β (0
Β· ((π§ β β
β¦ (expβ(π§
β π₯)))βπ₯)) = 0) |
83 | | fvex 6894 |
. . . . . . . . . . . . . . . . . 18
β’
(expβπ₯) β
V |
84 | 83 | fvconst2 7197 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β β ((β
Γ {(expβπ₯)})βπ₯) = (expβπ₯)) |
85 | 84 | oveq2d 7417 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β (1
Β· ((β Γ {(expβπ₯)})βπ₯)) = (1 Β· (expβπ₯))) |
86 | 24 | mullidd 11229 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β (1
Β· (expβπ₯)) =
(expβπ₯)) |
87 | 85, 86 | eqtrd 2764 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β (1
Β· ((β Γ {(expβπ₯)})βπ₯)) = (expβπ₯)) |
88 | 82, 87 | oveq12d 7419 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β ((0
Β· ((π§ β β
β¦ (expβ(π§
β π₯)))βπ₯)) + (1 Β· ((β
Γ {(expβπ₯)})βπ₯))) = (0 + (expβπ₯))) |
89 | 24 | addlidd 11412 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (0 +
(expβπ₯)) =
(expβπ₯)) |
90 | 88, 89 | eqtrd 2764 |
. . . . . . . . . . . . 13
β’ (π₯ β β β ((0
Β· ((π§ β β
β¦ (expβ(π§
β π₯)))βπ₯)) + (1 Β· ((β
Γ {(expβπ₯)})βπ₯))) = (expβπ₯)) |
91 | 80, 90 | breqtrd 5164 |
. . . . . . . . . . . 12
β’ (π₯ β β β π₯(β D ((β Γ
{(expβπ₯)})
βf Β· (π§ β β β¦ (expβ(π§ β π₯)))))(expβπ₯)) |
92 | 23, 91 | breqdi 5153 |
. . . . . . . . . . 11
β’ (π₯ β β β π₯(β D exp)(expβπ₯)) |
93 | | vex 3470 |
. . . . . . . . . . . 12
β’ π₯ β V |
94 | 93, 83 | breldm 5898 |
. . . . . . . . . . 11
β’ (π₯(β D exp)(expβπ₯) β π₯ β dom (β D exp)) |
95 | 92, 94 | syl 17 |
. . . . . . . . . 10
β’ (π₯ β β β π₯ β dom (β D
exp)) |
96 | 95 | ssriv 3978 |
. . . . . . . . 9
β’ β
β dom (β D exp) |
97 | 2, 96 | eqssi 3990 |
. . . . . . . 8
β’ dom
(β D exp) = β |
98 | 97 | feq2i 6699 |
. . . . . . 7
β’ ((β
D exp):dom (β D exp)βΆβ β (β D
exp):ββΆβ) |
99 | 1, 98 | mpbi 229 |
. . . . . 6
β’ (β
D exp):ββΆβ |
100 | 99 | a1i 11 |
. . . . 5
β’ (β€
β (β D exp):ββΆβ) |
101 | 100 | feqmptd 6950 |
. . . 4
β’ (β€
β (β D exp) = (π₯
β β β¦ ((β D exp)βπ₯))) |
102 | | ffun 6710 |
. . . . . . 7
β’ ((β
D exp):dom (β D exp)βΆβ β Fun (β D
exp)) |
103 | 1, 102 | ax-mp 5 |
. . . . . 6
β’ Fun
(β D exp) |
104 | | funbrfv 6932 |
. . . . . 6
β’ (Fun
(β D exp) β (π₯(β D exp)(expβπ₯) β ((β D exp)βπ₯) = (expβπ₯))) |
105 | 103, 92, 104 | mpsyl 68 |
. . . . 5
β’ (π₯ β β β ((β
D exp)βπ₯) =
(expβπ₯)) |
106 | 105 | mpteq2ia 5241 |
. . . 4
β’ (π₯ β β β¦
((β D exp)βπ₯))
= (π₯ β β β¦
(expβπ₯)) |
107 | 101, 106 | eqtrdi 2780 |
. . 3
β’ (β€
β (β D exp) = (π₯
β β β¦ (expβπ₯))) |
108 | 19 | a1i 11 |
. . . 4
β’ (β€
β exp:ββΆβ) |
109 | 108 | feqmptd 6950 |
. . 3
β’ (β€
β exp = (π₯ β
β β¦ (expβπ₯))) |
110 | 107, 109 | eqtr4d 2767 |
. 2
β’ (β€
β (β D exp) = exp) |
111 | 110 | mptru 1540 |
1
β’ (β
D exp) = exp |