Step | Hyp | Ref
| Expression |
1 | | dv11cn.f |
. . . . 5
β’ (π β πΉ:πβΆβ) |
2 | 1 | ffnd 6673 |
. . . 4
β’ (π β πΉ Fn π) |
3 | | dv11cn.g |
. . . . 5
β’ (π β πΊ:πβΆβ) |
4 | 3 | ffnd 6673 |
. . . 4
β’ (π β πΊ Fn π) |
5 | | dv11cn.x |
. . . . . 6
β’ π = (π΄(ballβ(abs β β ))π
) |
6 | 5 | ovexi 7395 |
. . . . 5
β’ π β V |
7 | 6 | a1i 11 |
. . . 4
β’ (π β π β V) |
8 | | inidm 4182 |
. . . 4
β’ (π β© π) = π |
9 | 2, 4, 7, 7, 8 | offn 7634 |
. . 3
β’ (π β (πΉ βf β πΊ) Fn π) |
10 | | 0cn 11155 |
. . . 4
β’ 0 β
β |
11 | | fnconstg 6734 |
. . . 4
β’ (0 β
β β (π Γ
{0}) Fn π) |
12 | 10, 11 | mp1i 13 |
. . 3
β’ (π β (π Γ {0}) Fn π) |
13 | | subcl 11408 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β (π₯ β π¦) β β) |
14 | 13 | adantl 483 |
. . . . . . 7
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ β π¦) β β) |
15 | 14, 1, 3, 7, 7, 8 | off 7639 |
. . . . . 6
β’ (π β (πΉ βf β πΊ):πβΆβ) |
16 | 15 | ffvelcdmda 7039 |
. . . . 5
β’ ((π β§ π₯ β π) β ((πΉ βf β πΊ)βπ₯) β β) |
17 | | dv11cn.c |
. . . . . . . . 9
β’ (π β πΆ β π) |
18 | 17 | anim1ci 617 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (π₯ β π β§ πΆ β π)) |
19 | | cnxmet 24159 |
. . . . . . . . . . 11
β’ (abs
β β ) β (βMetββ) |
20 | | dv11cn.a |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
21 | | dv11cn.r |
. . . . . . . . . . 11
β’ (π β π
β
β*) |
22 | | blssm 23794 |
. . . . . . . . . . 11
β’ (((abs
β β ) β (βMetββ) β§ π΄ β β β§ π
β β*) β (π΄(ballβ(abs β β
))π
) β
β) |
23 | 19, 20, 21, 22 | mp3an2i 1467 |
. . . . . . . . . 10
β’ (π β (π΄(ballβ(abs β β ))π
) β
β) |
24 | 5, 23 | eqsstrid 3996 |
. . . . . . . . 9
β’ (π β π β β) |
25 | 1 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π) β (πΉβπ₯) β β) |
26 | 3 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π) β (πΊβπ₯) β β) |
27 | 1 | feqmptd 6914 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ = (π₯ β π β¦ (πΉβπ₯))) |
28 | 3 | feqmptd 6914 |
. . . . . . . . . . . . . . 15
β’ (π β πΊ = (π₯ β π β¦ (πΊβπ₯))) |
29 | 7, 25, 26, 27, 28 | offval2 7641 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ βf β πΊ) = (π₯ β π β¦ ((πΉβπ₯) β (πΊβπ₯)))) |
30 | 29 | oveq2d 7377 |
. . . . . . . . . . . . 13
β’ (π β (β D (πΉ βf β
πΊ)) = (β D (π₯ β π β¦ ((πΉβπ₯) β (πΊβπ₯))))) |
31 | | cnelprrecn 11152 |
. . . . . . . . . . . . . . 15
β’ β
β {β, β} |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β β {β,
β}) |
33 | | fvexd 6861 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β ((β D πΉ)βπ₯) β V) |
34 | 27 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’ (π β (β D πΉ) = (β D (π₯ β π β¦ (πΉβπ₯)))) |
35 | | dvfcn 25295 |
. . . . . . . . . . . . . . . . 17
β’ (β
D πΉ):dom (β D πΉ)βΆβ |
36 | | dv11cn.d |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom (β D πΉ) = π) |
37 | 36 | feq2d 6658 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((β D πΉ):dom (β D πΉ)βΆβ β (β
D πΉ):πβΆβ)) |
38 | 35, 37 | mpbii 232 |
. . . . . . . . . . . . . . . 16
β’ (π β (β D πΉ):πβΆβ) |
39 | 38 | feqmptd 6914 |
. . . . . . . . . . . . . . 15
β’ (π β (β D πΉ) = (π₯ β π β¦ ((β D πΉ)βπ₯))) |
40 | 34, 39 | eqtr3d 2775 |
. . . . . . . . . . . . . 14
β’ (π β (β D (π₯ β π β¦ (πΉβπ₯))) = (π₯ β π β¦ ((β D πΉ)βπ₯))) |
41 | | dv11cn.e |
. . . . . . . . . . . . . . 15
β’ (π β (β D πΉ) = (β D πΊ)) |
42 | 28 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’ (π β (β D πΊ) = (β D (π₯ β π β¦ (πΊβπ₯)))) |
43 | 41, 39, 42 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . 14
β’ (π β (β D (π₯ β π β¦ (πΊβπ₯))) = (π₯ β π β¦ ((β D πΉ)βπ₯))) |
44 | 32, 25, 33, 40, 26, 33, 43 | dvmptsub 25354 |
. . . . . . . . . . . . 13
β’ (π β (β D (π₯ β π β¦ ((πΉβπ₯) β (πΊβπ₯)))) = (π₯ β π β¦ (((β D πΉ)βπ₯) β ((β D πΉ)βπ₯)))) |
45 | 38 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π) β ((β D πΉ)βπ₯) β β) |
46 | 45 | subidd 11508 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π) β (((β D πΉ)βπ₯) β ((β D πΉ)βπ₯)) = 0) |
47 | 46 | mpteq2dva 5209 |
. . . . . . . . . . . . . 14
β’ (π β (π₯ β π β¦ (((β D πΉ)βπ₯) β ((β D πΉ)βπ₯))) = (π₯ β π β¦ 0)) |
48 | | fconstmpt 5698 |
. . . . . . . . . . . . . 14
β’ (π Γ {0}) = (π₯ β π β¦ 0) |
49 | 47, 48 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ (π β (π₯ β π β¦ (((β D πΉ)βπ₯) β ((β D πΉ)βπ₯))) = (π Γ {0})) |
50 | 30, 44, 49 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π β (β D (πΉ βf β
πΊ)) = (π Γ {0})) |
51 | 50 | dmeqd 5865 |
. . . . . . . . . . 11
β’ (π β dom (β D (πΉ βf β
πΊ)) = dom (π Γ {0})) |
52 | | snnzg 4739 |
. . . . . . . . . . . 12
β’ (0 β
β β {0} β β
) |
53 | | dmxp 5888 |
. . . . . . . . . . . 12
β’ ({0} β
β
β dom (π
Γ {0}) = π) |
54 | 10, 52, 53 | mp2b 10 |
. . . . . . . . . . 11
β’ dom
(π Γ {0}) = π |
55 | 51, 54 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π β dom (β D (πΉ βf β
πΊ)) = π) |
56 | | eqimss2 4005 |
. . . . . . . . . 10
β’ (dom
(β D (πΉ
βf β πΊ)) = π β π β dom (β D (πΉ βf β πΊ))) |
57 | 55, 56 | syl 17 |
. . . . . . . . 9
β’ (π β π β dom (β D (πΉ βf β πΊ))) |
58 | | 0red 11166 |
. . . . . . . . 9
β’ (π β 0 β
β) |
59 | 50 | fveq1d 6848 |
. . . . . . . . . . . 12
β’ (π β ((β D (πΉ βf β
πΊ))βπ₯) = ((π Γ {0})βπ₯)) |
60 | | c0ex 11157 |
. . . . . . . . . . . . 13
β’ 0 β
V |
61 | 60 | fvconst2 7157 |
. . . . . . . . . . . 12
β’ (π₯ β π β ((π Γ {0})βπ₯) = 0) |
62 | 59, 61 | sylan9eq 2793 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β ((β D (πΉ βf β πΊ))βπ₯) = 0) |
63 | 62 | abs00bd 15185 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (absβ((β D (πΉ βf β
πΊ))βπ₯)) = 0) |
64 | | 0le0 12262 |
. . . . . . . . . 10
β’ 0 β€
0 |
65 | 63, 64 | eqbrtrdi 5148 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (absβ((β D (πΉ βf β
πΊ))βπ₯)) β€ 0) |
66 | 24, 15, 20, 21, 5, 57, 58, 65 | dvlipcn 25381 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ πΆ β π)) β (absβ(((πΉ βf β πΊ)βπ₯) β ((πΉ βf β πΊ)βπΆ))) β€ (0 Β· (absβ(π₯ β πΆ)))) |
67 | 18, 66 | syldan 592 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (absβ(((πΉ βf β πΊ)βπ₯) β ((πΉ βf β πΊ)βπΆ))) β€ (0 Β· (absβ(π₯ β πΆ)))) |
68 | 29 | fveq1d 6848 |
. . . . . . . . . . . 12
β’ (π β ((πΉ βf β πΊ)βπΆ) = ((π₯ β π β¦ ((πΉβπ₯) β (πΊβπ₯)))βπΆ)) |
69 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π₯ = πΆ β (πΉβπ₯) = (πΉβπΆ)) |
70 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π₯ = πΆ β (πΊβπ₯) = (πΊβπΆ)) |
71 | 69, 70 | oveq12d 7379 |
. . . . . . . . . . . . . 14
β’ (π₯ = πΆ β ((πΉβπ₯) β (πΊβπ₯)) = ((πΉβπΆ) β (πΊβπΆ))) |
72 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β¦ ((πΉβπ₯) β (πΊβπ₯))) = (π₯ β π β¦ ((πΉβπ₯) β (πΊβπ₯))) |
73 | | ovex 7394 |
. . . . . . . . . . . . . 14
β’ ((πΉβπΆ) β (πΊβπΆ)) β V |
74 | 71, 72, 73 | fvmpt 6952 |
. . . . . . . . . . . . 13
β’ (πΆ β π β ((π₯ β π β¦ ((πΉβπ₯) β (πΊβπ₯)))βπΆ) = ((πΉβπΆ) β (πΊβπΆ))) |
75 | 17, 74 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((π₯ β π β¦ ((πΉβπ₯) β (πΊβπ₯)))βπΆ) = ((πΉβπΆ) β (πΊβπΆ))) |
76 | 1, 17 | ffvelcdmd 7040 |
. . . . . . . . . . . . 13
β’ (π β (πΉβπΆ) β β) |
77 | | dv11cn.p |
. . . . . . . . . . . . 13
β’ (π β (πΉβπΆ) = (πΊβπΆ)) |
78 | 76, 77 | subeq0bd 11589 |
. . . . . . . . . . . 12
β’ (π β ((πΉβπΆ) β (πΊβπΆ)) = 0) |
79 | 68, 75, 78 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ (π β ((πΉ βf β πΊ)βπΆ) = 0) |
80 | 79 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β ((πΉ βf β πΊ)βπΆ) = 0) |
81 | 80 | oveq2d 7377 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (((πΉ βf β πΊ)βπ₯) β ((πΉ βf β πΊ)βπΆ)) = (((πΉ βf β πΊ)βπ₯) β 0)) |
82 | 16 | subid1d 11509 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (((πΉ βf β πΊ)βπ₯) β 0) = ((πΉ βf β πΊ)βπ₯)) |
83 | 81, 82 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (((πΉ βf β πΊ)βπ₯) β ((πΉ βf β πΊ)βπΆ)) = ((πΉ βf β πΊ)βπ₯)) |
84 | 83 | fveq2d 6850 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (absβ(((πΉ βf β πΊ)βπ₯) β ((πΉ βf β πΊ)βπΆ))) = (absβ((πΉ βf β πΊ)βπ₯))) |
85 | 24 | sselda 3948 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β π₯ β β) |
86 | 24, 17 | sseldd 3949 |
. . . . . . . . . . . 12
β’ (π β πΆ β β) |
87 | 86 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β πΆ β β) |
88 | 85, 87 | subcld 11520 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (π₯ β πΆ) β β) |
89 | 88 | abscld 15330 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (absβ(π₯ β πΆ)) β β) |
90 | 89 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (absβ(π₯ β πΆ)) β β) |
91 | 90 | mul02d 11361 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (0 Β· (absβ(π₯ β πΆ))) = 0) |
92 | 67, 84, 91 | 3brtr3d 5140 |
. . . . . 6
β’ ((π β§ π₯ β π) β (absβ((πΉ βf β πΊ)βπ₯)) β€ 0) |
93 | 16 | absge0d 15338 |
. . . . . 6
β’ ((π β§ π₯ β π) β 0 β€ (absβ((πΉ βf β
πΊ)βπ₯))) |
94 | 16 | abscld 15330 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (absβ((πΉ βf β πΊ)βπ₯)) β β) |
95 | | 0re 11165 |
. . . . . . 7
β’ 0 β
β |
96 | | letri3 11248 |
. . . . . . 7
β’
(((absβ((πΉ
βf β πΊ)βπ₯)) β β β§ 0 β β)
β ((absβ((πΉ
βf β πΊ)βπ₯)) = 0 β ((absβ((πΉ βf β πΊ)βπ₯)) β€ 0 β§ 0 β€ (absβ((πΉ βf β
πΊ)βπ₯))))) |
97 | 94, 95, 96 | sylancl 587 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((absβ((πΉ βf β πΊ)βπ₯)) = 0 β ((absβ((πΉ βf β πΊ)βπ₯)) β€ 0 β§ 0 β€ (absβ((πΉ βf β
πΊ)βπ₯))))) |
98 | 92, 93, 97 | mpbir2and 712 |
. . . . 5
β’ ((π β§ π₯ β π) β (absβ((πΉ βf β πΊ)βπ₯)) = 0) |
99 | 16, 98 | abs00d 15340 |
. . . 4
β’ ((π β§ π₯ β π) β ((πΉ βf β πΊ)βπ₯) = 0) |
100 | 61 | adantl 483 |
. . . 4
β’ ((π β§ π₯ β π) β ((π Γ {0})βπ₯) = 0) |
101 | 99, 100 | eqtr4d 2776 |
. . 3
β’ ((π β§ π₯ β π) β ((πΉ βf β πΊ)βπ₯) = ((π Γ {0})βπ₯)) |
102 | 9, 12, 101 | eqfnfvd 6989 |
. 2
β’ (π β (πΉ βf β πΊ) = (π Γ {0})) |
103 | | ofsubeq0 12158 |
. . 3
β’ ((π β V β§ πΉ:πβΆβ β§ πΊ:πβΆβ) β ((πΉ βf β πΊ) = (π Γ {0}) β πΉ = πΊ)) |
104 | 6, 1, 3, 103 | mp3an2i 1467 |
. 2
β’ (π β ((πΉ βf β πΊ) = (π Γ {0}) β πΉ = πΊ)) |
105 | 102, 104 | mpbid 231 |
1
β’ (π β πΉ = πΊ) |