Metamath Proof Explorer

Theorem knoppcnlem10

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppcnlem10.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
knoppcnlem10.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppcnlem10.n 
|- ( ph -> N e. NN )
knoppcnlem10.1 
|- ( ph -> C e. RR )
knoppcnlem10.2 
|- ( ph -> M e. NN0 )
Assertion knoppcnlem10 
|- ( ph -> ( z e. RR |-> ( ( F ` z ) ` M ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )

Proof

Step Hyp Ref Expression
1 knoppcnlem10.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppcnlem10.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppcnlem10.n 
 |-  ( ph -> N e. NN )
4 knoppcnlem10.1 
 |-  ( ph -> C e. RR )
5 knoppcnlem10.2 
 |-  ( ph -> M e. NN0 )
6 simpr 
 |-  ( ( ph /\ z e. RR ) -> z e. RR )
7 5 adantr 
 |-  ( ( ph /\ z e. RR ) -> M e. NN0 )
8 2 6 7 knoppcnlem1 
 |-  ( ( ph /\ z e. RR ) -> ( ( F ` z ) ` M ) = ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. z ) ) ) )
9 8 mpteq2dva 
 |-  ( ph -> ( z e. RR |-> ( ( F ` z ) ` M ) ) = ( z e. RR |-> ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. z ) ) ) ) )
10 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
11 10 a1i 
 |-  ( ph -> ( topGen ` ran (,) ) e. ( TopOn ` RR ) )
12 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
13 12 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
14 13 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
15 4 recnd 
 |-  ( ph -> C e. CC )
16 15 5 expcld 
 |-  ( ph -> ( C ^ M ) e. CC )
17 11 14 16 cnmptc 
 |-  ( ph -> ( z e. RR |-> ( C ^ M ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
18 2re 
 |-  2 e. RR
19 18 a1i 
 |-  ( ph -> 2 e. RR )
20 nnre 
 |-  ( N e. NN -> N e. RR )
21 3 20 syl 
 |-  ( ph -> N e. RR )
22 19 21 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
23 22 5 reexpcld 
 |-  ( ph -> ( ( 2 x. N ) ^ M ) e. RR )
24 23 recnd 
 |-  ( ph -> ( ( 2 x. N ) ^ M ) e. CC )
25 11 14 24 cnmptc 
 |-  ( ph -> ( z e. RR |-> ( ( 2 x. N ) ^ M ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
26 12 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
27 26 oveq2i 
 |-  ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) = ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t RR ) )
28 13 topontopi 
 |-  ( TopOpen ` CCfld ) e. Top
29 cnrest2r 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) C_ ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
30 28 29 ax-mp 
 |-  ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) C_ ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) )
31 27 30 eqsstri 
 |-  ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) C_ ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) )
32 11 cnmptid 
 |-  ( ph -> ( z e. RR |-> z ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
33 31 32 sselid 
 |-  ( ph -> ( z e. RR |-> z ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
34 12 mulcn 
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
35 34 a1i 
 |-  ( ph -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
36 11 25 33 35 cnmpt12f 
 |-  ( ph -> ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
37 23 adantr 
 |-  ( ( ph /\ z e. RR ) -> ( ( 2 x. N ) ^ M ) e. RR )
38 37 6 remulcld 
 |-  ( ( ph /\ z e. RR ) -> ( ( ( 2 x. N ) ^ M ) x. z ) e. RR )
39 38 fmpttd 
 |-  ( ph -> ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) : RR --> RR )
40 39 frnd 
 |-  ( ph -> ran ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) C_ RR )
41 ax-resscn 
 |-  RR C_ CC
42 41 a1i 
 |-  ( ph -> RR C_ CC )
43 14 40 42 3jca 
 |-  ( ph -> ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) C_ RR /\ RR C_ CC ) )
44 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) C_ RR /\ RR C_ CC ) -> ( ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) <-> ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
45 43 44 syl 
 |-  ( ph -> ( ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) <-> ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
46 36 45 mpbid 
 |-  ( ph -> ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
47 46 27 eleqtrrdi 
 |-  ( ph -> ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
48 ssid 
 |-  CC C_ CC
49 41 48 pm3.2i 
 |-  ( RR C_ CC /\ CC C_ CC )
50 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( RR -cn-> RR ) C_ ( RR -cn-> CC ) )
51 49 50 ax-mp 
 |-  ( RR -cn-> RR ) C_ ( RR -cn-> CC )
52 1 dnicn 
 |-  T e. ( RR -cn-> RR )
53 52 a1i 
 |-  ( ph -> T e. ( RR -cn-> RR ) )
54 51 53 sselid 
 |-  ( ph -> T e. ( RR -cn-> CC ) )
55 13 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
56 12 26 55 cncfcn 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( RR -cn-> CC ) = ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
57 49 56 ax-mp 
 |-  ( RR -cn-> CC ) = ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) )
58 54 57 eleqtrdi 
 |-  ( ph -> T e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
59 11 47 58 cnmpt11f 
 |-  ( ph -> ( z e. RR |-> ( T ` ( ( ( 2 x. N ) ^ M ) x. z ) ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
60 11 17 59 35 cnmpt12f 
 |-  ( ph -> ( z e. RR |-> ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. z ) ) ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
61 9 60 eqeltrd 
 |-  ( ph -> ( z e. RR |-> ( ( F ` z ) ` M ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )