Theorem eengbas

Description: The Base of the Euclidean geometry. (Contributed by Thierry Arnoux, 15-Mar-2019)

	Ref	Expression
Assertion	eengbas	$$⊢N\in \mathbb{N}\to 𝔼\left(N\right)={\mathrm{Base}}_{{𝔼}_{𝒢}\left(N\right)}$$

Proof

Step	Hyp	Ref	Expression
1		eengstr	$$⊢N\in \mathbb{N}\to {𝔼}_{𝒢}\left(N\right)\mathrm{Struct}⟨1,17⟩$$
2		fvexd	$$⊢N\in \mathbb{N}\to 𝔼\left(N\right)\in \mathrm{V}$$
3		opex	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩\in \mathrm{V}$$
4	3	prid1	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩\in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\sum _{i=1}^N{\left(x\left(i\right)-y\left(i\right)\right)}^2\right)⟩\right\}$$
5		elun1	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩\in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\sum _{i=1}^N{\left(x\left(i\right)-y\left(i\right)\right)}^2\right)⟩\right\}\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩\in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\sum _{i=1}^N{\left(x\left(i\right)-y\left(i\right)\right)}^2\right)⟩\right\}\cup \left\{⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\left\{z\in 𝔼\left(N\right)|z\mathrm{Btwn}⟨x,y⟩\right\}\right)⟩,⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in \left(𝔼\left(N\right)\setminus \left\{x\right\}\right)⟼\left\{z\in 𝔼\left(N\right)|\left(z\mathrm{Btwn}⟨x,y⟩\vee x\mathrm{Btwn}⟨z,y⟩\vee y\mathrm{Btwn}⟨x,z⟩\right)\right\}\right)⟩\right\}\right)$$
6	4 5	ax-mp	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩\in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\sum _{i=1}^N{\left(x\left(i\right)-y\left(i\right)\right)}^2\right)⟩\right\}\cup \left\{⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\left\{z\in 𝔼\left(N\right)|z\mathrm{Btwn}⟨x,y⟩\right\}\right)⟩,⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in \left(𝔼\left(N\right)\setminus \left\{x\right\}\right)⟼\left\{z\in 𝔼\left(N\right)|\left(z\mathrm{Btwn}⟨x,y⟩\vee x\mathrm{Btwn}⟨z,y⟩\vee y\mathrm{Btwn}⟨x,z⟩\right)\right\}\right)⟩\right\}\right)$$
7		eengv	$$⊢N\in \mathbb{N}\to {𝔼}_{𝒢}\left(N\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\sum _{i=1}^N{\left(x\left(i\right)-y\left(i\right)\right)}^2\right)⟩\right\}\cup \left\{⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\left\{z\in 𝔼\left(N\right)|z\mathrm{Btwn}⟨x,y⟩\right\}\right)⟩,⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in \left(𝔼\left(N\right)\setminus \left\{x\right\}\right)⟼\left\{z\in 𝔼\left(N\right)|\left(z\mathrm{Btwn}⟨x,y⟩\vee x\mathrm{Btwn}⟨z,y⟩\vee y\mathrm{Btwn}⟨x,z⟩\right)\right\}\right)⟩\right\}$$
8	6 7	eleqtrrid	$$⊢N\in \mathbb{N}\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩\in {𝔼}_{𝒢}\left(N\right)$$
9	1 2 8	opelstrbas	$$⊢N\in \mathbb{N}\to 𝔼\left(N\right)={\mathrm{Base}}_{{𝔼}_{𝒢}\left(N\right)}$$