Proof of Theorem axcontlem1
Step | Hyp | Ref
| Expression |
1 | | axcontlem1.1 |
. 2
⊢ 𝐹 = {〈𝑥, 𝑡〉 ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} |
2 | | eleq1w 2815 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷)) |
3 | 2 | adantr 484 |
. . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → (𝑥 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷)) |
4 | | eleq1w 2815 |
. . . . . 6
⊢ (𝑡 = 𝑠 → (𝑡 ∈ (0[,)+∞) ↔ 𝑠 ∈
(0[,)+∞))) |
5 | 4 | adantl 485 |
. . . . 5
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → (𝑡 ∈ (0[,)+∞) ↔ 𝑠 ∈
(0[,)+∞))) |
6 | | fveq1 6673 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥‘𝑖) = (𝑦‘𝑖)) |
7 | | oveq2 7178 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → (1 − 𝑡) = (1 − 𝑠)) |
8 | 7 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝑡 = 𝑠 → ((1 − 𝑡) · (𝑍‘𝑖)) = ((1 − 𝑠) · (𝑍‘𝑖))) |
9 | | oveq1 7177 |
. . . . . . . . 9
⊢ (𝑡 = 𝑠 → (𝑡 · (𝑈‘𝑖)) = (𝑠 · (𝑈‘𝑖))) |
10 | 8, 9 | oveq12d 7188 |
. . . . . . . 8
⊢ (𝑡 = 𝑠 → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) |
11 | 6, 10 | eqeqan12d 2755 |
. . . . . . 7
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑦‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))) |
12 | 11 | ralbidv 3109 |
. . . . . 6
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))) |
13 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (𝑦‘𝑖) = (𝑦‘𝑗)) |
14 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (𝑍‘𝑖) = (𝑍‘𝑗)) |
15 | 14 | oveq2d 7186 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → ((1 − 𝑠) · (𝑍‘𝑖)) = ((1 − 𝑠) · (𝑍‘𝑗))) |
16 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (𝑈‘𝑖) = (𝑈‘𝑗)) |
17 | 16 | oveq2d 7186 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (𝑠 · (𝑈‘𝑖)) = (𝑠 · (𝑈‘𝑗))) |
18 | 15, 17 | oveq12d 7188 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗)))) |
19 | 13, 18 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑖 = 𝑗 → ((𝑦‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ (𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗))))) |
20 | 19 | cbvralvw 3349 |
. . . . . 6
⊢
(∀𝑖 ∈
(1...𝑁)(𝑦‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ∀𝑗 ∈ (1...𝑁)(𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗)))) |
21 | 12, 20 | bitrdi 290 |
. . . . 5
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑗 ∈ (1...𝑁)(𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗))))) |
22 | 5, 21 | anbi12d 634 |
. . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → ((𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ (𝑠 ∈ (0[,)+∞) ∧ ∀𝑗 ∈ (1...𝑁)(𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗)))))) |
23 | 3, 22 | anbi12d 634 |
. . 3
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → ((𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) ↔ (𝑦 ∈ 𝐷 ∧ (𝑠 ∈ (0[,)+∞) ∧ ∀𝑗 ∈ (1...𝑁)(𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗))))))) |
24 | 23 | cbvopabv 5102 |
. 2
⊢
{〈𝑥, 𝑡〉 ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} = {〈𝑦, 𝑠〉 ∣ (𝑦 ∈ 𝐷 ∧ (𝑠 ∈ (0[,)+∞) ∧ ∀𝑗 ∈ (1...𝑁)(𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗)))))} |
25 | 1, 24 | eqtri 2761 |
1
⊢ 𝐹 = {〈𝑦, 𝑠〉 ∣ (𝑦 ∈ 𝐷 ∧ (𝑠 ∈ (0[,)+∞) ∧ ∀𝑗 ∈ (1...𝑁)(𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗)))))} |