eenglngeehlnm

Description: The line definition in the Tarski structure for the Euclidean geometry (see elntg ) corresponds to the definition of lines passing through two different points in a left module (see rrxlines ). (Contributed by AV, 16-Feb-2023)

		Ref	Expression
	Assertion	eenglngeehlnm	$⊢ N \in ℕ \to {Line}_{𝒢} (𝔼_{𝒢} (N)) = {Line}_{M} (𝔼_{hil} (N))$

Proof

Step	Hyp	Ref	Expression
1		eengbas	$⊢ N \in ℕ \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
2	1	eqcomd	$⊢ N \in ℕ \to {Base}_{𝔼_{𝒢} (N)} = 𝔼 (N)$
3		oveq2	$⊢ n = N \to (1 \dots n) = (1 \dots N)$
4	3	oveq2d	$⊢ n = N \to ℝ^{(1 \dots n)} = ℝ^{(1 \dots N)}$
5		df-ee	$⊢ 𝔼 = (n \in ℕ ⟼ ℝ^{(1 \dots n)})$
6		ovex	$⊢ ℝ^{(1 \dots N)} \in V$
7	4 5 6	fvmpt	$⊢ N \in ℕ \to 𝔼 (N) = ℝ^{(1 \dots N)}$
8	2 7	eqtrd	$⊢ N \in ℕ \to {Base}_{𝔼_{𝒢} (N)} = ℝ^{(1 \dots N)}$
9	2	ancli	$⊢ N \in ℕ \to (N \in ℕ \land {Base}_{𝔼_{𝒢} (N)} = 𝔼 (N))$
10	9 8	jca	$⊢ N \in ℕ \to ((N \in ℕ \land {Base}_{𝔼_{𝒢} (N)} = 𝔼 (N)) \land {Base}_{𝔼_{𝒢} (N)} = ℝ^{(1 \dots N)})$
11		difeq1	$⊢ {Base}_{𝔼_{𝒢} (N)} = ℝ^{(1 \dots N)} \to {Base}_{𝔼_{𝒢} (N)} ∖ \{x\} = (ℝ^{(1 \dots N)}) ∖ \{x\}$
12	11	ad2antlr	$⊢ (((N \in ℕ \land {Base}_{𝔼_{𝒢} (N)} = 𝔼 (N)) \land {Base}_{𝔼_{𝒢} (N)} = ℝ^{(1 \dots N)}) \land x \in {Base}_{𝔼_{𝒢} (N)}) \to {Base}_{𝔼_{𝒢} (N)} ∖ \{x\} = (ℝ^{(1 \dots N)}) ∖ \{x\}$
13	10 12	sylan	$⊢ (N \in ℕ \land x \in {Base}_{𝔼_{𝒢} (N)}) \to {Base}_{𝔼_{𝒢} (N)} ∖ \{x\} = (ℝ^{(1 \dots N)}) ∖ \{x\}$
14	8	adantr	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}))) \to {Base}_{𝔼_{𝒢} (N)} = ℝ^{(1 \dots N)}$
15		simpll	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}))) \land p \in {Base}_{𝔼_{𝒢} (N)}) \to N \in ℕ$
16	8	eleq2d	$⊢ N \in ℕ \to (x \in {Base}_{𝔼_{𝒢} (N)} \leftrightarrow x \in (ℝ^{(1 \dots N)}))$
17	16	biimpcd	$⊢ x \in {Base}_{𝔼_{𝒢} (N)} \to (N \in ℕ \to x \in (ℝ^{(1 \dots N)}))$
18	17	adantr	$⊢ (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\})) \to (N \in ℕ \to x \in (ℝ^{(1 \dots N)}))$
19	18	impcom	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}))) \to x \in (ℝ^{(1 \dots N)})$
20	19	adantr	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}))) \land p \in {Base}_{𝔼_{𝒢} (N)}) \to x \in (ℝ^{(1 \dots N)})$
21	8	difeq1d	$⊢ N \in ℕ \to {Base}_{𝔼_{𝒢} (N)} ∖ \{x\} = (ℝ^{(1 \dots N)}) ∖ \{x\}$
22	21	eleq2d	$⊢ N \in ℕ \to (y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}) \leftrightarrow y \in ((ℝ^{(1 \dots N)}) ∖ \{x\}))$
23	22	biimpd	$⊢ N \in ℕ \to (y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}) \to y \in ((ℝ^{(1 \dots N)}) ∖ \{x\}))$
24	23	adantld	$⊢ N \in ℕ \to ((x \in {Base}_{𝔼_{𝒢} (N)} \land y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\})) \to y \in ((ℝ^{(1 \dots N)}) ∖ \{x\}))$
25	24	imp	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}))) \to y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})$
26	25	adantr	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}))) \land p \in {Base}_{𝔼_{𝒢} (N)}) \to y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})$
27	14	eleq2d	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}))) \to (p \in {Base}_{𝔼_{𝒢} (N)} \leftrightarrow p \in (ℝ^{(1 \dots N)}))$
28	27	biimpa	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}))) \land p \in {Base}_{𝔼_{𝒢} (N)}) \to p \in (ℝ^{(1 \dots N)})$
29		eenglngeehlnmlem1	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \to ((\exists z \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - z) x (i) + z y (i) \lor \exists v \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - v) p (i) + v y (i) \lor \exists w \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - w) x (i) + w p (i)) \to \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i))$
30		eenglngeehlnmlem2	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \to (\exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to (\exists z \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - z) x (i) + z y (i) \lor \exists v \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - v) p (i) + v y (i) \lor \exists w \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - w) x (i) + w p (i)))$
31	29 30	impbid	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \to ((\exists z \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - z) x (i) + z y (i) \lor \exists v \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - v) p (i) + v y (i) \lor \exists w \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - w) x (i) + w p (i)) \leftrightarrow \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i))$
32	15 20 26 28 31	syl31anc	$⊢ ((N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}))) \land p \in {Base}_{𝔼_{𝒢} (N)}) \to ((\exists z \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - z) x (i) + z y (i) \lor \exists v \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - v) p (i) + v y (i) \lor \exists w \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - w) x (i) + w p (i)) \leftrightarrow \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i))$
33	14 32	rabeqbidva	$⊢ (N \in ℕ \land (x \in {Base}_{𝔼_{𝒢} (N)} \land y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}))) \to \{p \in {Base}_{𝔼_{𝒢} (N)} \| (\exists z \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - z) x (i) + z y (i) \lor \exists v \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - v) p (i) + v y (i) \lor \exists w \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - w) x (i) + w p (i))\} = \{p \in (ℝ^{(1 \dots N)}) \| \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)\}$
34	8 13 33	mpoeq123dva	$⊢ N \in ℕ \to (x \in {Base}_{𝔼_{𝒢} (N)}, y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}) ⟼ \{p \in {Base}_{𝔼_{𝒢} (N)} \| (\exists z \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - z) x (i) + z y (i) \lor \exists v \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - v) p (i) + v y (i) \lor \exists w \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - w) x (i) + w p (i))\}) = (x \in (ℝ^{(1 \dots N)}), y \in ((ℝ^{(1 \dots N)}) ∖ \{x\}) ⟼ \{p \in (ℝ^{(1 \dots N)}) \| \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)\})$
35		eqid	$⊢ {Base}_{𝔼_{𝒢} (N)} = {Base}_{𝔼_{𝒢} (N)}$
36		eqid	$⊢ (1 \dots N) = (1 \dots N)$
37	35 36	elntg2	$⊢ N \in ℕ \to {Line}_{𝒢} (𝔼_{𝒢} (N)) = (x \in {Base}_{𝔼_{𝒢} (N)}, y \in ({Base}_{𝔼_{𝒢} (N)} ∖ \{x\}) ⟼ \{p \in {Base}_{𝔼_{𝒢} (N)} \| (\exists z \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - z) x (i) + z y (i) \lor \exists v \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - v) p (i) + v y (i) \lor \exists w \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - w) x (i) + w p (i))\})$
38		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
39		eqid	$⊢ 𝔼_{hil} (N) = 𝔼_{hil} (N)$
40	39	ehlval	$⊢ N \in ℕ_{0} \to 𝔼_{hil} (N) = (1 \dots N)$
41	38 40	syl	$⊢ N \in ℕ \to 𝔼_{hil} (N) = (1 \dots N)$
42	41	fveq2d	$⊢ N \in ℕ \to {Line}_{M} (𝔼_{hil} (N)) = {Line}_{M} ((1 \dots N))$
43		fzfid	$⊢ N \in ℕ \to (1 \dots N) \in Fin$
44		eqid	$⊢ (1 \dots N) = (1 \dots N)$
45		eqid	$⊢ ℝ^{(1 \dots N)} = ℝ^{(1 \dots N)}$
46		eqid	$⊢ {Line}_{M} ((1 \dots N)) = {Line}_{M} ((1 \dots N))$
47	44 45 46	rrxlinesc	$⊢ (1 \dots N) \in Fin \to {Line}_{M} ((1 \dots N)) = (x \in (ℝ^{(1 \dots N)}), y \in ((ℝ^{(1 \dots N)}) ∖ \{x\}) ⟼ \{p \in (ℝ^{(1 \dots N)}) \| \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)\})$
48	43 47	syl	$⊢ N \in ℕ \to {Line}_{M} ((1 \dots N)) = (x \in (ℝ^{(1 \dots N)}), y \in ((ℝ^{(1 \dots N)}) ∖ \{x\}) ⟼ \{p \in (ℝ^{(1 \dots N)}) \| \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)\})$
49	42 48	eqtrd	$⊢ N \in ℕ \to {Line}_{M} (𝔼_{hil} (N)) = (x \in (ℝ^{(1 \dots N)}), y \in ((ℝ^{(1 \dots N)}) ∖ \{x\}) ⟼ \{p \in (ℝ^{(1 \dots N)}) \| \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)\})$
50	34 37 49	3eqtr4d	$⊢ N \in ℕ \to {Line}_{𝒢} (𝔼_{𝒢} (N)) = {Line}_{M} (𝔼_{hil} (N))$

Metamath Proof Explorer

Theorem eenglngeehlnm

Proof