Metamath Proof Explorer


Theorem eengv

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

Ref Expression
Assertion eengv N𝔼𝒢N=Basendx𝔼Ndistndxx𝔼N,y𝔼Ni=1Nxiyi2Itvndxx𝔼N,y𝔼Nz𝔼N|zBtwnxyLine𝒢ndxx𝔼N,y𝔼Nxz𝔼N|zBtwnxyxBtwnzyyBtwnxz

Proof

Step Hyp Ref Expression
1 fveq2 n=N𝔼n=𝔼N
2 1 opeq2d n=NBasendx𝔼n=Basendx𝔼N
3 1 adantr n=Nx𝔼n𝔼n=𝔼N
4 simpl n=Nx𝔼ny𝔼nn=N
5 4 oveq2d n=Nx𝔼ny𝔼n1n=1N
6 5 sumeq1d n=Nx𝔼ny𝔼ni=1nxiyi2=i=1Nxiyi2
7 1 3 6 mpoeq123dva n=Nx𝔼n,y𝔼ni=1nxiyi2=x𝔼N,y𝔼Ni=1Nxiyi2
8 7 opeq2d n=Ndistndxx𝔼n,y𝔼ni=1nxiyi2=distndxx𝔼N,y𝔼Ni=1Nxiyi2
9 2 8 preq12d n=NBasendx𝔼ndistndxx𝔼n,y𝔼ni=1nxiyi2=Basendx𝔼Ndistndxx𝔼N,y𝔼Ni=1Nxiyi2
10 1 adantr n=Nx𝔼ny𝔼n𝔼n=𝔼N
11 10 rabeqdv n=Nx𝔼ny𝔼nz𝔼n|zBtwnxy=z𝔼N|zBtwnxy
12 1 3 11 mpoeq123dva n=Nx𝔼n,y𝔼nz𝔼n|zBtwnxy=x𝔼N,y𝔼Nz𝔼N|zBtwnxy
13 12 opeq2d n=NItvndxx𝔼n,y𝔼nz𝔼n|zBtwnxy=Itvndxx𝔼N,y𝔼Nz𝔼N|zBtwnxy
14 3 difeq1d n=Nx𝔼n𝔼nx=𝔼Nx
15 1 rabeqdv n=Nz𝔼n|zBtwnxyxBtwnzyyBtwnxz=z𝔼N|zBtwnxyxBtwnzyyBtwnxz
16 15 adantr n=Nx𝔼ny𝔼nxz𝔼n|zBtwnxyxBtwnzyyBtwnxz=z𝔼N|zBtwnxyxBtwnzyyBtwnxz
17 1 14 16 mpoeq123dva n=Nx𝔼n,y𝔼nxz𝔼n|zBtwnxyxBtwnzyyBtwnxz=x𝔼N,y𝔼Nxz𝔼N|zBtwnxyxBtwnzyyBtwnxz
18 17 opeq2d n=NLine𝒢ndxx𝔼n,y𝔼nxz𝔼n|zBtwnxyxBtwnzyyBtwnxz=Line𝒢ndxx𝔼N,y𝔼Nxz𝔼N|zBtwnxyxBtwnzyyBtwnxz
19 13 18 preq12d n=NItvndxx𝔼n,y𝔼nz𝔼n|zBtwnxyLine𝒢ndxx𝔼n,y𝔼nxz𝔼n|zBtwnxyxBtwnzyyBtwnxz=Itvndxx𝔼N,y𝔼Nz𝔼N|zBtwnxyLine𝒢ndxx𝔼N,y𝔼Nxz𝔼N|zBtwnxyxBtwnzyyBtwnxz
20 9 19 uneq12d n=NBasendx𝔼ndistndxx𝔼n,y𝔼ni=1nxiyi2Itvndxx𝔼n,y𝔼nz𝔼n|zBtwnxyLine𝒢ndxx𝔼n,y𝔼nxz𝔼n|zBtwnxyxBtwnzyyBtwnxz=Basendx𝔼Ndistndxx𝔼N,y𝔼Ni=1Nxiyi2Itvndxx𝔼N,y𝔼Nz𝔼N|zBtwnxyLine𝒢ndxx𝔼N,y𝔼Nxz𝔼N|zBtwnxyxBtwnzyyBtwnxz
21 df-eeng 𝔼𝒢=nBasendx𝔼ndistndxx𝔼n,y𝔼ni=1nxiyi2Itvndxx𝔼n,y𝔼nz𝔼n|zBtwnxyLine𝒢ndxx𝔼n,y𝔼nxz𝔼n|zBtwnxyxBtwnzyyBtwnxz
22 prex Basendx𝔼Ndistndxx𝔼N,y𝔼Ni=1Nxiyi2V
23 prex Itvndxx𝔼N,y𝔼Nz𝔼N|zBtwnxyLine𝒢ndxx𝔼N,y𝔼Nxz𝔼N|zBtwnxyxBtwnzyyBtwnxzV
24 22 23 unex Basendx𝔼Ndistndxx𝔼N,y𝔼Ni=1Nxiyi2Itvndxx𝔼N,y𝔼Nz𝔼N|zBtwnxyLine𝒢ndxx𝔼N,y𝔼Nxz𝔼N|zBtwnxyxBtwnzyyBtwnxzV
25 20 21 24 fvmpt N𝔼𝒢N=Basendx𝔼Ndistndxx𝔼N,y𝔼Ni=1Nxiyi2Itvndxx𝔼N,y𝔼Nz𝔼N|zBtwnxyLine𝒢ndxx𝔼N,y𝔼Nxz𝔼N|zBtwnxyxBtwnzyyBtwnxz