Theorem axcontlem1

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

	Ref	Expression
Hypothesis	axcontlem1.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
Assertion	axcontlem1	⊢ 𝐹 = { ⟨ 𝑦 , 𝑠 ⟩ ∣ ( 𝑦 ∈ 𝐷 ∧ ( 𝑠 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑗 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑗 ) ) ) ) ) }

Proof

Step	Hyp	Ref	Expression
1		axcontlem1.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
2		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷 ) )
3	2	adantr	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑡 = 𝑠 ) → ( 𝑥 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷 ) )
4		eleq1w	⊢ ( 𝑡 = 𝑠 → ( 𝑡 ∈ ( 0 [,) +∞ ) ↔ 𝑠 ∈ ( 0 [,) +∞ ) ) )
5	4	adantl	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑡 = 𝑠 ) → ( 𝑡 ∈ ( 0 [,) +∞ ) ↔ 𝑠 ∈ ( 0 [,) +∞ ) ) )
6		fveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) )
7		oveq2	⊢ ( 𝑡 = 𝑠 → ( 1 − 𝑡 ) = ( 1 − 𝑠 ) )
8	7	oveq1d	⊢ ( 𝑡 = 𝑠 → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) )
9		oveq1	⊢ ( 𝑡 = 𝑠 → ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) = ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) )
10	8 9	oveq12d	⊢ ( 𝑡 = 𝑠 → ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) )
11	6 10	eqeqan12d	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑡 = 𝑠 ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
12	11	ralbidv	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑡 = 𝑠 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
13		fveq2	⊢ ( 𝑖 = 𝑗 → ( 𝑦 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑗 ) )
14		fveq2	⊢ ( 𝑖 = 𝑗 → ( 𝑍 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑗 ) )
15	14	oveq2d	⊢ ( 𝑖 = 𝑗 → ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑗 ) ) )
16		fveq2	⊢ ( 𝑖 = 𝑗 → ( 𝑈 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑗 ) )
17	16	oveq2d	⊢ ( 𝑖 = 𝑗 → ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) = ( 𝑠 · ( 𝑈 ‘ 𝑗 ) ) )
18	15 17	oveq12d	⊢ ( 𝑖 = 𝑗 → ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑗 ) ) ) )
19	13 18	eqeq12d	⊢ ( 𝑖 = 𝑗 → ( ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( 𝑦 ‘ 𝑗 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑗 ) ) ) ) )
20	19	cbvralvw	⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑗 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑗 ) ) ) )
21	12 20	bitrdi	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑡 = 𝑠 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑗 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑗 ) ) ) ) )
22	5 21	anbi12d	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑡 = 𝑠 ) → ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ( 𝑠 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑗 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑗 ) ) ) ) ) )
23	3 22	anbi12d	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑡 = 𝑠 ) → ( ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ↔ ( 𝑦 ∈ 𝐷 ∧ ( 𝑠 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑗 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑗 ) ) ) ) ) ) )
24	23	cbvopabv	⊢ { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) } = { ⟨ 𝑦 , 𝑠 ⟩ ∣ ( 𝑦 ∈ 𝐷 ∧ ( 𝑠 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑗 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑗 ) ) ) ) ) }
25	1 24	eqtri	⊢ 𝐹 = { ⟨ 𝑦 , 𝑠 ⟩ ∣ ( 𝑦 ∈ 𝐷 ∧ ( 𝑠 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑗 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑗 ) ) ) ) ) }