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 ⊢ Ⅎ 𝑥 𝐴
refsum2cnlem1.2 ⊢ Ⅎ 𝑥 𝐹
refsum2cnlem1.3 ⊢ Ⅎ 𝑥 𝐺
refsum2cnlem1.4 ⊢ Ⅎ 𝑥 𝜑
refsum2cnlem1.5 ⊢ 𝐴 = ( 𝑘 ∈ { 1 , 2 } ↦ if ( 𝑘 = 1 , 𝐹 , 𝐺 ) )
refsum2cnlem1.6 ⊢ 𝐾 = ( topGen ‘ ran (,) )
refsum2cnlem1.7 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
refsum2cnlem1.8 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
refsum2cnlem1.9 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion refsum2cnlem1 ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

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