Metamath Proof Explorer


Theorem efopn

Description: The exponential map is an open map. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypothesis efopn.j J = TopOpen fld
Assertion efopn S J exp S J

Proof

Step Hyp Ref Expression
1 efopn.j J = TopOpen fld
2 1 cnfldtopon J TopOn
3 toponss J TopOn S J S
4 2 3 mpan S J S
5 4 sselda S J x S x
6 cnxmet abs ∞Met
7 pirp π +
8 1 cnfldtopn J = MetOpen abs
9 8 mopni3 abs ∞Met S J x S π + r + r < π x ball abs r S
10 7 9 mpan2 abs ∞Met S J x S r + r < π x ball abs r S
11 6 10 mp3an1 S J x S r + r < π x ball abs r S
12 imass2 x ball abs r S exp x ball abs r exp S
13 imassrn exp x ball abs r ran exp
14 eff exp :
15 frn exp : ran exp
16 14 15 ax-mp ran exp
17 13 16 sstri exp x ball abs r
18 sseqin2 exp x ball abs r exp x ball abs r = exp x ball abs r
19 17 18 mpbi exp x ball abs r = exp x ball abs r
20 rpxr r + r *
21 blssm abs ∞Met x r * x ball abs r
22 6 21 mp3an1 x r * x ball abs r
23 20 22 sylan2 x r + x ball abs r
24 23 ad2antrr x r + r < π z x ball abs r
25 24 sselda x r + r < π z y x ball abs r y
26 simp-4l x r + r < π z y x ball abs r x
27 25 26 subcld x r + r < π z y x ball abs r y x
28 27 subid1d x r + r < π z y x ball abs r y - x - 0 = y x
29 28 fveq2d x r + r < π z y x ball abs r y - x - 0 = y x
30 0cn 0
31 eqid abs = abs
32 31 cnmetdval y x 0 y x abs 0 = y - x - 0
33 27 30 32 sylancl x r + r < π z y x ball abs r y x abs 0 = y - x - 0
34 31 cnmetdval y x y abs x = y x
35 25 26 34 syl2anc x r + r < π z y x ball abs r y abs x = y x
36 29 33 35 3eqtr4d x r + r < π z y x ball abs r y x abs 0 = y abs x
37 simpr x r + r < π z y x ball abs r y x ball abs r
38 6 a1i x r + r < π z y x ball abs r abs ∞Met
39 simpllr x r + r < π z r +
40 39 adantr x r + r < π z y x ball abs r r +
41 40 rpxrd x r + r < π z y x ball abs r r *
42 elbl3 abs ∞Met r * x y y x ball abs r y abs x < r
43 38 41 26 25 42 syl22anc x r + r < π z y x ball abs r y x ball abs r y abs x < r
44 37 43 mpbid x r + r < π z y x ball abs r y abs x < r
45 36 44 eqbrtrd x r + r < π z y x ball abs r y x abs 0 < r
46 0cnd x r + r < π z y x ball abs r 0
47 elbl3 abs ∞Met r * 0 y x y x 0 ball abs r y x abs 0 < r
48 38 41 46 27 47 syl22anc x r + r < π z y x ball abs r y x 0 ball abs r y x abs 0 < r
49 45 48 mpbird x r + r < π z y x ball abs r y x 0 ball abs r
50 efsub y x e y x = e y e x
51 25 26 50 syl2anc x r + r < π z y x ball abs r e y x = e y e x
52 fveqeq2 w = y x e w = e y e x e y x = e y e x
53 52 rspcev y x 0 ball abs r e y x = e y e x w 0 ball abs r e w = e y e x
54 49 51 53 syl2anc x r + r < π z y x ball abs r w 0 ball abs r e w = e y e x
55 oveq1 e y = z e y e x = z e x
56 55 eqeq2d e y = z e w = e y e x e w = z e x
57 56 rexbidv e y = z w 0 ball abs r e w = e y e x w 0 ball abs r e w = z e x
58 54 57 syl5ibcom x r + r < π z y x ball abs r e y = z w 0 ball abs r e w = z e x
59 58 rexlimdva x r + r < π z y x ball abs r e y = z w 0 ball abs r e w = z e x
60 eqcom e w = z e x z e x = e w
61 simplr x r + r < π z w 0 ball abs r z
62 simp-4l x r + r < π z w 0 ball abs r x
63 efcl x e x
64 62 63 syl x r + r < π z w 0 ball abs r e x
65 39 rpxrd x r + r < π z r *
66 blssm abs ∞Met 0 r * 0 ball abs r
67 6 30 65 66 mp3an12i x r + r < π z 0 ball abs r
68 67 sselda x r + r < π z w 0 ball abs r w
69 efcl w e w
70 68 69 syl x r + r < π z w 0 ball abs r e w
71 efne0 x e x 0
72 62 71 syl x r + r < π z w 0 ball abs r e x 0
73 61 64 70 72 divmuld x r + r < π z w 0 ball abs r z e x = e w e x e w = z
74 60 73 syl5bb x r + r < π z w 0 ball abs r e w = z e x e x e w = z
75 62 68 pncan2d x r + r < π z w 0 ball abs r x + w - x = w
76 68 subid1d x r + r < π z w 0 ball abs r w 0 = w
77 75 76 eqtr4d x r + r < π z w 0 ball abs r x + w - x = w 0
78 77 fveq2d x r + r < π z w 0 ball abs r x + w - x = w 0
79 62 68 addcld x r + r < π z w 0 ball abs r x + w
80 31 cnmetdval x + w x x + w abs x = x + w - x
81 79 62 80 syl2anc x r + r < π z w 0 ball abs r x + w abs x = x + w - x
82 31 cnmetdval w 0 w abs 0 = w 0
83 68 30 82 sylancl x r + r < π z w 0 ball abs r w abs 0 = w 0
84 78 81 83 3eqtr4d x r + r < π z w 0 ball abs r x + w abs x = w abs 0
85 simpr x r + r < π z w 0 ball abs r w 0 ball abs r
86 6 a1i x r + r < π z w 0 ball abs r abs ∞Met
87 39 adantr x r + r < π z w 0 ball abs r r +
88 87 rpxrd x r + r < π z w 0 ball abs r r *
89 0cnd x r + r < π z w 0 ball abs r 0
90 elbl3 abs ∞Met r * 0 w w 0 ball abs r w abs 0 < r
91 86 88 89 68 90 syl22anc x r + r < π z w 0 ball abs r w 0 ball abs r w abs 0 < r
92 85 91 mpbid x r + r < π z w 0 ball abs r w abs 0 < r
93 84 92 eqbrtrd x r + r < π z w 0 ball abs r x + w abs x < r
94 elbl3 abs ∞Met r * x x + w x + w x ball abs r x + w abs x < r
95 86 88 62 79 94 syl22anc x r + r < π z w 0 ball abs r x + w x ball abs r x + w abs x < r
96 93 95 mpbird x r + r < π z w 0 ball abs r x + w x ball abs r
97 efadd x w e x + w = e x e w
98 62 68 97 syl2anc x r + r < π z w 0 ball abs r e x + w = e x e w
99 fveqeq2 y = x + w e y = e x e w e x + w = e x e w
100 99 rspcev x + w x ball abs r e x + w = e x e w y x ball abs r e y = e x e w
101 96 98 100 syl2anc x r + r < π z w 0 ball abs r y x ball abs r e y = e x e w
102 eqeq2 e x e w = z e y = e x e w e y = z
103 102 rexbidv e x e w = z y x ball abs r e y = e x e w y x ball abs r e y = z
104 101 103 syl5ibcom x r + r < π z w 0 ball abs r e x e w = z y x ball abs r e y = z
105 74 104 sylbid x r + r < π z w 0 ball abs r e w = z e x y x ball abs r e y = z
106 105 rexlimdva x r + r < π z w 0 ball abs r e w = z e x y x ball abs r e y = z
107 59 106 impbid x r + r < π z y x ball abs r e y = z w 0 ball abs r e w = z e x
108 ffn exp : exp Fn
109 14 108 ax-mp exp Fn
110 fvelimab exp Fn x ball abs r z exp x ball abs r y x ball abs r e y = z
111 109 24 110 sylancr x r + r < π z z exp x ball abs r y x ball abs r e y = z
112 fvelimab exp Fn 0 ball abs r z e x exp 0 ball abs r w 0 ball abs r e w = z e x
113 109 67 112 sylancr x r + r < π z z e x exp 0 ball abs r w 0 ball abs r e w = z e x
114 107 111 113 3bitr4d x r + r < π z z exp x ball abs r z e x exp 0 ball abs r
115 114 rabbi2dva x r + r < π exp x ball abs r = z | z e x exp 0 ball abs r
116 19 115 eqtr3id x r + r < π exp x ball abs r = z | z e x exp 0 ball abs r
117 eqid z z e x = z z e x
118 117 mptpreima z z e x -1 exp 0 ball abs r = z | z e x exp 0 ball abs r
119 116 118 eqtr4di x r + r < π exp x ball abs r = z z e x -1 exp 0 ball abs r
120 63 ad2antrr x r + r < π e x
121 71 ad2antrr x r + r < π e x 0
122 117 divccncf e x e x 0 z z e x : cn
123 120 121 122 syl2anc x r + r < π z z e x : cn
124 1 cncfcn1 cn = J Cn J
125 123 124 eleqtrdi x r + r < π z z e x J Cn J
126 1 efopnlem2 r + r < π exp 0 ball abs r J
127 126 adantll x r + r < π exp 0 ball abs r J
128 cnima z z e x J Cn J exp 0 ball abs r J z z e x -1 exp 0 ball abs r J
129 125 127 128 syl2anc x r + r < π z z e x -1 exp 0 ball abs r J
130 119 129 eqeltrd x r + r < π exp x ball abs r J
131 blcntr abs ∞Met x r + x x ball abs r
132 6 131 mp3an1 x r + x x ball abs r
133 ffun exp : Fun exp
134 14 133 ax-mp Fun exp
135 14 fdmi dom exp =
136 23 135 sseqtrrdi x r + x ball abs r dom exp
137 funfvima2 Fun exp x ball abs r dom exp x x ball abs r e x exp x ball abs r
138 134 136 137 sylancr x r + x x ball abs r e x exp x ball abs r
139 132 138 mpd x r + e x exp x ball abs r
140 139 adantr x r + r < π e x exp x ball abs r
141 eleq2 y = exp x ball abs r e x y e x exp x ball abs r
142 sseq1 y = exp x ball abs r y exp S exp x ball abs r exp S
143 141 142 anbi12d y = exp x ball abs r e x y y exp S e x exp x ball abs r exp x ball abs r exp S
144 143 rspcev exp x ball abs r J e x exp x ball abs r exp x ball abs r exp S y J e x y y exp S
145 144 expr exp x ball abs r J e x exp x ball abs r exp x ball abs r exp S y J e x y y exp S
146 130 140 145 syl2anc x r + r < π exp x ball abs r exp S y J e x y y exp S
147 12 146 syl5 x r + r < π x ball abs r S y J e x y y exp S
148 147 expimpd x r + r < π x ball abs r S y J e x y y exp S
149 148 rexlimdva x r + r < π x ball abs r S y J e x y y exp S
150 5 11 149 sylc S J x S y J e x y y exp S
151 150 ralrimiva S J x S y J e x y y exp S
152 eleq1 z = e x z y e x y
153 152 anbi1d z = e x z y y exp S e x y y exp S
154 153 rexbidv z = e x y J z y y exp S y J e x y y exp S
155 154 ralima exp Fn S z exp S y J z y y exp S x S y J e x y y exp S
156 109 4 155 sylancr S J z exp S y J z y y exp S x S y J e x y y exp S
157 151 156 mpbird S J z exp S y J z y y exp S
158 1 cnfldtop J Top
159 eltop2 J Top exp S J z exp S y J z y y exp S
160 158 159 ax-mp exp S J z exp S y J z y y exp S
161 157 160 sylibr S J exp S J