axcontlem5

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

	Ref	Expression
Hypotheses	axcontlem5.1	$⊢ D = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
	axcontlem5.2	$⊢ F = \{⟨x, t⟩ \| (x \in D \land (t \in [0, +∞) \land \forall i \in (1 \dots N) x (i) = (1 - t) Z (i) + t U (i)))\}$
Assertion	axcontlem5	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land P \in D) \to (F (P) = T \leftrightarrow (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)))$

Proof

Step	Hyp	Ref	Expression
1		axcontlem5.1	$⊢ D = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
2		axcontlem5.2	$⊢ F = \{⟨x, t⟩ \| (x \in D \land (t \in [0, +∞) \land \forall i \in (1 \dots N) x (i) = (1 - t) Z (i) + t U (i)))\}$
3	1 2	axcontlem2	$⊢ ((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \to F : D \underset{1-1 onto}{⟶} [0, +∞)$
4		f1of	$⊢ F : D \underset{1-1 onto}{⟶} [0, +∞) \to F : D ⟶ [0, +∞)$
5	3 4	syl	$⊢ ((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \to F : D ⟶ [0, +∞)$
6	5	ffvelrnda	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land P \in D) \to F (P) \in [0, +∞)$
7		eleq1	$⊢ F (P) = T \to (F (P) \in [0, +∞) \leftrightarrow T \in [0, +∞))$
8	6 7	syl5ibcom	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land P \in D) \to (F (P) = T \to T \in [0, +∞))$
9		simpl	$⊢ (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)) \to T \in [0, +∞)$
10	9	a1i	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land P \in D) \to ((T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)) \to T \in [0, +∞))$
11		f1ofn	$⊢ F : D \underset{1-1 onto}{⟶} [0, +∞) \to F Fn D$
12	3 11	syl	$⊢ ((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \to F Fn D$
13		fnbrfvb	$⊢ (F Fn D \land P \in D) \to (F (P) = T \leftrightarrow P F T)$
14	12 13	sylan	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land P \in D) \to (F (P) = T \leftrightarrow P F T)$
15	14	3adant3	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land P \in D \land T \in [0, +∞)) \to (F (P) = T \leftrightarrow P F T)$
16		eleq1	$⊢ x = P \to (x \in D \leftrightarrow P \in D)$
17		fveq1	$⊢ x = P \to x (i) = P (i)$
18	17	eqeq1d	$⊢ x = P \to (x (i) = (1 - t) Z (i) + t U (i) \leftrightarrow P (i) = (1 - t) Z (i) + t U (i))$
19	18	ralbidv	$⊢ x = P \to (\forall i \in (1 \dots N) x (i) = (1 - t) Z (i) + t U (i) \leftrightarrow \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t U (i))$
20	19	anbi2d	$⊢ x = P \to ((t \in [0, +∞) \land \forall i \in (1 \dots N) x (i) = (1 - t) Z (i) + t U (i)) \leftrightarrow (t \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t U (i)))$
21	16 20	anbi12d	$⊢ x = P \to ((x \in D \land (t \in [0, +∞) \land \forall i \in (1 \dots N) x (i) = (1 - t) Z (i) + t U (i))) \leftrightarrow (P \in D \land (t \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t U (i))))$
22		eleq1	$⊢ t = T \to (t \in [0, +∞) \leftrightarrow T \in [0, +∞))$
23		oveq2	$⊢ t = T \to 1 - t = 1 - T$
24	23	oveq1d	$⊢ t = T \to (1 - t) Z (i) = (1 - T) Z (i)$
25		oveq1	$⊢ t = T \to t U (i) = T U (i)$
26	24 25	oveq12d	$⊢ t = T \to (1 - t) Z (i) + t U (i) = (1 - T) Z (i) + T U (i)$
27	26	eqeq2d	$⊢ t = T \to (P (i) = (1 - t) Z (i) + t U (i) \leftrightarrow P (i) = (1 - T) Z (i) + T U (i))$
28	27	ralbidv	$⊢ t = T \to (\forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t U (i) \leftrightarrow \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i))$
29	22 28	anbi12d	$⊢ t = T \to ((t \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t U (i)) \leftrightarrow (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)))$
30	29	anbi2d	$⊢ t = T \to ((P \in D \land (t \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t U (i))) \leftrightarrow (P \in D \land (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i))))$
31		anass	$⊢ ((P \in D \land T \in [0, +∞)) \land T \in [0, +∞)) \leftrightarrow (P \in D \land (T \in [0, +∞) \land T \in [0, +∞)))$
32		anidm	$⊢ (T \in [0, +∞) \land T \in [0, +∞)) \leftrightarrow T \in [0, +∞)$
33	32	anbi2i	$⊢ (P \in D \land (T \in [0, +∞) \land T \in [0, +∞))) \leftrightarrow (P \in D \land T \in [0, +∞))$
34	31 33	bitr2i	$⊢ (P \in D \land T \in [0, +∞)) \leftrightarrow ((P \in D \land T \in [0, +∞)) \land T \in [0, +∞))$
35	34	anbi1i	$⊢ ((P \in D \land T \in [0, +∞)) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)) \leftrightarrow (((P \in D \land T \in [0, +∞)) \land T \in [0, +∞)) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i))$
36		anass	$⊢ ((P \in D \land T \in [0, +∞)) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)) \leftrightarrow (P \in D \land (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)))$
37		anass	$⊢ (((P \in D \land T \in [0, +∞)) \land T \in [0, +∞)) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)) \leftrightarrow ((P \in D \land T \in [0, +∞)) \land (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)))$
38	35 36 37	3bitr3i	$⊢ (P \in D \land (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i))) \leftrightarrow ((P \in D \land T \in [0, +∞)) \land (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)))$
39	30 38	bitrdi	$⊢ t = T \to ((P \in D \land (t \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t U (i))) \leftrightarrow ((P \in D \land T \in [0, +∞)) \land (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i))))$
40	21 39 2	brabg	$⊢ (P \in D \land T \in [0, +∞)) \to (P F T \leftrightarrow ((P \in D \land T \in [0, +∞)) \land (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i))))$
41	40	bianabs	$⊢ (P \in D \land T \in [0, +∞)) \to (P F T \leftrightarrow (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)))$
42	41	3adant1	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land P \in D \land T \in [0, +∞)) \to (P F T \leftrightarrow (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)))$
43	15 42	bitrd	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land P \in D \land T \in [0, +∞)) \to (F (P) = T \leftrightarrow (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)))$
44	43	3expia	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land P \in D) \to (T \in [0, +∞) \to (F (P) = T \leftrightarrow (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i))))$
45	8 10 44	pm5.21ndd	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land P \in D) \to (F (P) = T \leftrightarrow (T \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - T) Z (i) + T U (i)))$

Metamath Proof Explorer

Theorem axcontlem5

Proof