Proof of Theorem axcontlem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | axcontlem1.1 | . 2
⊢ 𝐹 = {〈𝑥, 𝑡〉 ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} | 
| 2 |  | eleq1w 2823 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷)) | 
| 3 | 2 | adantr 480 | . . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → (𝑥 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷)) | 
| 4 |  | eleq1w 2823 | . . . . . 6
⊢ (𝑡 = 𝑠 → (𝑡 ∈ (0[,)+∞) ↔ 𝑠 ∈
(0[,)+∞))) | 
| 5 | 4 | adantl 481 | . . . . 5
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → (𝑡 ∈ (0[,)+∞) ↔ 𝑠 ∈
(0[,)+∞))) | 
| 6 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥‘𝑖) = (𝑦‘𝑖)) | 
| 7 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑡 = 𝑠 → (1 − 𝑡) = (1 − 𝑠)) | 
| 8 | 7 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝑡 = 𝑠 → ((1 − 𝑡) · (𝑍‘𝑖)) = ((1 − 𝑠) · (𝑍‘𝑖))) | 
| 9 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑡 = 𝑠 → (𝑡 · (𝑈‘𝑖)) = (𝑠 · (𝑈‘𝑖))) | 
| 10 | 8, 9 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑡 = 𝑠 → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) | 
| 11 | 6, 10 | eqeqan12d 2750 | . . . . . . 7
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑦‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))) | 
| 12 | 11 | ralbidv 3177 | . . . . . 6
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))) | 
| 13 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑖 = 𝑗 → (𝑦‘𝑖) = (𝑦‘𝑗)) | 
| 14 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (𝑍‘𝑖) = (𝑍‘𝑗)) | 
| 15 | 14 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑖 = 𝑗 → ((1 − 𝑠) · (𝑍‘𝑖)) = ((1 − 𝑠) · (𝑍‘𝑗))) | 
| 16 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (𝑈‘𝑖) = (𝑈‘𝑗)) | 
| 17 | 16 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑖 = 𝑗 → (𝑠 · (𝑈‘𝑖)) = (𝑠 · (𝑈‘𝑗))) | 
| 18 | 15, 17 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑖 = 𝑗 → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗)))) | 
| 19 | 13, 18 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑖 = 𝑗 → ((𝑦‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ (𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗))))) | 
| 20 | 19 | cbvralvw 3236 | . . . . . 6
⊢
(∀𝑖 ∈
(1...𝑁)(𝑦‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ∀𝑗 ∈ (1...𝑁)(𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗)))) | 
| 21 | 12, 20 | bitrdi 287 | . . . . 5
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑗 ∈ (1...𝑁)(𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗))))) | 
| 22 | 5, 21 | anbi12d 632 | . . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → ((𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ (𝑠 ∈ (0[,)+∞) ∧ ∀𝑗 ∈ (1...𝑁)(𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗)))))) | 
| 23 | 3, 22 | anbi12d 632 | . . 3
⊢ ((𝑥 = 𝑦 ∧ 𝑡 = 𝑠) → ((𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) ↔ (𝑦 ∈ 𝐷 ∧ (𝑠 ∈ (0[,)+∞) ∧ ∀𝑗 ∈ (1...𝑁)(𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗))))))) | 
| 24 | 23 | cbvopabv 5215 | . 2
⊢
{〈𝑥, 𝑡〉 ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} = {〈𝑦, 𝑠〉 ∣ (𝑦 ∈ 𝐷 ∧ (𝑠 ∈ (0[,)+∞) ∧ ∀𝑗 ∈ (1...𝑁)(𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗)))))} | 
| 25 | 1, 24 | eqtri 2764 | 1
⊢ 𝐹 = {〈𝑦, 𝑠〉 ∣ (𝑦 ∈ 𝐷 ∧ (𝑠 ∈ (0[,)+∞) ∧ ∀𝑗 ∈ (1...𝑁)(𝑦‘𝑗) = (((1 − 𝑠) · (𝑍‘𝑗)) + (𝑠 · (𝑈‘𝑗)))))} |