elntg2

Description: The line definition in the Tarski structure for the Euclidean geometry. In contrast to elntg , the betweenness can be strengthened by excluding 1 resp. 0 from the related intervals (because of x =/= y ). (Contributed by AV, 14-Feb-2023)

	Ref	Expression
Hypotheses	elntg2.1	$⊢ P = {Base}_{𝔼_{𝒢} (N)}$
	elntg2.2	$⊢ I = (1 \dots N)$
Assertion	elntg2	$⊢ N \in ℕ \to {Line}_{𝒢} (𝔼_{𝒢} (N)) = (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| (\exists k \in [0, 1] \forall i \in I p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in I x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in I y (i) = (1 - m) x (i) + m p (i))\})$

Proof

Step	Hyp	Ref	Expression
1		elntg2.1	$⊢ P = {Base}_{𝔼_{𝒢} (N)}$
2		elntg2.2	$⊢ I = (1 \dots N)$
3		eqid	$⊢ Itv (𝔼_{𝒢} (N)) = Itv (𝔼_{𝒢} (N))$
4	1 3	elntg	$⊢ N \in ℕ \to {Line}_{𝒢} (𝔼_{𝒢} (N)) = (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| (p \in (x Itv (𝔼_{𝒢} (N)) y) \lor x \in (p Itv (𝔼_{𝒢} (N)) y) \lor y \in (x Itv (𝔼_{𝒢} (N)) p))\})$
5		simpl1	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to N \in ℕ$
6		simpl2	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to x \in P$
7		eldifi	$⊢ y \in (P ∖ \{x\}) \to y \in P$
8	7	3ad2ant3	$⊢ (N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \to y \in P$
9	8	adantr	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to y \in P$
10		simpr	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to p \in P$
11	5 1 3 6 9 10	ebtwntg	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (p Btwn ⟨x, y⟩ \leftrightarrow p \in (x Itv (𝔼_{𝒢} (N)) y))$
12		eengbas	$⊢ N \in ℕ \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
13	1 12	eqtr4id	$⊢ N \in ℕ \to P = 𝔼 (N)$
14	13	3ad2ant1	$⊢ (N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \to P = 𝔼 (N)$
15	14	eleq2d	$⊢ (N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \to (p \in P \leftrightarrow p \in 𝔼 (N))$
16	15	biimpa	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to p \in 𝔼 (N)$
17	13	eleq2d	$⊢ N \in ℕ \to (x \in P \leftrightarrow x \in 𝔼 (N))$
18	17	biimpa	$⊢ (N \in ℕ \land x \in P) \to x \in 𝔼 (N)$
19	18	3adant3	$⊢ (N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \to x \in 𝔼 (N)$
20	19	adantr	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to x \in 𝔼 (N)$
21	13	eleq2d	$⊢ N \in ℕ \to (y \in P \leftrightarrow y \in 𝔼 (N))$
22	21	biimpcd	$⊢ y \in P \to (N \in ℕ \to y \in 𝔼 (N))$
23	22 7	syl11	$⊢ N \in ℕ \to (y \in (P ∖ \{x\}) \to y \in 𝔼 (N))$
24	23	a1d	$⊢ N \in ℕ \to (x \in P \to (y \in (P ∖ \{x\}) \to y \in 𝔼 (N)))$
25	24	3imp	$⊢ (N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \to y \in 𝔼 (N)$
26	25	adantr	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to y \in 𝔼 (N)$
27		brbtwn	$⊢ (p \in 𝔼 (N) \land x \in 𝔼 (N) \land y \in 𝔼 (N)) \to (p Btwn ⟨x, y⟩ \leftrightarrow \exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i))$
28	16 20 26 27	syl3anc	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (p Btwn ⟨x, y⟩ \leftrightarrow \exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i))$
29	2	raleqi	$⊢ \forall i \in I p (i) = (1 - k) x (i) + k y (i) \leftrightarrow \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i)$
30	29	rexbii	$⊢ \exists k \in [0, 1] \forall i \in I p (i) = (1 - k) x (i) + k y (i) \leftrightarrow \exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i)$
31	28 30	bitr4di	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (p Btwn ⟨x, y⟩ \leftrightarrow \exists k \in [0, 1] \forall i \in I p (i) = (1 - k) x (i) + k y (i))$
32	11 31	bitr3d	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (p \in (x Itv (𝔼_{𝒢} (N)) y) \leftrightarrow \exists k \in [0, 1] \forall i \in I p (i) = (1 - k) x (i) + k y (i))$
33	5 1 3 10 9 6	ebtwntg	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (x Btwn ⟨p, y⟩ \leftrightarrow x \in (p Itv (𝔼_{𝒢} (N)) y))$
34		brbtwn	$⊢ (x \in 𝔼 (N) \land p \in 𝔼 (N) \land y \in 𝔼 (N)) \to (x Btwn ⟨p, y⟩ \leftrightarrow \exists l \in [0, 1] \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i))$
35	20 16 26 34	syl3anc	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (x Btwn ⟨p, y⟩ \leftrightarrow \exists l \in [0, 1] \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i))$
36	33 35	bitr3d	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (x \in (p Itv (𝔼_{𝒢} (N)) y) \leftrightarrow \exists l \in [0, 1] \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i))$
37		0xr	$⊢ 0 \in ℝ^{*}$
38		1xr	$⊢ 1 \in ℝ^{*}$
39		0le1	$⊢ 0 \leq 1$
40		snunico	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{} \land 0 \leq 1) \to [0, 1) \cup \{1\} = [0, 1]$
41	37 38 39 40	mp3an	$⊢ [0, 1) \cup \{1\} = [0, 1]$
42	41	eqcomi	$⊢ [0, 1] = [0, 1) \cup \{1\}$
43	42	a1i	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to [0, 1] = [0, 1) \cup \{1\}$
44	43	rexeqdv	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (\exists l \in [0, 1] \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \leftrightarrow \exists l \in ([0, 1) \cup \{1\}) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i))$
45		rexun	$⊢ \exists l \in ([0, 1) \cup \{1\}) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \leftrightarrow (\exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists l \in \{1\} \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i))$
46		eldifsn	$⊢ y \in (P ∖ \{x\}) \leftrightarrow (y \in P \land y \neq x)$
47		elee	$⊢ N \in ℕ \to (x \in 𝔼 (N) \leftrightarrow x : (1 \dots N) ⟶ ℝ)$
48		ffn	$⊢ x : (1 \dots N) ⟶ ℝ \to x Fn (1 \dots N)$
49	47 48	syl6bi	$⊢ N \in ℕ \to (x \in 𝔼 (N) \to x Fn (1 \dots N))$
50	17 49	sylbid	$⊢ N \in ℕ \to (x \in P \to x Fn (1 \dots N))$
51	50	a1i	$⊢ y \in P \to (N \in ℕ \to (x \in P \to x Fn (1 \dots N)))$
52	51	3imp	$⊢ (y \in P \land N \in ℕ \land x \in P) \to x Fn (1 \dots N)$
53		elee	$⊢ N \in ℕ \to (y \in 𝔼 (N) \leftrightarrow y : (1 \dots N) ⟶ ℝ)$
54		ffn	$⊢ y : (1 \dots N) ⟶ ℝ \to y Fn (1 \dots N)$
55	53 54	syl6bi	$⊢ N \in ℕ \to (y \in 𝔼 (N) \to y Fn (1 \dots N))$
56	21 55	sylbid	$⊢ N \in ℕ \to (y \in P \to y Fn (1 \dots N))$
57	56	a1i	$⊢ x \in P \to (N \in ℕ \to (y \in P \to y Fn (1 \dots N)))$
58	57	3imp31	$⊢ (y \in P \land N \in ℕ \land x \in P) \to y Fn (1 \dots N)$
59		eqfnfv	$⊢ (x Fn (1 \dots N) \land y Fn (1 \dots N)) \to (x = y \leftrightarrow \forall i \in (1 \dots N) x (i) = y (i))$
60	52 58 59	syl2anc	$⊢ (y \in P \land N \in ℕ \land x \in P) \to (x = y \leftrightarrow \forall i \in (1 \dots N) x (i) = y (i))$
61	60	biimprd	$⊢ (y \in P \land N \in ℕ \land x \in P) \to (\forall i \in (1 \dots N) x (i) = y (i) \to x = y)$
62		eqcom	$⊢ y = x \leftrightarrow x = y$
63	61 62	imbitrrdi	$⊢ (y \in P \land N \in ℕ \land x \in P) \to (\forall i \in (1 \dots N) x (i) = y (i) \to y = x)$
64	63	necon3ad	$⊢ (y \in P \land N \in ℕ \land x \in P) \to (y \neq x \to \neg \forall i \in (1 \dots N) x (i) = y (i))$
65	64	3exp	$⊢ y \in P \to (N \in ℕ \to (x \in P \to (y \neq x \to \neg \forall i \in (1 \dots N) x (i) = y (i))))$
66	65	com24	$⊢ y \in P \to (y \neq x \to (x \in P \to (N \in ℕ \to \neg \forall i \in (1 \dots N) x (i) = y (i))))$
67	66	imp	$⊢ (y \in P \land y \neq x) \to (x \in P \to (N \in ℕ \to \neg \forall i \in (1 \dots N) x (i) = y (i)))$
68	46 67	sylbi	$⊢ y \in (P ∖ \{x\}) \to (x \in P \to (N \in ℕ \to \neg \forall i \in (1 \dots N) x (i) = y (i)))$
69	68	3imp31	$⊢ (N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \to \neg \forall i \in (1 \dots N) x (i) = y (i)$
70	69	adantr	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to \neg \forall i \in (1 \dots N) x (i) = y (i)$
71	13	eleq2d	$⊢ N \in ℕ \to (p \in P \leftrightarrow p \in 𝔼 (N))$
72		elee	$⊢ N \in ℕ \to (p \in 𝔼 (N) \leftrightarrow p : (1 \dots N) ⟶ ℝ)$
73	72	biimpd	$⊢ N \in ℕ \to (p \in 𝔼 (N) \to p : (1 \dots N) ⟶ ℝ)$
74	71 73	sylbid	$⊢ N \in ℕ \to (p \in P \to p : (1 \dots N) ⟶ ℝ)$
75	74	3ad2ant1	$⊢ (N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \to (p \in P \to p : (1 \dots N) ⟶ ℝ)$
76	75	imp	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to p : (1 \dots N) ⟶ ℝ$
77	76	ffvelcdmda	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to p (i) \in ℝ$
78	77	recnd	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to p (i) \in ℂ$
79	78	mul02d	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to 0 \cdot p (i) = 0$
80	22 53	mpbidi	$⊢ y \in P \to (N \in ℕ \to y : (1 \dots N) ⟶ ℝ)$
81	80 7	syl11	$⊢ N \in ℕ \to (y \in (P ∖ \{x\}) \to y : (1 \dots N) ⟶ ℝ)$
82	81	a1d	$⊢ N \in ℕ \to (x \in P \to (y \in (P ∖ \{x\}) \to y : (1 \dots N) ⟶ ℝ))$
83	82	3imp	$⊢ (N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \to y : (1 \dots N) ⟶ ℝ$
84	83	adantr	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to y : (1 \dots N) ⟶ ℝ$
85	84	ffvelcdmda	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to y (i) \in ℝ$
86	85	recnd	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to y (i) \in ℂ$
87	86	mullidd	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to 1 y (i) = y (i)$
88	79 87	oveq12d	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to 0 \cdot p (i) + 1 y (i) = 0 + y (i)$
89	86	addlidd	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to 0 + y (i) = y (i)$
90	88 89	eqtrd	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to 0 \cdot p (i) + 1 y (i) = y (i)$
91	90	eqeq2d	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to (x (i) = 0 \cdot p (i) + 1 y (i) \leftrightarrow x (i) = y (i))$
92	91	ralbidva	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (\forall i \in (1 \dots N) x (i) = 0 \cdot p (i) + 1 y (i) \leftrightarrow \forall i \in (1 \dots N) x (i) = y (i))$
93	70 92	mtbird	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to \neg \forall i \in (1 \dots N) x (i) = 0 \cdot p (i) + 1 y (i)$
94		1re	$⊢ 1 \in ℝ$
95		oveq2	$⊢ l = 1 \to 1 - l = 1 - 1$
96	95	oveq1d	$⊢ l = 1 \to (1 - l) p (i) = (1 - 1) p (i)$
97		1m1e0	$⊢ 1 - 1 = 0$
98	97	oveq1i	$⊢ (1 - 1) p (i) = 0 \cdot p (i)$
99	96 98	eqtrdi	$⊢ l = 1 \to (1 - l) p (i) = 0 \cdot p (i)$
100		oveq1	$⊢ l = 1 \to l y (i) = 1 y (i)$
101	99 100	oveq12d	$⊢ l = 1 \to (1 - l) p (i) + l y (i) = 0 \cdot p (i) + 1 y (i)$
102	101	eqeq2d	$⊢ l = 1 \to (x (i) = (1 - l) p (i) + l y (i) \leftrightarrow x (i) = 0 \cdot p (i) + 1 y (i))$
103	102	ralbidv	$⊢ l = 1 \to (\forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \leftrightarrow \forall i \in (1 \dots N) x (i) = 0 \cdot p (i) + 1 y (i))$
104	103	rexsng	$⊢ 1 \in ℝ \to (\exists l \in \{1\} \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \leftrightarrow \forall i \in (1 \dots N) x (i) = 0 \cdot p (i) + 1 y (i))$
105	94 104	ax-mp	$⊢ \exists l \in \{1\} \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \leftrightarrow \forall i \in (1 \dots N) x (i) = 0 \cdot p (i) + 1 y (i)$
106	93 105	sylnibr	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to \neg \exists l \in \{1\} \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)$
107	2	raleqi	$⊢ \forall i \in I x (i) = (1 - l) p (i) + l y (i) \leftrightarrow \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)$
108	107	rexbii	$⊢ \exists l \in [0, 1) \forall i \in I x (i) = (1 - l) p (i) + l y (i) \leftrightarrow \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)$
109		biorf	$⊢ \neg \exists l \in \{1\} \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \to (\exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \leftrightarrow (\exists l \in \{1\} \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)))$
110	108 109	bitrid	$⊢ \neg \exists l \in \{1\} \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \to (\exists l \in [0, 1) \forall i \in I x (i) = (1 - l) p (i) + l y (i) \leftrightarrow (\exists l \in \{1\} \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)))$
111	106 110	syl	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (\exists l \in [0, 1) \forall i \in I x (i) = (1 - l) p (i) + l y (i) \leftrightarrow (\exists l \in \{1\} \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)))$
112		orcom	$⊢ (\exists l \in \{1\} \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)) \leftrightarrow (\exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists l \in \{1\} \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i))$
113	111 112	bitr2di	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to ((\exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists l \in \{1\} \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)) \leftrightarrow \exists l \in [0, 1) \forall i \in I x (i) = (1 - l) p (i) + l y (i))$
114	45 113	bitrid	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (\exists l \in ([0, 1) \cup \{1\}) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \leftrightarrow \exists l \in [0, 1) \forall i \in I x (i) = (1 - l) p (i) + l y (i))$
115	36 44 114	3bitrd	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (x \in (p Itv (𝔼_{𝒢} (N)) y) \leftrightarrow \exists l \in [0, 1) \forall i \in I x (i) = (1 - l) p (i) + l y (i))$
116	5 1 3 6 10 9	ebtwntg	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (y Btwn ⟨x, p⟩ \leftrightarrow y \in (x Itv (𝔼_{𝒢} (N)) p))$
117		brbtwn	$⊢ (y \in 𝔼 (N) \land x \in 𝔼 (N) \land p \in 𝔼 (N)) \to (y Btwn ⟨x, p⟩ \leftrightarrow \exists m \in [0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))$
118	26 20 16 117	syl3anc	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (y Btwn ⟨x, p⟩ \leftrightarrow \exists m \in [0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))$
119	116 118	bitr3d	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (y \in (x Itv (𝔼_{𝒢} (N)) p) \leftrightarrow \exists m \in [0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))$
120		snunioc	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{} \land 0 \leq 1) \to \{0\} \cup (0, 1] = [0, 1]$
121	37 38 39 120	mp3an	$⊢ \{0\} \cup (0, 1] = [0, 1]$
122	121	eqcomi	$⊢ [0, 1] = \{0\} \cup (0, 1]$
123	122	a1i	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to [0, 1] = \{0\} \cup (0, 1]$
124	123	rexeqdv	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (\exists m \in [0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \leftrightarrow \exists m \in (\{0\} \cup (0, 1]) \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))$
125		rexun	$⊢ \exists m \in (\{0\} \cup (0, 1]) \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \leftrightarrow (\exists m \in \{0\} \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))$
126		eqcom	$⊢ x (i) = y (i) \leftrightarrow y (i) = x (i)$
127	126	ralbii	$⊢ \forall i \in (1 \dots N) x (i) = y (i) \leftrightarrow \forall i \in (1 \dots N) y (i) = x (i)$
128	70 127	sylnib	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to \neg \forall i \in (1 \dots N) y (i) = x (i)$
129	17	biimpd	$⊢ N \in ℕ \to (x \in P \to x \in 𝔼 (N))$
130	129 47	sylibd	$⊢ N \in ℕ \to (x \in P \to x : (1 \dots N) ⟶ ℝ)$
131	130	imp	$⊢ (N \in ℕ \land x \in P) \to x : (1 \dots N) ⟶ ℝ$
132	131	3adant3	$⊢ (N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \to x : (1 \dots N) ⟶ ℝ$
133	132	adantr	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to x : (1 \dots N) ⟶ ℝ$
134	133	ffvelcdmda	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to x (i) \in ℝ$
135	134	recnd	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to x (i) \in ℂ$
136	135	mullidd	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to 1 x (i) = x (i)$
137	136 79	oveq12d	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to 1 x (i) + 0 \cdot p (i) = x (i) + 0$
138	135	addridd	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to x (i) + 0 = x (i)$
139	137 138	eqtrd	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to 1 x (i) + 0 \cdot p (i) = x (i)$
140	139	eqeq2d	$⊢ (((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land i \in (1 \dots N)) \to (y (i) = 1 x (i) + 0 \cdot p (i) \leftrightarrow y (i) = x (i))$
141	140	ralbidva	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (\forall i \in (1 \dots N) y (i) = 1 x (i) + 0 \cdot p (i) \leftrightarrow \forall i \in (1 \dots N) y (i) = x (i))$
142	128 141	mtbird	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to \neg \forall i \in (1 \dots N) y (i) = 1 x (i) + 0 \cdot p (i)$
143		0re	$⊢ 0 \in ℝ$
144		oveq2	$⊢ m = 0 \to 1 - m = 1 - 0$
145	144	oveq1d	$⊢ m = 0 \to (1 - m) x (i) = (1 - 0) x (i)$
146		1m0e1	$⊢ 1 - 0 = 1$
147	146	oveq1i	$⊢ (1 - 0) x (i) = 1 x (i)$
148	145 147	eqtrdi	$⊢ m = 0 \to (1 - m) x (i) = 1 x (i)$
149		oveq1	$⊢ m = 0 \to m p (i) = 0 \cdot p (i)$
150	148 149	oveq12d	$⊢ m = 0 \to (1 - m) x (i) + m p (i) = 1 x (i) + 0 \cdot p (i)$
151	150	eqeq2d	$⊢ m = 0 \to (y (i) = (1 - m) x (i) + m p (i) \leftrightarrow y (i) = 1 x (i) + 0 \cdot p (i))$
152	151	ralbidv	$⊢ m = 0 \to (\forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \leftrightarrow \forall i \in (1 \dots N) y (i) = 1 x (i) + 0 \cdot p (i))$
153	152	rexsng	$⊢ 0 \in ℝ \to (\exists m \in \{0\} \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \leftrightarrow \forall i \in (1 \dots N) y (i) = 1 x (i) + 0 \cdot p (i))$
154	143 153	ax-mp	$⊢ \exists m \in \{0\} \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \leftrightarrow \forall i \in (1 \dots N) y (i) = 1 x (i) + 0 \cdot p (i)$
155	142 154	sylnibr	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to \neg \exists m \in \{0\} \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)$
156	2	raleqi	$⊢ \forall i \in I y (i) = (1 - m) x (i) + m p (i) \leftrightarrow \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)$
157	156	rexbii	$⊢ \exists m \in (0, 1] \forall i \in I y (i) = (1 - m) x (i) + m p (i) \leftrightarrow \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)$
158		biorf	$⊢ \neg \exists m \in \{0\} \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \to (\exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \leftrightarrow (\exists m \in \{0\} \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)))$
159	157 158	bitrid	$⊢ \neg \exists m \in \{0\} \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \to (\exists m \in (0, 1] \forall i \in I y (i) = (1 - m) x (i) + m p (i) \leftrightarrow (\exists m \in \{0\} \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)))$
160	155 159	syl	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (\exists m \in (0, 1] \forall i \in I y (i) = (1 - m) x (i) + m p (i) \leftrightarrow (\exists m \in \{0\} \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)))$
161	125 160	bitr4id	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (\exists m \in (\{0\} \cup (0, 1]) \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \leftrightarrow \exists m \in (0, 1] \forall i \in I y (i) = (1 - m) x (i) + m p (i))$
162	119 124 161	3bitrd	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to (y \in (x Itv (𝔼_{𝒢} (N)) p) \leftrightarrow \exists m \in (0, 1] \forall i \in I y (i) = (1 - m) x (i) + m p (i))$
163	32 115 162	3orbi123d	$⊢ ((N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to ((p \in (x Itv (𝔼_{𝒢} (N)) y) \lor x \in (p Itv (𝔼_{𝒢} (N)) y) \lor y \in (x Itv (𝔼_{𝒢} (N)) p)) \leftrightarrow (\exists k \in [0, 1] \forall i \in I p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in I x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in I y (i) = (1 - m) x (i) + m p (i)))$
164	163	rabbidva	$⊢ (N \in ℕ \land x \in P \land y \in (P ∖ \{x\})) \to \{p \in P \| (p \in (x Itv (𝔼_{𝒢} (N)) y) \lor x \in (p Itv (𝔼_{𝒢} (N)) y) \lor y \in (x Itv (𝔼_{𝒢} (N)) p))\} = \{p \in P \| (\exists k \in [0, 1] \forall i \in I p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in I x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in I y (i) = (1 - m) x (i) + m p (i))\}$
165	164	mpoeq3dva	$⊢ N \in ℕ \to (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| (p \in (x Itv (𝔼_{𝒢} (N)) y) \lor x \in (p Itv (𝔼_{𝒢} (N)) y) \lor y \in (x Itv (𝔼_{𝒢} (N)) p))\}) = (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| (\exists k \in [0, 1] \forall i \in I p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in I x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in I y (i) = (1 - m) x (i) + m p (i))\})$
166	4 165	eqtrd	$⊢ N \in ℕ \to {Line}_{𝒢} (𝔼_{𝒢} (N)) = (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| (\exists k \in [0, 1] \forall i \in I p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in I x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in I y (i) = (1 - m) x (i) + m p (i))\})$

Metamath Proof Explorer

Theorem elntg2

Proof