Proof of Theorem refsum2cnlem1
Step | Hyp | Ref
| Expression |
1 | | refsum2cnlem1.4 |
. . 3
⊢
Ⅎ𝑥𝜑 |
2 | | refsum2cnlem1.5 |
. . . . . . . . 9
⊢ 𝐴 = (𝑘 ∈ {1, 2} ↦ if(𝑘 = 1, 𝐹, 𝐺)) |
3 | | nfmpt1 4675 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝑘 ∈ {1, 2} ↦ if(𝑘 = 1, 𝐹, 𝐺)) |
4 | 2, 3 | nfcxfr 2749 |
. . . . . . . 8
⊢
Ⅎ𝑘𝐴 |
5 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑘1 |
6 | 4, 5 | nffv 6110 |
. . . . . . 7
⊢
Ⅎ𝑘(𝐴‘1) |
7 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑘𝑥 |
8 | 6, 7 | nffv 6110 |
. . . . . 6
⊢
Ⅎ𝑘((𝐴‘1)‘𝑥) |
9 | 8 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Ⅎ𝑘((𝐴‘1)‘𝑥)) |
10 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑘2 |
11 | 4, 10 | nffv 6110 |
. . . . . . 7
⊢
Ⅎ𝑘(𝐴‘2) |
12 | 11, 7 | nffv 6110 |
. . . . . 6
⊢
Ⅎ𝑘((𝐴‘2)‘𝑥) |
13 | 12 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Ⅎ𝑘((𝐴‘2)‘𝑥)) |
14 | | 1cnd 9935 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 1 ∈ ℂ) |
15 | | 2cnd 10970 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 2 ∈ ℂ) |
16 | | 1ex 9914 |
. . . . . . . . . . 11
⊢ 1 ∈
V |
17 | 16 | prid1 4241 |
. . . . . . . . . 10
⊢ 1 ∈
{1, 2} |
18 | | refsum2cnlem1.8 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
19 | | refsum2cnlem1.9 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) |
20 | 18, 19 | ifcld 4081 |
. . . . . . . . . 10
⊢ (𝜑 → if(1 = 1, 𝐹, 𝐺) ∈ (𝐽 Cn 𝐾)) |
21 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → (𝑘 = 1 ↔ 1 = 1)) |
22 | 21 | ifbid 4058 |
. . . . . . . . . . 11
⊢ (𝑘 = 1 → if(𝑘 = 1, 𝐹, 𝐺) = if(1 = 1, 𝐹, 𝐺)) |
23 | 22, 2 | fvmptg 6189 |
. . . . . . . . . 10
⊢ ((1
∈ {1, 2} ∧ if(1 = 1, 𝐹, 𝐺) ∈ (𝐽 Cn 𝐾)) → (𝐴‘1) = if(1 = 1, 𝐹, 𝐺)) |
24 | 17, 20, 23 | sylancr 694 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴‘1) = if(1 = 1, 𝐹, 𝐺)) |
25 | | eqid 2610 |
. . . . . . . . . 10
⊢ 1 =
1 |
26 | 25 | iftruei 4043 |
. . . . . . . . 9
⊢ if(1 = 1,
𝐹, 𝐺) = 𝐹 |
27 | 24, 26 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘1) = 𝐹) |
28 | 27 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐴‘1) = 𝐹) |
29 | 28 | fveq1d 6105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐴‘1)‘𝑥) = (𝐹‘𝑥)) |
30 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ 𝐽 =
∪ 𝐽 |
31 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ 𝐾 =
∪ 𝐾 |
32 | 30, 31 | cnf 20860 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
33 | 18, 32 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:∪ 𝐽⟶∪ 𝐾) |
34 | | refsum2cnlem1.7 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
35 | | toponuni 20542 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
37 | 36 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝐽 =
𝑋) |
38 | | refsum2cnlem1.6 |
. . . . . . . . . . . . 13
⊢ 𝐾 = (topGen‘ran
(,)) |
39 | 38 | unieqi 4381 |
. . . . . . . . . . . 12
⊢ ∪ 𝐾 =
∪ (topGen‘ran (,)) |
40 | | uniretop 22376 |
. . . . . . . . . . . 12
⊢ ℝ =
∪ (topGen‘ran (,)) |
41 | 39, 40 | eqtr4i 2635 |
. . . . . . . . . . 11
⊢ ∪ 𝐾 =
ℝ |
42 | 41 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝐾 =
ℝ) |
43 | 37, 42 | feq23d 5953 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹:∪ 𝐽⟶∪ 𝐾
↔ 𝐹:𝑋⟶ℝ)) |
44 | 33, 43 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
45 | 44 | anim1i 590 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹:𝑋⟶ℝ ∧ 𝑥 ∈ 𝑋)) |
46 | | ffvelrn 6265 |
. . . . . . 7
⊢ ((𝐹:𝑋⟶ℝ ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ℝ) |
47 | | recn 9905 |
. . . . . . 7
⊢ ((𝐹‘𝑥) ∈ ℝ → (𝐹‘𝑥) ∈ ℂ) |
48 | 45, 46, 47 | 3syl 18 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ℂ) |
49 | 29, 48 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐴‘1)‘𝑥) ∈ ℂ) |
50 | | 2ex 10969 |
. . . . . . . . . . 11
⊢ 2 ∈
V |
51 | 50 | prid2 4242 |
. . . . . . . . . 10
⊢ 2 ∈
{1, 2} |
52 | 18, 19 | ifcld 4081 |
. . . . . . . . . 10
⊢ (𝜑 → if(2 = 1, 𝐹, 𝐺) ∈ (𝐽 Cn 𝐾)) |
53 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑘 = 2 → (𝑘 = 1 ↔ 2 = 1)) |
54 | 53 | ifbid 4058 |
. . . . . . . . . . 11
⊢ (𝑘 = 2 → if(𝑘 = 1, 𝐹, 𝐺) = if(2 = 1, 𝐹, 𝐺)) |
55 | 54, 2 | fvmptg 6189 |
. . . . . . . . . 10
⊢ ((2
∈ {1, 2} ∧ if(2 = 1, 𝐹, 𝐺) ∈ (𝐽 Cn 𝐾)) → (𝐴‘2) = if(2 = 1, 𝐹, 𝐺)) |
56 | 51, 52, 55 | sylancr 694 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴‘2) = if(2 = 1, 𝐹, 𝐺)) |
57 | | 1ne2 11117 |
. . . . . . . . . . 11
⊢ 1 ≠
2 |
58 | 57 | nesymi 2839 |
. . . . . . . . . 10
⊢ ¬ 2
= 1 |
59 | 58 | iffalsei 4046 |
. . . . . . . . 9
⊢ if(2 = 1,
𝐹, 𝐺) = 𝐺 |
60 | 56, 59 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘2) = 𝐺) |
61 | 60 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐴‘2) = 𝐺) |
62 | 61 | fveq1d 6105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐴‘2)‘𝑥) = (𝐺‘𝑥)) |
63 | 30, 31 | cnf 20860 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (𝐽 Cn 𝐾) → 𝐺:∪ 𝐽⟶∪ 𝐾) |
64 | 19, 63 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:∪ 𝐽⟶∪ 𝐾) |
65 | 37, 42 | feq23d 5953 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺:∪ 𝐽⟶∪ 𝐾
↔ 𝐺:𝑋⟶ℝ)) |
66 | 64, 65 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:𝑋⟶ℝ) |
67 | 66 | anim1i 590 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺:𝑋⟶ℝ ∧ 𝑥 ∈ 𝑋)) |
68 | | ffvelrn 6265 |
. . . . . . 7
⊢ ((𝐺:𝑋⟶ℝ ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈ ℝ) |
69 | | recn 9905 |
. . . . . . 7
⊢ ((𝐺‘𝑥) ∈ ℝ → (𝐺‘𝑥) ∈ ℂ) |
70 | 67, 68, 69 | 3syl 18 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈ ℂ) |
71 | 62, 70 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐴‘2)‘𝑥) ∈ ℂ) |
72 | 57 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 1 ≠ 2) |
73 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 1 → (𝐴‘𝑘) = (𝐴‘1)) |
74 | 73 | fveq1d 6105 |
. . . . . 6
⊢ (𝑘 = 1 → ((𝐴‘𝑘)‘𝑥) = ((𝐴‘1)‘𝑥)) |
75 | 74 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 = 1) → ((𝐴‘𝑘)‘𝑥) = ((𝐴‘1)‘𝑥)) |
76 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 2 → (𝐴‘𝑘) = (𝐴‘2)) |
77 | 76 | fveq1d 6105 |
. . . . . 6
⊢ (𝑘 = 2 → ((𝐴‘𝑘)‘𝑥) = ((𝐴‘2)‘𝑥)) |
78 | 77 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 = 2) → ((𝐴‘𝑘)‘𝑥) = ((𝐴‘2)‘𝑥)) |
79 | 9, 13, 14, 15, 49, 71, 72, 75, 78 | sumpair 38217 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Σ𝑘 ∈ {1, 2} ((𝐴‘𝑘)‘𝑥) = (((𝐴‘1)‘𝑥) + ((𝐴‘2)‘𝑥))) |
80 | 29, 62 | oveq12d 6567 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝐴‘1)‘𝑥) + ((𝐴‘2)‘𝑥)) = ((𝐹‘𝑥) + (𝐺‘𝑥))) |
81 | 79, 80 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Σ𝑘 ∈ {1, 2} ((𝐴‘𝑘)‘𝑥) = ((𝐹‘𝑥) + (𝐺‘𝑥))) |
82 | 1, 81 | mpteq2da 4671 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ {1, 2} ((𝐴‘𝑘)‘𝑥)) = (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) + (𝐺‘𝑥)))) |
83 | | prfi 8120 |
. . . 4
⊢ {1, 2}
∈ Fin |
84 | 83 | a1i 11 |
. . 3
⊢ (𝜑 → {1, 2} ∈
Fin) |
85 | | eqid 2610 |
. . . . . . . . . 10
⊢ 𝑋 = 𝑋 |
86 | 85 | ax-gen 1713 |
. . . . . . . . 9
⊢
∀𝑥 𝑋 = 𝑋 |
87 | | refsum2cnlem1.1 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝐴 |
88 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑘 |
89 | 87, 88 | nffv 6110 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝐴‘𝑘) |
90 | | refsum2cnlem1.2 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐹 |
91 | 89, 90 | nfeq 2762 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝐴‘𝑘) = 𝐹 |
92 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ ((𝐴‘𝑘) = 𝐹 → ((𝐴‘𝑘)‘𝑥) = (𝐹‘𝑥)) |
93 | 92 | a1d 25 |
. . . . . . . . . 10
⊢ ((𝐴‘𝑘) = 𝐹 → (𝑥 ∈ 𝑋 → ((𝐴‘𝑘)‘𝑥) = (𝐹‘𝑥))) |
94 | 91, 93 | ralrimi 2940 |
. . . . . . . . 9
⊢ ((𝐴‘𝑘) = 𝐹 → ∀𝑥 ∈ 𝑋 ((𝐴‘𝑘)‘𝑥) = (𝐹‘𝑥)) |
95 | | mpteq12f 4661 |
. . . . . . . . 9
⊢
((∀𝑥 𝑋 = 𝑋 ∧ ∀𝑥 ∈ 𝑋 ((𝐴‘𝑘)‘𝑥) = (𝐹‘𝑥)) → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
96 | 86, 94, 95 | sylancr 694 |
. . . . . . . 8
⊢ ((𝐴‘𝑘) = 𝐹 → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
97 | 96 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴‘𝑘) = 𝐹) → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
98 | | retopon 22377 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
99 | 38, 98 | eqeltri 2684 |
. . . . . . . . . . . 12
⊢ 𝐾 ∈
(TopOn‘ℝ) |
100 | 99 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈
(TopOn‘ℝ)) |
101 | | cnf2 20863 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘ℝ) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶ℝ) |
102 | 34, 100, 18, 101 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
103 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:𝑋⟶ℝ → 𝐹 Fn 𝑋) |
104 | 102, 103 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝑋) |
105 | 90 | dffn5f 6162 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑋 ↔ 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
106 | 104, 105 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
107 | 106 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴‘𝑘) = 𝐹) → 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
108 | 97, 107 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴‘𝑘) = 𝐹) → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) = 𝐹) |
109 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴‘𝑘) = 𝐹) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
110 | 108, 109 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴‘𝑘) = 𝐹) → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) ∈ (𝐽 Cn 𝐾)) |
111 | 110 | adantlr 747 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ {1, 2}) ∧ (𝐴‘𝑘) = 𝐹) → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) ∈ (𝐽 Cn 𝐾)) |
112 | | refsum2cnlem1.3 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐺 |
113 | 89, 112 | nfeq 2762 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝐴‘𝑘) = 𝐺 |
114 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ ((𝐴‘𝑘) = 𝐺 → ((𝐴‘𝑘)‘𝑥) = (𝐺‘𝑥)) |
115 | 114 | a1d 25 |
. . . . . . . . . 10
⊢ ((𝐴‘𝑘) = 𝐺 → (𝑥 ∈ 𝑋 → ((𝐴‘𝑘)‘𝑥) = (𝐺‘𝑥))) |
116 | 113, 115 | ralrimi 2940 |
. . . . . . . . 9
⊢ ((𝐴‘𝑘) = 𝐺 → ∀𝑥 ∈ 𝑋 ((𝐴‘𝑘)‘𝑥) = (𝐺‘𝑥)) |
117 | | mpteq12f 4661 |
. . . . . . . . 9
⊢
((∀𝑥 𝑋 = 𝑋 ∧ ∀𝑥 ∈ 𝑋 ((𝐴‘𝑘)‘𝑥) = (𝐺‘𝑥)) → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
118 | 86, 116, 117 | sylancr 694 |
. . . . . . . 8
⊢ ((𝐴‘𝑘) = 𝐺 → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
119 | 118 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴‘𝑘) = 𝐺) → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
120 | | cnf2 20863 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘ℝ) ∧ 𝐺 ∈ (𝐽 Cn 𝐾)) → 𝐺:𝑋⟶ℝ) |
121 | 34, 100, 19, 120 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:𝑋⟶ℝ) |
122 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐺:𝑋⟶ℝ → 𝐺 Fn 𝑋) |
123 | 121, 122 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn 𝑋) |
124 | 112 | dffn5f 6162 |
. . . . . . . . 9
⊢ (𝐺 Fn 𝑋 ↔ 𝐺 = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
125 | 123, 124 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
126 | 125 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴‘𝑘) = 𝐺) → 𝐺 = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
127 | 119, 126 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴‘𝑘) = 𝐺) → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) = 𝐺) |
128 | 19 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴‘𝑘) = 𝐺) → 𝐺 ∈ (𝐽 Cn 𝐾)) |
129 | 127, 128 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴‘𝑘) = 𝐺) → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) ∈ (𝐽 Cn 𝐾)) |
130 | 129 | adantlr 747 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ {1, 2}) ∧ (𝐴‘𝑘) = 𝐺) → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) ∈ (𝐽 Cn 𝐾)) |
131 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {1, 2}) → 𝑘 ∈ {1, 2}) |
132 | 18, 19 | ifcld 4081 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑘 = 1, 𝐹, 𝐺) ∈ (𝐽 Cn 𝐾)) |
133 | 132 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {1, 2}) → if(𝑘 = 1, 𝐹, 𝐺) ∈ (𝐽 Cn 𝐾)) |
134 | 2 | fvmpt2 6200 |
. . . . . . . 8
⊢ ((𝑘 ∈ {1, 2} ∧ if(𝑘 = 1, 𝐹, 𝐺) ∈ (𝐽 Cn 𝐾)) → (𝐴‘𝑘) = if(𝑘 = 1, 𝐹, 𝐺)) |
135 | 131, 133,
134 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {1, 2}) → (𝐴‘𝑘) = if(𝑘 = 1, 𝐹, 𝐺)) |
136 | | iftrue 4042 |
. . . . . . 7
⊢ (𝑘 = 1 → if(𝑘 = 1, 𝐹, 𝐺) = 𝐹) |
137 | 135, 136 | sylan9eq 2664 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ {1, 2}) ∧ 𝑘 = 1) → (𝐴‘𝑘) = 𝐹) |
138 | 137 | orcd 406 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ {1, 2}) ∧ 𝑘 = 1) → ((𝐴‘𝑘) = 𝐹 ∨ (𝐴‘𝑘) = 𝐺)) |
139 | 135 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ {1, 2}) ∧ 𝑘 = 2) → (𝐴‘𝑘) = if(𝑘 = 1, 𝐹, 𝐺)) |
140 | | neeq2 2845 |
. . . . . . . . . . . 12
⊢ (𝑘 = 2 → (1 ≠ 𝑘 ↔ 1 ≠
2)) |
141 | 57, 140 | mpbiri 247 |
. . . . . . . . . . 11
⊢ (𝑘 = 2 → 1 ≠ 𝑘) |
142 | 141 | necomd 2837 |
. . . . . . . . . 10
⊢ (𝑘 = 2 → 𝑘 ≠ 1) |
143 | 142 | neneqd 2787 |
. . . . . . . . 9
⊢ (𝑘 = 2 → ¬ 𝑘 = 1) |
144 | 143 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ {1, 2}) ∧ 𝑘 = 2) → ¬ 𝑘 = 1) |
145 | 144 | iffalsed 4047 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ {1, 2}) ∧ 𝑘 = 2) → if(𝑘 = 1, 𝐹, 𝐺) = 𝐺) |
146 | 139, 145 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ {1, 2}) ∧ 𝑘 = 2) → (𝐴‘𝑘) = 𝐺) |
147 | 146 | olcd 407 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ {1, 2}) ∧ 𝑘 = 2) → ((𝐴‘𝑘) = 𝐹 ∨ (𝐴‘𝑘) = 𝐺)) |
148 | | elpri 4145 |
. . . . . 6
⊢ (𝑘 ∈ {1, 2} → (𝑘 = 1 ∨ 𝑘 = 2)) |
149 | 148 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {1, 2}) → (𝑘 = 1 ∨ 𝑘 = 2)) |
150 | 138, 147,
149 | mpjaodan 823 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {1, 2}) → ((𝐴‘𝑘) = 𝐹 ∨ (𝐴‘𝑘) = 𝐺)) |
151 | 111, 130,
150 | mpjaodan 823 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ {1, 2}) → (𝑥 ∈ 𝑋 ↦ ((𝐴‘𝑘)‘𝑥)) ∈ (𝐽 Cn 𝐾)) |
152 | 1, 38, 34, 84, 151 | refsumcn 38212 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ {1, 2} ((𝐴‘𝑘)‘𝑥)) ∈ (𝐽 Cn 𝐾)) |
153 | 82, 152 | eqeltrrd 2689 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ (𝐽 Cn 𝐾)) |