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	$⊢ \underline{Ⅎ} x A$
	refsum2cnlem1.2	$⊢ \underline{Ⅎ} x F$
	refsum2cnlem1.3	$⊢ \underline{Ⅎ} x G$
	refsum2cnlem1.4	$⊢ Ⅎ x φ$
	refsum2cnlem1.5	$⊢ A = (k \in \{1, 2\} ⟼ if (k = 1, F, G))$
	refsum2cnlem1.6	$⊢ K = topGen (ran (.))$
	refsum2cnlem1.7	$⊢ φ \to J \in TopOn (X)$
	refsum2cnlem1.8	$⊢ φ \to F \in (J Cn K)$
	refsum2cnlem1.9	$⊢ φ \to G \in (J Cn K)$
Assertion	refsum2cnlem1	$⊢ φ \to (x \in X ⟼ F (x) + G (x)) \in (J Cn K)$

Proof

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

Metamath Proof Explorer

Theorem refsum2cnlem1

Proof