Theorem axcontlem6

Description: Lemma for axcont . State the defining properties of the value of F . (Contributed by Scott Fenton, 19-Jun-2013)

	Ref	Expression
Hypotheses	axcontlem5.1	⊢ 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
	axcontlem5.2	⊢ 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
Assertion	axcontlem6	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑖 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		axcontlem5.1	⊢ 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
2		axcontlem5.2	⊢ 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
3		eqid	⊢ ( 𝐹 ‘ 𝑃 ) = ( 𝐹 ‘ 𝑃 )
4	2	axcontlem1	⊢ 𝐹 = { ⟨ 𝑦 , 𝑠 ⟩ ∣ ( 𝑦 ∈ 𝐷 ∧ ( 𝑠 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑗 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑗 ) ) ) ) ) }
5	1 4	axcontlem5	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑃 ) = ( 𝐹 ‘ 𝑃 ) ↔ ( ( 𝐹 ‘ 𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑗 ) = ( ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑗 ) ) + ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑗 ) ) ) ) ) )
6	3 5	mpbii	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑗 ) = ( ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑗 ) ) + ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑗 ) ) ) ) )
7		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝑖 ) )
8		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝑍 ‘ 𝑗 ) = ( 𝑍 ‘ 𝑖 ) )
9	8	oveq2d	⊢ ( 𝑗 = 𝑖 → ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑗 ) ) = ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑖 ) ) )
10		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝑈 ‘ 𝑗 ) = ( 𝑈 ‘ 𝑖 ) )
11	10	oveq2d	⊢ ( 𝑗 = 𝑖 → ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑗 ) ) = ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑖 ) ) )
12	9 11	oveq12d	⊢ ( 𝑗 = 𝑖 → ( ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑗 ) ) + ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑗 ) ) ) = ( ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑖 ) ) ) )
13	7 12	eqeq12d	⊢ ( 𝑗 = 𝑖 → ( ( 𝑃 ‘ 𝑗 ) = ( ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑗 ) ) + ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑗 ) ) ) ↔ ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑖 ) ) ) ) )
14	13	cbvralvw	⊢ ( ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑗 ) = ( ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑗 ) ) + ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑗 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑖 ) ) ) )
15	14	anbi2i	⊢ ( ( ( 𝐹 ‘ 𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑗 ) = ( ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑗 ) ) + ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑗 ) ) ) ) ↔ ( ( 𝐹 ‘ 𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑖 ) ) ) ) )
16	6 15	sylib	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − ( 𝐹 ‘ 𝑃 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝐹 ‘ 𝑃 ) · ( 𝑈 ‘ 𝑖 ) ) ) ) )