Theorem eengv 28995

Description: The value of the Euclidean geometry for dimension 𝑁. (Contributed by Thierry Arnoux, 15-Mar-2019.)

Assertion

Ref	Expression
eengv	⊢ (𝑁 ∈ ℕ → (EEG‘𝑁) = ({⟨(Base‘ndx), (𝔼‘𝑁)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}))

Distinct variable group:   𝑥,𝑖,𝑦,𝑧,𝑁

Proof of Theorem eengv

Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6905	. . . . 5 ⊢ (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
2	1	opeq2d 4879	. . . 4 ⊢ (𝑛 = 𝑁 → ⟨(Base‘ndx), (𝔼‘𝑛)⟩ = ⟨(Base‘ndx), (𝔼‘𝑁)⟩)
3	1	adantr 480	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ 𝑥 ∈ (𝔼‘𝑛)) → (𝔼‘𝑛) = (𝔼‘𝑁))
4		simpl 482	. . . . . . . 8 ⊢ ((𝑛 = 𝑁 ∧ (𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛))) → 𝑛 = 𝑁)
5	4	oveq2d 7448	. . . . . . 7 ⊢ ((𝑛 = 𝑁 ∧ (𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛))) → (1...𝑛) = (1...𝑁))
6	5	sumeq1d 15737	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ (𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛))) → Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))
7	1, 3, 6	mpoeq123dva 7508	. . . . 5 ⊢ (𝑛 = 𝑁 → (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)) = (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)))
8	7	opeq2d 4879	. . . 4 ⊢ (𝑛 = 𝑁 → ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩ = ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩)
9	2, 8	preq12d 4740	. . 3 ⊢ (𝑛 = 𝑁 → {⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} = {⟨(Base‘ndx), (𝔼‘𝑁)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩})
10	1	adantr 480	. . . . . . 7 ⊢ ((𝑛 = 𝑁 ∧ (𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛))) → (𝔼‘𝑛) = (𝔼‘𝑁))
11	10	rabeqdv 3451	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ (𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛))) → {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩} = {𝑧 ∈ (𝔼‘𝑁) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})
12	1, 3, 11	mpoeq123dva 7508	. . . . 5 ⊢ (𝑛 = 𝑁 → (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩}) = (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩}))
13	12	opeq2d 4879	. . . 4 ⊢ (𝑛 = 𝑁 → ⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩ = ⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩)
14	3	difeq1d 4124	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ 𝑥 ∈ (𝔼‘𝑛)) → ((𝔼‘𝑛) ∖ {𝑥}) = ((𝔼‘𝑁) ∖ {𝑥}))
15	1	rabeqdv 3451	. . . . . . 7 ⊢ (𝑛 = 𝑁 → {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)} = {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})
16	15	adantr 480	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ (𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}))) → {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)} = {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})
17	1, 14, 16	mpoeq123dva 7508	. . . . 5 ⊢ (𝑛 = 𝑁 → (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)}) = (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)}))
18	17	opeq2d 4879	. . . 4 ⊢ (𝑛 = 𝑁 → ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩ = ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩)
19	13, 18	preq12d 4740	. . 3 ⊢ (𝑛 = 𝑁 → {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩} = {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩})
20	9, 19	uneq12d 4168	. 2 ⊢ (𝑛 = 𝑁 → ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}) = ({⟨(Base‘ndx), (𝔼‘𝑁)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}))
21		df-eeng 28994	. 2 ⊢ EEG = (𝑛 ∈ ℕ ↦ ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}))
22		prex 5436	. . 3 ⊢ {⟨(Base‘ndx), (𝔼‘𝑁)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∈ V
23		prex 5436	. . 3 ⊢ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩} ∈ V
24	22, 23	unex 7765	. 2 ⊢ ({⟨(Base‘ndx), (𝔼‘𝑁)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}) ∈ V
25	20, 21, 24	fvmpt 7015	1 ⊢ (𝑁 ∈ ℕ → (EEG‘𝑁) = ({⟨(Base‘ndx), (𝔼‘𝑁)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}))

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085   = wceq 1539   ∈ wcel 2107  {crab 3435   ∖ cdif 3947   ∪ cun 3948  {csn 4625  {cpr 4627  ⟨cop 4631   class class class wbr 5142  ‘cfv 6560  (class class class)co 7432   ∈ cmpo 7434  1c1 11157   − cmin 11493  ℕcn 12267  2c2 12322  ...cfz 13548  ↑cexp 14103  Σcsu 15723  ndxcnx 17231  Basecbs 17248  distcds 17307  Itvcitv 28442  LineGclng 28443  𝔼cee 28904   Btwn cbtwn 28905  EEGceeng 28993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-iota 6513  df-fun 6562  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-seq 14044  df-sum 15724  df-eeng 28994

This theorem is referenced by:  eengstr  28996  eengbas  28997  ebtwntg  28998  ecgrtg  28999  elntg  29000