Metamath Proof Explorer


Theorem eengtrkge

Description: The geometry structure for EE ^ N is a Euclidean geometry. (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Assertion eengtrkge N𝔼𝒢N𝒢TarskiE

Proof

Step Hyp Ref Expression
1 fvexd N𝔼𝒢NV
2 simpll NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NN
3 simprl NxBase𝔼𝒢NyBase𝔼𝒢NxBase𝔼𝒢N
4 eengbas N𝔼N=Base𝔼𝒢N
5 4 adantr NxBase𝔼𝒢NyBase𝔼𝒢N𝔼N=Base𝔼𝒢N
6 3 5 eleqtrrd NxBase𝔼𝒢NyBase𝔼𝒢Nx𝔼N
7 6 adantr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Nx𝔼N
8 simprr NxBase𝔼𝒢NyBase𝔼𝒢NyBase𝔼𝒢N
9 8 5 eleqtrrd NxBase𝔼𝒢NyBase𝔼𝒢Ny𝔼N
10 9 adantr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Ny𝔼N
11 3 adantr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NxBase𝔼𝒢N
12 8 adantr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NyBase𝔼𝒢N
13 simpr1 NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NzBase𝔼𝒢N
14 simpr3 NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NzBase𝔼𝒢N
15 4 adantr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢N𝔼N=Base𝔼𝒢N
16 14 15 eleqtrrd NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢Nz𝔼N
17 2 11 12 13 16 syl13anc NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Nz𝔼N
18 simpr2 NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NuBase𝔼𝒢N
19 4 ad2antrr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢N𝔼N=Base𝔼𝒢N
20 18 19 eleqtrrd NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Nu𝔼N
21 simpr3 NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NvBase𝔼𝒢N
22 21 19 eleqtrrd NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Nv𝔼N
23 axeuclid Nx𝔼Ny𝔼Nz𝔼Nu𝔼Nv𝔼NuBtwnxvuBtwnyzxua𝔼Nb𝔼NyBtwnxazBtwnxbvBtwnab
24 2 7 10 17 20 22 23 syl132anc NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NuBtwnxvuBtwnyzxua𝔼Nb𝔼NyBtwnxazBtwnxbvBtwnab
25 eqid Base𝔼𝒢N=Base𝔼𝒢N
26 eqid Itv𝔼𝒢N=Itv𝔼𝒢N
27 2 25 26 11 21 18 ebtwntg NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NuBtwnxvuxItv𝔼𝒢Nv
28 2 25 26 12 13 18 ebtwntg NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NuBtwnyzuyItv𝔼𝒢Nz
29 27 28 3anbi12d NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NuBtwnxvuBtwnyzxuuxItv𝔼𝒢NvuyItv𝔼𝒢Nzxu
30 19 adantr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼N𝔼N=Base𝔼𝒢N
31 2 ad2antrr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NN
32 11 ad2antrr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NxBase𝔼𝒢N
33 simpr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Na𝔼N
34 33 30 eleqtrd NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼NaBase𝔼𝒢N
35 34 adantr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NaBase𝔼𝒢N
36 12 ad2antrr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NyBase𝔼𝒢N
37 31 25 26 32 35 36 ebtwntg NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NyBtwnxayxItv𝔼𝒢Na
38 simpr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼Nb𝔼N
39 19 ad2antrr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼N𝔼N=Base𝔼𝒢N
40 38 39 eleqtrd NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NbBase𝔼𝒢N
41 13 ad2antrr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NzBase𝔼𝒢N
42 31 25 26 32 40 41 ebtwntg NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NzBtwnxbzxItv𝔼𝒢Nb
43 21 ad2antrr NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NvBase𝔼𝒢N
44 31 25 26 35 40 43 ebtwntg NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NvBtwnabvaItv𝔼𝒢Nb
45 37 42 44 3anbi123d NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NyBtwnxazBtwnxbvBtwnabyxItv𝔼𝒢NazxItv𝔼𝒢NbvaItv𝔼𝒢Nb
46 30 45 rexeqbidva NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NyBtwnxazBtwnxbvBtwnabbBase𝔼𝒢NyxItv𝔼𝒢NazxItv𝔼𝒢NbvaItv𝔼𝒢Nb
47 19 46 rexeqbidva NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢Na𝔼Nb𝔼NyBtwnxazBtwnxbvBtwnabaBase𝔼𝒢NbBase𝔼𝒢NyxItv𝔼𝒢NazxItv𝔼𝒢NbvaItv𝔼𝒢Nb
48 24 29 47 3imtr3d NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NuxItv𝔼𝒢NvuyItv𝔼𝒢NzxuaBase𝔼𝒢NbBase𝔼𝒢NyxItv𝔼𝒢NazxItv𝔼𝒢NbvaItv𝔼𝒢Nb
49 48 ralrimivvva NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NuxItv𝔼𝒢NvuyItv𝔼𝒢NzxuaBase𝔼𝒢NbBase𝔼𝒢NyxItv𝔼𝒢NazxItv𝔼𝒢NbvaItv𝔼𝒢Nb
50 49 ralrimivva NxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NuxItv𝔼𝒢NvuyItv𝔼𝒢NzxuaBase𝔼𝒢NbBase𝔼𝒢NyxItv𝔼𝒢NazxItv𝔼𝒢NbvaItv𝔼𝒢Nb
51 eqid dist𝔼𝒢N=dist𝔼𝒢N
52 25 51 26 istrkge 𝔼𝒢N𝒢TarskiE𝔼𝒢NVxBase𝔼𝒢NyBase𝔼𝒢NzBase𝔼𝒢NuBase𝔼𝒢NvBase𝔼𝒢NuxItv𝔼𝒢NvuyItv𝔼𝒢NzxuaBase𝔼𝒢NbBase𝔼𝒢NyxItv𝔼𝒢NazxItv𝔼𝒢NbvaItv𝔼𝒢Nb
53 1 50 52 sylanbrc N𝔼𝒢N𝒢TarskiE