Metamath Proof Explorer

Theorem refsum2cnlem1

Description: This is the core Lemma for refsum2cn : the sum of two continuous real functions (from a common topological space) is continuous. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses refsum2cnlem1.1 
|- F/_ x A
refsum2cnlem1.2 
|- F/_ x F
refsum2cnlem1.3 
|- F/_ x G
refsum2cnlem1.4 
|- F/ x ph
refsum2cnlem1.5 
|- A = ( k e. { 1 , 2 } |-> if ( k = 1 , F , G ) )
refsum2cnlem1.6 
|- K = ( topGen ` ran (,) )
refsum2cnlem1.7 
|- ( ph -> J e. ( TopOn ` X ) )
refsum2cnlem1.8 
|- ( ph -> F e. ( J Cn K ) )
refsum2cnlem1.9 
|- ( ph -> G e. ( J Cn K ) )
Assertion refsum2cnlem1 
|- ( ph -> ( x e. X |-> ( ( F ` x ) + ( G ` x ) ) ) e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 refsum2cnlem1.1 
 |-  F/_ x A
2 refsum2cnlem1.2 
 |-  F/_ x F
3 refsum2cnlem1.3 
 |-  F/_ x G
4 refsum2cnlem1.4 
 |-  F/ x ph
5 refsum2cnlem1.5 
 |-  A = ( k e. { 1 , 2 } |-> if ( k = 1 , F , G ) )
6 refsum2cnlem1.6 
 |-  K = ( topGen ` ran (,) )
7 refsum2cnlem1.7 
 |-  ( ph -> J e. ( TopOn ` X ) )
8 refsum2cnlem1.8 
 |-  ( ph -> F e. ( J Cn K ) )
9 refsum2cnlem1.9 
 |-  ( ph -> G e. ( J Cn K ) )
10 nfmpt1 
 |-  F/_ k ( k e. { 1 , 2 } |-> if ( k = 1 , F , G ) )
11 5 10 nfcxfr 
 |-  F/_ k A
12 nfcv 
 |-  F/_ k 1
13 11 12 nffv 
 |-  F/_ k ( A ` 1 )
14 nfcv 
 |-  F/_ k x
15 13 14 nffv 
 |-  F/_ k ( ( A ` 1 ) ` x )
16 15 a1i 
 |-  ( ( ph /\ x e. X ) -> F/_ k ( ( A ` 1 ) ` x ) )
17 nfcv 
 |-  F/_ k 2
18 11 17 nffv 
 |-  F/_ k ( A ` 2 )
19 18 14 nffv 
 |-  F/_ k ( ( A ` 2 ) ` x )
20 19 a1i 
 |-  ( ( ph /\ x e. X ) -> F/_ k ( ( A ` 2 ) ` x ) )
21 1cnd 
 |-  ( ( ph /\ x e. X ) -> 1 e. CC )
22 2cnd 
 |-  ( ( ph /\ x e. X ) -> 2 e. CC )
23 1ex 
 |-  1 e. _V
24 23 prid1 
 |-  1 e. { 1 , 2 }
25 8 9 ifcld 
 |-  ( ph -> if ( 1 = 1 , F , G ) e. ( J Cn K ) )
26 eqeq1 
 |-  ( k = 1 -> ( k = 1 <-> 1 = 1 ) )
27 26 ifbid 
 |-  ( k = 1 -> if ( k = 1 , F , G ) = if ( 1 = 1 , F , G ) )
28 27 5 fvmptg 
 |-  ( ( 1 e. { 1 , 2 } /\ if ( 1 = 1 , F , G ) e. ( J Cn K ) ) -> ( A ` 1 ) = if ( 1 = 1 , F , G ) )
29 24 25 28 sylancr 
 |-  ( ph -> ( A ` 1 ) = if ( 1 = 1 , F , G ) )
30 eqid 
 |-  1 = 1
31 30 iftruei 
 |-  if ( 1 = 1 , F , G ) = F
32 29 31 eqtrdi 
 |-  ( ph -> ( A ` 1 ) = F )
33 32 adantr 
 |-  ( ( ph /\ x e. X ) -> ( A ` 1 ) = F )
34 33 fveq1d 
 |-  ( ( ph /\ x e. X ) -> ( ( A ` 1 ) ` x ) = ( F ` x ) )
35 eqid 
 |-  U. J = U. J
36 eqid 
 |-  U. K = U. K
37 35 36 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
38 8 37 syl 
 |-  ( ph -> F : U. J --> U. K )
39 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
40 7 39 syl 
 |-  ( ph -> X = U. J )
41 40 eqcomd 
 |-  ( ph -> U. J = X )
42 6 unieqi 
 |-  U. K = U. ( topGen ` ran (,) )
43 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
44 42 43 eqtr4i 
 |-  U. K = RR
45 44 a1i 
 |-  ( ph -> U. K = RR )
46 41 45 feq23d 
 |-  ( ph -> ( F : U. J --> U. K <-> F : X --> RR ) )
47 38 46 mpbid 
 |-  ( ph -> F : X --> RR )
48 47 anim1i 
 |-  ( ( ph /\ x e. X ) -> ( F : X --> RR /\ x e. X ) )
49 ffvelcdm 
 |-  ( ( F : X --> RR /\ x e. X ) -> ( F ` x ) e. RR )
50 recn 
 |-  ( ( F ` x ) e. RR -> ( F ` x ) e. CC )
51 48 49 50 3syl 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. CC )
52 34 51 eqeltrd 
 |-  ( ( ph /\ x e. X ) -> ( ( A ` 1 ) ` x ) e. CC )
53 2ex 
 |-  2 e. _V
54 53 prid2 
 |-  2 e. { 1 , 2 }
55 8 9 ifcld 
 |-  ( ph -> if ( 2 = 1 , F , G ) e. ( J Cn K ) )
56 eqeq1 
 |-  ( k = 2 -> ( k = 1 <-> 2 = 1 ) )
57 56 ifbid 
 |-  ( k = 2 -> if ( k = 1 , F , G ) = if ( 2 = 1 , F , G ) )
58 57 5 fvmptg 
 |-  ( ( 2 e. { 1 , 2 } /\ if ( 2 = 1 , F , G ) e. ( J Cn K ) ) -> ( A ` 2 ) = if ( 2 = 1 , F , G ) )
59 54 55 58 sylancr 
 |-  ( ph -> ( A ` 2 ) = if ( 2 = 1 , F , G ) )
60 1ne2 
 |-  1 =/= 2
61 60 nesymi 
 |-  -. 2 = 1
62 61 iffalsei 
 |-  if ( 2 = 1 , F , G ) = G
63 59 62 eqtrdi 
 |-  ( ph -> ( A ` 2 ) = G )
64 63 adantr 
 |-  ( ( ph /\ x e. X ) -> ( A ` 2 ) = G )
65 64 fveq1d 
 |-  ( ( ph /\ x e. X ) -> ( ( A ` 2 ) ` x ) = ( G ` x ) )
66 35 36 cnf 
 |-  ( G e. ( J Cn K ) -> G : U. J --> U. K )
67 9 66 syl 
 |-  ( ph -> G : U. J --> U. K )
68 41 45 feq23d 
 |-  ( ph -> ( G : U. J --> U. K <-> G : X --> RR ) )
69 67 68 mpbid 
 |-  ( ph -> G : X --> RR )
70 69 anim1i 
 |-  ( ( ph /\ x e. X ) -> ( G : X --> RR /\ x e. X ) )
71 ffvelcdm 
 |-  ( ( G : X --> RR /\ x e. X ) -> ( G ` x ) e. RR )
72 recn 
 |-  ( ( G ` x ) e. RR -> ( G ` x ) e. CC )
73 70 71 72 3syl 
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. CC )
74 65 73 eqeltrd 
 |-  ( ( ph /\ x e. X ) -> ( ( A ` 2 ) ` x ) e. CC )
75 60 a1i 
 |-  ( ( ph /\ x e. X ) -> 1 =/= 2 )
76 fveq2 
 |-  ( k = 1 -> ( A ` k ) = ( A ` 1 ) )
77 76 fveq1d 
 |-  ( k = 1 -> ( ( A ` k ) ` x ) = ( ( A ` 1 ) ` x ) )
78 77 adantl 
 |-  ( ( ( ph /\ x e. X ) /\ k = 1 ) -> ( ( A ` k ) ` x ) = ( ( A ` 1 ) ` x ) )
79 fveq2 
 |-  ( k = 2 -> ( A ` k ) = ( A ` 2 ) )
80 79 fveq1d 
 |-  ( k = 2 -> ( ( A ` k ) ` x ) = ( ( A ` 2 ) ` x ) )
81 80 adantl 
 |-  ( ( ( ph /\ x e. X ) /\ k = 2 ) -> ( ( A ` k ) ` x ) = ( ( A ` 2 ) ` x ) )
82 16 20 21 22 52 74 75 78 81 sumpair 
 |-  ( ( ph /\ x e. X ) -> sum_ k e. { 1 , 2 } ( ( A ` k ) ` x ) = ( ( ( A ` 1 ) ` x ) + ( ( A ` 2 ) ` x ) ) )
83 34 65 oveq12d 
 |-  ( ( ph /\ x e. X ) -> ( ( ( A ` 1 ) ` x ) + ( ( A ` 2 ) ` x ) ) = ( ( F ` x ) + ( G ` x ) ) )
84 82 83 eqtrd 
 |-  ( ( ph /\ x e. X ) -> sum_ k e. { 1 , 2 } ( ( A ` k ) ` x ) = ( ( F ` x ) + ( G ` x ) ) )
85 4 84 mpteq2da 
 |-  ( ph -> ( x e. X |-> sum_ k e. { 1 , 2 } ( ( A ` k ) ` x ) ) = ( x e. X |-> ( ( F ` x ) + ( G ` x ) ) ) )
86 prfi 
 |-  { 1 , 2 } e. Fin
87 86 a1i 
 |-  ( ph -> { 1 , 2 } e. Fin )
88 eqid 
 |-  X = X
89 88 ax-gen 
 |-  A. x X = X
90 nfcv 
 |-  F/_ x k
91 1 90 nffv 
 |-  F/_ x ( A ` k )
92 91 2 nfeq 
 |-  F/ x ( A ` k ) = F
93 fveq1 
 |-  ( ( A ` k ) = F -> ( ( A ` k ) ` x ) = ( F ` x ) )
94 93 a1d 
 |-  ( ( A ` k ) = F -> ( x e. X -> ( ( A ` k ) ` x ) = ( F ` x ) ) )
95 92 94 ralrimi 
 |-  ( ( A ` k ) = F -> A. x e. X ( ( A ` k ) ` x ) = ( F ` x ) )
96 mpteq12f 
 |-  ( ( A. x X = X /\ A. x e. X ( ( A ` k ) ` x ) = ( F ` x ) ) -> ( x e. X |-> ( ( A ` k ) ` x ) ) = ( x e. X |-> ( F ` x ) ) )
97 89 95 96 sylancr 
 |-  ( ( A ` k ) = F -> ( x e. X |-> ( ( A ` k ) ` x ) ) = ( x e. X |-> ( F ` x ) ) )
98 97 adantl 
 |-  ( ( ph /\ ( A ` k ) = F ) -> ( x e. X |-> ( ( A ` k ) ` x ) ) = ( x e. X |-> ( F ` x ) ) )
99 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
100 6 99 eqeltri 
 |-  K e. ( TopOn ` RR )
101 100 a1i 
 |-  ( ph -> K e. ( TopOn ` RR ) )
102 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` RR ) /\ F e. ( J Cn K ) ) -> F : X --> RR )
103 7 101 8 102 syl3anc 
 |-  ( ph -> F : X --> RR )
104 103 ffnd 
 |-  ( ph -> F Fn X )
105 2 dffn5f 
 |-  ( F Fn X <-> F = ( x e. X |-> ( F ` x ) ) )
106 104 105 sylib 
 |-  ( ph -> F = ( x e. X |-> ( F ` x ) ) )
107 106 adantr 
 |-  ( ( ph /\ ( A ` k ) = F ) -> F = ( x e. X |-> ( F ` x ) ) )
108 98 107 eqtr4d 
 |-  ( ( ph /\ ( A ` k ) = F ) -> ( x e. X |-> ( ( A ` k ) ` x ) ) = F )
109 8 adantr 
 |-  ( ( ph /\ ( A ` k ) = F ) -> F e. ( J Cn K ) )
110 108 109 eqeltrd 
 |-  ( ( ph /\ ( A ` k ) = F ) -> ( x e. X |-> ( ( A ` k ) ` x ) ) e. ( J Cn K ) )
111 110 adantlr 
 |-  ( ( ( ph /\ k e. { 1 , 2 } ) /\ ( A ` k ) = F ) -> ( x e. X |-> ( ( A ` k ) ` x ) ) e. ( J Cn K ) )
112 91 3 nfeq 
 |-  F/ x ( A ` k ) = G
113 fveq1 
 |-  ( ( A ` k ) = G -> ( ( A ` k ) ` x ) = ( G ` x ) )
114 113 a1d 
 |-  ( ( A ` k ) = G -> ( x e. X -> ( ( A ` k ) ` x ) = ( G ` x ) ) )
115 112 114 ralrimi 
 |-  ( ( A ` k ) = G -> A. x e. X ( ( A ` k ) ` x ) = ( G ` x ) )
116 mpteq12f 
 |-  ( ( A. x X = X /\ A. x e. X ( ( A ` k ) ` x ) = ( G ` x ) ) -> ( x e. X |-> ( ( A ` k ) ` x ) ) = ( x e. X |-> ( G ` x ) ) )
117 89 115 116 sylancr 
 |-  ( ( A ` k ) = G -> ( x e. X |-> ( ( A ` k ) ` x ) ) = ( x e. X |-> ( G ` x ) ) )
118 117 adantl 
 |-  ( ( ph /\ ( A ` k ) = G ) -> ( x e. X |-> ( ( A ` k ) ` x ) ) = ( x e. X |-> ( G ` x ) ) )
119 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` RR ) /\ G e. ( J Cn K ) ) -> G : X --> RR )
120 7 101 9 119 syl3anc 
 |-  ( ph -> G : X --> RR )
121 120 ffnd 
 |-  ( ph -> G Fn X )
122 3 dffn5f 
 |-  ( G Fn X <-> G = ( x e. X |-> ( G ` x ) ) )
123 121 122 sylib 
 |-  ( ph -> G = ( x e. X |-> ( G ` x ) ) )
124 123 adantr 
 |-  ( ( ph /\ ( A ` k ) = G ) -> G = ( x e. X |-> ( G ` x ) ) )
125 118 124 eqtr4d 
 |-  ( ( ph /\ ( A ` k ) = G ) -> ( x e. X |-> ( ( A ` k ) ` x ) ) = G )
126 9 adantr 
 |-  ( ( ph /\ ( A ` k ) = G ) -> G e. ( J Cn K ) )
127 125 126 eqeltrd 
 |-  ( ( ph /\ ( A ` k ) = G ) -> ( x e. X |-> ( ( A ` k ) ` x ) ) e. ( J Cn K ) )
128 127 adantlr 
 |-  ( ( ( ph /\ k e. { 1 , 2 } ) /\ ( A ` k ) = G ) -> ( x e. X |-> ( ( A ` k ) ` x ) ) e. ( J Cn K ) )
129 simpr 
 |-  ( ( ph /\ k e. { 1 , 2 } ) -> k e. { 1 , 2 } )
130 8 9 ifcld 
 |-  ( ph -> if ( k = 1 , F , G ) e. ( J Cn K ) )
131 130 adantr 
 |-  ( ( ph /\ k e. { 1 , 2 } ) -> if ( k = 1 , F , G ) e. ( J Cn K ) )
132 5 fvmpt2 
 |-  ( ( k e. { 1 , 2 } /\ if ( k = 1 , F , G ) e. ( J Cn K ) ) -> ( A ` k ) = if ( k = 1 , F , G ) )
133 129 131 132 syl2anc 
 |-  ( ( ph /\ k e. { 1 , 2 } ) -> ( A ` k ) = if ( k = 1 , F , G ) )
134 iftrue 
 |-  ( k = 1 -> if ( k = 1 , F , G ) = F )
135 133 134 sylan9eq 
 |-  ( ( ( ph /\ k e. { 1 , 2 } ) /\ k = 1 ) -> ( A ` k ) = F )
136 135 orcd 
 |-  ( ( ( ph /\ k e. { 1 , 2 } ) /\ k = 1 ) -> ( ( A ` k ) = F \/ ( A ` k ) = G ) )
137 133 adantr 
 |-  ( ( ( ph /\ k e. { 1 , 2 } ) /\ k = 2 ) -> ( A ` k ) = if ( k = 1 , F , G ) )
138 neeq2 
 |-  ( k = 2 -> ( 1 =/= k <-> 1 =/= 2 ) )
139 60 138 mpbiri 
 |-  ( k = 2 -> 1 =/= k )
140 139 necomd 
 |-  ( k = 2 -> k =/= 1 )
141 140 neneqd 
 |-  ( k = 2 -> -. k = 1 )
142 141 adantl 
 |-  ( ( ( ph /\ k e. { 1 , 2 } ) /\ k = 2 ) -> -. k = 1 )
143 142 iffalsed 
 |-  ( ( ( ph /\ k e. { 1 , 2 } ) /\ k = 2 ) -> if ( k = 1 , F , G ) = G )
144 137 143 eqtrd 
 |-  ( ( ( ph /\ k e. { 1 , 2 } ) /\ k = 2 ) -> ( A ` k ) = G )
145 144 olcd 
 |-  ( ( ( ph /\ k e. { 1 , 2 } ) /\ k = 2 ) -> ( ( A ` k ) = F \/ ( A ` k ) = G ) )
146 elpri 
 |-  ( k e. { 1 , 2 } -> ( k = 1 \/ k = 2 ) )
147 146 adantl 
 |-  ( ( ph /\ k e. { 1 , 2 } ) -> ( k = 1 \/ k = 2 ) )
148 136 145 147 mpjaodan 
 |-  ( ( ph /\ k e. { 1 , 2 } ) -> ( ( A ` k ) = F \/ ( A ` k ) = G ) )
149 111 128 148 mpjaodan 
 |-  ( ( ph /\ k e. { 1 , 2 } ) -> ( x e. X |-> ( ( A ` k ) ` x ) ) e. ( J Cn K ) )
150 4 6 7 87 149 refsumcn 
 |-  ( ph -> ( x e. X |-> sum_ k e. { 1 , 2 } ( ( A ` k ) ` x ) ) e. ( J Cn K ) )
151 85 150 eqeltrrd 
 |-  ( ph -> ( x e. X |-> ( ( F ` x ) + ( G ` x ) ) ) e. ( J Cn K ) )