Theorem axcontlem5

Description: Lemma for axcont . Compute the value of F . (Contributed by Scott Fenton, 18-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		axcontlem5.1	⊢ 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
2		axcontlem5.2	⊢ 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
3	1 2	axcontlem2	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) )
4		f1of	⊢ ( 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) → 𝐹 : 𝐷 ⟶ ( 0 [,) +∞ ) )
5	3 4	syl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → 𝐹 : 𝐷 ⟶ ( 0 [,) +∞ ) )
6	5	ffvelrnda	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑃 ) ∈ ( 0 [,) +∞ ) )
7		eleq1	⊢ ( ( 𝐹 ‘ 𝑃 ) = 𝑇 → ( ( 𝐹 ‘ 𝑃 ) ∈ ( 0 [,) +∞ ) ↔ 𝑇 ∈ ( 0 [,) +∞ ) ) )
8	6 7	syl5ibcom	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑃 ) = 𝑇 → 𝑇 ∈ ( 0 [,) +∞ ) ) )
9		simpl	⊢ ( ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) → 𝑇 ∈ ( 0 [,) +∞ ) )
10	9	a1i	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ) → ( ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) → 𝑇 ∈ ( 0 [,) +∞ ) ) )
11		f1ofn	⊢ ( 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) → 𝐹 Fn 𝐷 )
12	3 11	syl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → 𝐹 Fn 𝐷 )
13		fnbrfvb	⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝑃 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑃 ) = 𝑇 ↔ 𝑃 𝐹 𝑇 ) )
14	12 13	sylan	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑃 ) = 𝑇 ↔ 𝑃 𝐹 𝑇 ) )
15	14	3adant3	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) → ( ( 𝐹 ‘ 𝑃 ) = 𝑇 ↔ 𝑃 𝐹 𝑇 ) )
16		eleq1	⊢ ( 𝑥 = 𝑃 → ( 𝑥 ∈ 𝐷 ↔ 𝑃 ∈ 𝐷 ) )
17		fveq1	⊢ ( 𝑥 = 𝑃 → ( 𝑥 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) )
18	17	eqeq1d	⊢ ( 𝑥 = 𝑃 → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
19	18	ralbidv	⊢ ( 𝑥 = 𝑃 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
20	19	anbi2d	⊢ ( 𝑥 = 𝑃 → ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
21	16 20	anbi12d	⊢ ( 𝑥 = 𝑃 → ( ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ↔ ( 𝑃 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ) )
22		eleq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ∈ ( 0 [,) +∞ ) ↔ 𝑇 ∈ ( 0 [,) +∞ ) ) )
23		oveq2	⊢ ( 𝑡 = 𝑇 → ( 1 − 𝑡 ) = ( 1 − 𝑇 ) )
24	23	oveq1d	⊢ ( 𝑡 = 𝑇 → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) )
25		oveq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) = ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) )
26	24 25	oveq12d	⊢ ( 𝑡 = 𝑇 → ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) )
27	26	eqeq2d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
28	27	ralbidv	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
29	22 28	anbi12d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
30	29	anbi2d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑃 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ↔ ( 𝑃 ∈ 𝐷 ∧ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ) )
31		anass	⊢ ( ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ↔ ( 𝑃 ∈ 𝐷 ∧ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ) )
32		anidm	⊢ ( ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ↔ 𝑇 ∈ ( 0 [,) +∞ ) )
33	32	anbi2i	⊢ ( ( 𝑃 ∈ 𝐷 ∧ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ) ↔ ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) )
34	31 33	bitr2i	⊢ ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ↔ ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) )
35	34	anbi1i	⊢ ( ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ( ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
36		anass	⊢ ( ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ( 𝑃 ∈ 𝐷 ∧ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
37		anass	⊢ ( ( ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
38	35 36 37	3bitr3i	⊢ ( ( 𝑃 ∈ 𝐷 ∧ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ↔ ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
39	30 38	bitrdi	⊢ ( 𝑡 = 𝑇 → ( ( 𝑃 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ↔ ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ) )
40	21 39 2	brabg	⊢ ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) → ( 𝑃 𝐹 𝑇 ↔ ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ) )
41	40	bianabs	⊢ ( ( 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) → ( 𝑃 𝐹 𝑇 ↔ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
42	41	3adant1	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) → ( 𝑃 𝐹 𝑇 ↔ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
43	15 42	bitrd	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,) +∞ ) ) → ( ( 𝐹 ‘ 𝑃 ) = 𝑇 ↔ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
44	43	3expia	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ) → ( 𝑇 ∈ ( 0 [,) +∞ ) → ( ( 𝐹 ‘ 𝑃 ) = 𝑇 ↔ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ) )
45	8 10 44	pm5.21ndd	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑃 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑃 ) = 𝑇 ↔ ( 𝑇 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )