Metamath Proof Explorer

Theorem axcontlem1

Description: Lemma for axcont . Change bound variables for later use. (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Hypothesis axcontlem1.1 ⊢ F = x t | x ∈ D ∧ t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i
Assertion axcontlem1 ⊢ F = y s | y ∈ D ∧ s ∈ 0 +∞ ∧ ∀ j ∈ 1 … N y ⁡ j = 1 − s ⁢ Z ⁡ j + s ⁢ U ⁡ j

Proof

Step Hyp Ref Expression
1 axcontlem1.1 ⊢ F = x t | x ∈ D ∧ t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i
2 eleq1w ⊢ x = y → x ∈ D ↔ y ∈ D
3 2 adantr ⊢ x = y ∧ t = s → x ∈ D ↔ y ∈ D
4 eleq1w ⊢ t = s → t ∈ 0 +∞ ↔ s ∈ 0 +∞
5 4 adantl ⊢ x = y ∧ t = s → t ∈ 0 +∞ ↔ s ∈ 0 +∞
6 fveq1 ⊢ x = y → x ⁡ i = y ⁡ i
7 oveq2 ⊢ t = s → 1 − t = 1 − s
8 7 oveq1d ⊢ t = s → 1 − t ⁢ Z ⁡ i = 1 − s ⁢ Z ⁡ i
9 oveq1 ⊢ t = s → t ⁢ U ⁡ i = s ⁢ U ⁡ i
10 8 9 oveq12d ⊢ t = s → 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i = 1 − s ⁢ Z ⁡ i + s ⁢ U ⁡ i
11 6 10 eqeqan12d ⊢ x = y ∧ t = s → x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ y ⁡ i = 1 − s ⁢ Z ⁡ i + s ⁢ U ⁡ i
12 11 ralbidv ⊢ x = y ∧ t = s → ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ ∀ i ∈ 1 … N y ⁡ i = 1 − s ⁢ Z ⁡ i + s ⁢ U ⁡ i
13 fveq2 ⊢ i = j → y ⁡ i = y ⁡ j
14 fveq2 ⊢ i = j → Z ⁡ i = Z ⁡ j
15 14 oveq2d ⊢ i = j → 1 − s ⁢ Z ⁡ i = 1 − s ⁢ Z ⁡ j
16 fveq2 ⊢ i = j → U ⁡ i = U ⁡ j
17 16 oveq2d ⊢ i = j → s ⁢ U ⁡ i = s ⁢ U ⁡ j
18 15 17 oveq12d ⊢ i = j → 1 − s ⁢ Z ⁡ i + s ⁢ U ⁡ i = 1 − s ⁢ Z ⁡ j + s ⁢ U ⁡ j
19 13 18 eqeq12d ⊢ i = j → y ⁡ i = 1 − s ⁢ Z ⁡ i + s ⁢ U ⁡ i ↔ y ⁡ j = 1 − s ⁢ Z ⁡ j + s ⁢ U ⁡ j
20 19 cbvralvw ⊢ ∀ i ∈ 1 … N y ⁡ i = 1 − s ⁢ Z ⁡ i + s ⁢ U ⁡ i ↔ ∀ j ∈ 1 … N y ⁡ j = 1 − s ⁢ Z ⁡ j + s ⁢ U ⁡ j
21 12 20 bitrdi ⊢ x = y ∧ t = s → ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ ∀ j ∈ 1 … N y ⁡ j = 1 − s ⁢ Z ⁡ j + s ⁢ U ⁡ j
22 5 21 anbi12d ⊢ x = y ∧ t = s → t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ s ∈ 0 +∞ ∧ ∀ j ∈ 1 … N y ⁡ j = 1 − s ⁢ Z ⁡ j + s ⁢ U ⁡ j
23 3 22 anbi12d ⊢ x = y ∧ t = s → x ∈ D ∧ t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ y ∈ D ∧ s ∈ 0 +∞ ∧ ∀ j ∈ 1 … N y ⁡ j = 1 − s ⁢ Z ⁡ j + s ⁢ U ⁡ j
24 23 cbvopabv ⊢ x t | x ∈ D ∧ t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i = y s | y ∈ D ∧ s ∈ 0 +∞ ∧ ∀ j ∈ 1 … N y ⁡ j = 1 − s ⁢ Z ⁡ j + s ⁢ U ⁡ j
25 1 24 eqtri ⊢ F = y s | y ∈ D ∧ s ∈ 0 +∞ ∧ ∀ j ∈ 1 … N y ⁡ j = 1 − s ⁢ Z ⁡ j + s ⁢ U ⁡ j