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 _ x A
refsum2cnlem1.2 _ x F
refsum2cnlem1.3 _ x G
refsum2cnlem1.4 x φ
refsum2cnlem1.5 A = k 1 2 if k = 1 F G
refsum2cnlem1.6 K = topGen ran .
refsum2cnlem1.7 φ J TopOn X
refsum2cnlem1.8 φ F J Cn K
refsum2cnlem1.9 φ G J Cn K
Assertion refsum2cnlem1 φ x X F x + G x J Cn K

Proof

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