Metamath Proof Explorer


Theorem elntg2

Description: The line definition in the Tarski structure for the Euclidean geometry. In contrast to elntg , the betweenness can be strengthened by excluding 1 resp. 0 from the related intervals (because of x =/= y ). (Contributed by AV, 14-Feb-2023)

Ref Expression
Hypotheses elntg2.1 P = Base 𝔼 𝒢 N
elntg2.2 I = 1 N
Assertion elntg2 N Line 𝒢 𝔼 𝒢 N = x P , y P x p P | k 0 1 i I p i = 1 k x i + k y i l 0 1 i I x i = 1 l p i + l y i m 0 1 i I y i = 1 m x i + m p i

Proof

Step Hyp Ref Expression
1 elntg2.1 P = Base 𝔼 𝒢 N
2 elntg2.2 I = 1 N
3 eqid Itv 𝔼 𝒢 N = Itv 𝔼 𝒢 N
4 1 3 elntg N Line 𝒢 𝔼 𝒢 N = x P , y P x p P | p x Itv 𝔼 𝒢 N y x p Itv 𝔼 𝒢 N y y x Itv 𝔼 𝒢 N p
5 simpl1 N x P y P x p P N
6 simpl2 N x P y P x p P x P
7 eldifi y P x y P
8 7 3ad2ant3 N x P y P x y P
9 8 adantr N x P y P x p P y P
10 simpr N x P y P x p P p P
11 5 1 3 6 9 10 ebtwntg N x P y P x p P p Btwn x y p x Itv 𝔼 𝒢 N y
12 eengbas N 𝔼 N = Base 𝔼 𝒢 N
13 1 12 eqtr4id N P = 𝔼 N
14 13 3ad2ant1 N x P y P x P = 𝔼 N
15 14 eleq2d N x P y P x p P p 𝔼 N
16 15 biimpa N x P y P x p P p 𝔼 N
17 13 eleq2d N x P x 𝔼 N
18 17 biimpa N x P x 𝔼 N
19 18 3adant3 N x P y P x x 𝔼 N
20 19 adantr N x P y P x p P x 𝔼 N
21 13 eleq2d N y P y 𝔼 N
22 21 biimpcd y P N y 𝔼 N
23 22 7 syl11 N y P x y 𝔼 N
24 23 a1d N x P y P x y 𝔼 N
25 24 3imp N x P y P x y 𝔼 N
26 25 adantr N x P y P x p P y 𝔼 N
27 brbtwn p 𝔼 N x 𝔼 N y 𝔼 N p Btwn x y k 0 1 i 1 N p i = 1 k x i + k y i
28 16 20 26 27 syl3anc N x P y P x p P p Btwn x y k 0 1 i 1 N p i = 1 k x i + k y i
29 2 raleqi i I p i = 1 k x i + k y i i 1 N p i = 1 k x i + k y i
30 29 rexbii k 0 1 i I p i = 1 k x i + k y i k 0 1 i 1 N p i = 1 k x i + k y i
31 28 30 bitr4di N x P y P x p P p Btwn x y k 0 1 i I p i = 1 k x i + k y i
32 11 31 bitr3d N x P y P x p P p x Itv 𝔼 𝒢 N y k 0 1 i I p i = 1 k x i + k y i
33 5 1 3 10 9 6 ebtwntg N x P y P x p P x Btwn p y x p Itv 𝔼 𝒢 N y
34 brbtwn x 𝔼 N p 𝔼 N y 𝔼 N x Btwn p y l 0 1 i 1 N x i = 1 l p i + l y i
35 20 16 26 34 syl3anc N x P y P x p P x Btwn p y l 0 1 i 1 N x i = 1 l p i + l y i
36 33 35 bitr3d N x P y P x p P x p Itv 𝔼 𝒢 N y l 0 1 i 1 N x i = 1 l p i + l y i
37 0xr 0 *
38 1xr 1 *
39 0le1 0 1
40 snunico 0 * 1 * 0 1 0 1 1 = 0 1
41 37 38 39 40 mp3an 0 1 1 = 0 1
42 41 eqcomi 0 1 = 0 1 1
43 42 a1i N x P y P x p P 0 1 = 0 1 1
44 43 rexeqdv N x P y P x p P l 0 1 i 1 N x i = 1 l p i + l y i l 0 1 1 i 1 N x i = 1 l p i + l y i
45 rexun l 0 1 1 i 1 N x i = 1 l p i + l y i l 0 1 i 1 N x i = 1 l p i + l y i l 1 i 1 N x i = 1 l p i + l y i
46 eldifsn y P x y P y x
47 elee N x 𝔼 N x : 1 N
48 ffn x : 1 N x Fn 1 N
49 47 48 syl6bi N x 𝔼 N x Fn 1 N
50 17 49 sylbid N x P x Fn 1 N
51 50 a1i y P N x P x Fn 1 N
52 51 3imp y P N x P x Fn 1 N
53 elee N y 𝔼 N y : 1 N
54 ffn y : 1 N y Fn 1 N
55 53 54 syl6bi N y 𝔼 N y Fn 1 N
56 21 55 sylbid N y P y Fn 1 N
57 56 a1i x P N y P y Fn 1 N
58 57 3imp31 y P N x P y Fn 1 N
59 eqfnfv x Fn 1 N y Fn 1 N x = y i 1 N x i = y i
60 52 58 59 syl2anc y P N x P x = y i 1 N x i = y i
61 60 biimprd y P N x P i 1 N x i = y i x = y
62 eqcom y = x x = y
63 61 62 syl6ibr y P N x P i 1 N x i = y i y = x
64 63 necon3ad y P N x P y x ¬ i 1 N x i = y i
65 64 3exp y P N x P y x ¬ i 1 N x i = y i
66 65 com24 y P y x x P N ¬ i 1 N x i = y i
67 66 imp y P y x x P N ¬ i 1 N x i = y i
68 46 67 sylbi y P x x P N ¬ i 1 N x i = y i
69 68 3imp31 N x P y P x ¬ i 1 N x i = y i
70 69 adantr N x P y P x p P ¬ i 1 N x i = y i
71 13 eleq2d N p P p 𝔼 N
72 elee N p 𝔼 N p : 1 N
73 72 biimpd N p 𝔼 N p : 1 N
74 71 73 sylbid N p P p : 1 N
75 74 3ad2ant1 N x P y P x p P p : 1 N
76 75 imp N x P y P x p P p : 1 N
77 76 ffvelrnda N x P y P x p P i 1 N p i
78 77 recnd N x P y P x p P i 1 N p i
79 78 mul02d N x P y P x p P i 1 N 0 p i = 0
80 22 53 mpbidi y P N y : 1 N
81 80 7 syl11 N y P x y : 1 N
82 81 a1d N x P y P x y : 1 N
83 82 3imp N x P y P x y : 1 N
84 83 adantr N x P y P x p P y : 1 N
85 84 ffvelrnda N x P y P x p P i 1 N y i
86 85 recnd N x P y P x p P i 1 N y i
87 86 mulid2d N x P y P x p P i 1 N 1 y i = y i
88 79 87 oveq12d N x P y P x p P i 1 N 0 p i + 1 y i = 0 + y i
89 86 addid2d N x P y P x p P i 1 N 0 + y i = y i
90 88 89 eqtrd N x P y P x p P i 1 N 0 p i + 1 y i = y i
91 90 eqeq2d N x P y P x p P i 1 N x i = 0 p i + 1 y i x i = y i
92 91 ralbidva N x P y P x p P i 1 N x i = 0 p i + 1 y i i 1 N x i = y i
93 70 92 mtbird N x P y P x p P ¬ i 1 N x i = 0 p i + 1 y i
94 1re 1
95 oveq2 l = 1 1 l = 1 1
96 95 oveq1d l = 1 1 l p i = 1 1 p i
97 1m1e0 1 1 = 0
98 97 oveq1i 1 1 p i = 0 p i
99 96 98 eqtrdi l = 1 1 l p i = 0 p i
100 oveq1 l = 1 l y i = 1 y i
101 99 100 oveq12d l = 1 1 l p i + l y i = 0 p i + 1 y i
102 101 eqeq2d l = 1 x i = 1 l p i + l y i x i = 0 p i + 1 y i
103 102 ralbidv l = 1 i 1 N x i = 1 l p i + l y i i 1 N x i = 0 p i + 1 y i
104 103 rexsng 1 l 1 i 1 N x i = 1 l p i + l y i i 1 N x i = 0 p i + 1 y i
105 94 104 ax-mp l 1 i 1 N x i = 1 l p i + l y i i 1 N x i = 0 p i + 1 y i
106 93 105 sylnibr N x P y P x p P ¬ l 1 i 1 N x i = 1 l p i + l y i
107 2 raleqi i I x i = 1 l p i + l y i i 1 N x i = 1 l p i + l y i
108 107 rexbii l 0 1 i I x i = 1 l p i + l y i l 0 1 i 1 N x i = 1 l p i + l y i
109 biorf ¬ l 1 i 1 N x i = 1 l p i + l y i l 0 1 i 1 N x i = 1 l p i + l y i l 1 i 1 N x i = 1 l p i + l y i l 0 1 i 1 N x i = 1 l p i + l y i
110 108 109 syl5bb ¬ l 1 i 1 N x i = 1 l p i + l y i l 0 1 i I x i = 1 l p i + l y i l 1 i 1 N x i = 1 l p i + l y i l 0 1 i 1 N x i = 1 l p i + l y i
111 106 110 syl N x P y P x p P l 0 1 i I x i = 1 l p i + l y i l 1 i 1 N x i = 1 l p i + l y i l 0 1 i 1 N x i = 1 l p i + l y i
112 orcom l 1 i 1 N x i = 1 l p i + l y i l 0 1 i 1 N x i = 1 l p i + l y i l 0 1 i 1 N x i = 1 l p i + l y i l 1 i 1 N x i = 1 l p i + l y i
113 111 112 bitr2di N x P y P x p P l 0 1 i 1 N x i = 1 l p i + l y i l 1 i 1 N x i = 1 l p i + l y i l 0 1 i I x i = 1 l p i + l y i
114 45 113 syl5bb N x P y P x p P l 0 1 1 i 1 N x i = 1 l p i + l y i l 0 1 i I x i = 1 l p i + l y i
115 36 44 114 3bitrd N x P y P x p P x p Itv 𝔼 𝒢 N y l 0 1 i I x i = 1 l p i + l y i
116 5 1 3 6 10 9 ebtwntg N x P y P x p P y Btwn x p y x Itv 𝔼 𝒢 N p
117 brbtwn y 𝔼 N x 𝔼 N p 𝔼 N y Btwn x p m 0 1 i 1 N y i = 1 m x i + m p i
118 26 20 16 117 syl3anc N x P y P x p P y Btwn x p m 0 1 i 1 N y i = 1 m x i + m p i
119 116 118 bitr3d N x P y P x p P y x Itv 𝔼 𝒢 N p m 0 1 i 1 N y i = 1 m x i + m p i
120 snunioc 0 * 1 * 0 1 0 0 1 = 0 1
121 37 38 39 120 mp3an 0 0 1 = 0 1
122 121 eqcomi 0 1 = 0 0 1
123 122 a1i N x P y P x p P 0 1 = 0 0 1
124 123 rexeqdv N x P y P x p P m 0 1 i 1 N y i = 1 m x i + m p i m 0 0 1 i 1 N y i = 1 m x i + m p i
125 rexun m 0 0 1 i 1 N y i = 1 m x i + m p i m 0 i 1 N y i = 1 m x i + m p i m 0 1 i 1 N y i = 1 m x i + m p i
126 eqcom x i = y i y i = x i
127 126 ralbii i 1 N x i = y i i 1 N y i = x i
128 70 127 sylnib N x P y P x p P ¬ i 1 N y i = x i
129 17 biimpd N x P x 𝔼 N
130 129 47 sylibd N x P x : 1 N
131 130 imp N x P x : 1 N
132 131 3adant3 N x P y P x x : 1 N
133 132 adantr N x P y P x p P x : 1 N
134 133 ffvelrnda N x P y P x p P i 1 N x i
135 134 recnd N x P y P x p P i 1 N x i
136 135 mulid2d N x P y P x p P i 1 N 1 x i = x i
137 136 79 oveq12d N x P y P x p P i 1 N 1 x i + 0 p i = x i + 0
138 135 addid1d N x P y P x p P i 1 N x i + 0 = x i
139 137 138 eqtrd N x P y P x p P i 1 N 1 x i + 0 p i = x i
140 139 eqeq2d N x P y P x p P i 1 N y i = 1 x i + 0 p i y i = x i
141 140 ralbidva N x P y P x p P i 1 N y i = 1 x i + 0 p i i 1 N y i = x i
142 128 141 mtbird N x P y P x p P ¬ i 1 N y i = 1 x i + 0 p i
143 0re 0
144 oveq2 m = 0 1 m = 1 0
145 144 oveq1d m = 0 1 m x i = 1 0 x i
146 1m0e1 1 0 = 1
147 146 oveq1i 1 0 x i = 1 x i
148 145 147 eqtrdi m = 0 1 m x i = 1 x i
149 oveq1 m = 0 m p i = 0 p i
150 148 149 oveq12d m = 0 1 m x i + m p i = 1 x i + 0 p i
151 150 eqeq2d m = 0 y i = 1 m x i + m p i y i = 1 x i + 0 p i
152 151 ralbidv m = 0 i 1 N y i = 1 m x i + m p i i 1 N y i = 1 x i + 0 p i
153 152 rexsng 0 m 0 i 1 N y i = 1 m x i + m p i i 1 N y i = 1 x i + 0 p i
154 143 153 ax-mp m 0 i 1 N y i = 1 m x i + m p i i 1 N y i = 1 x i + 0 p i
155 142 154 sylnibr N x P y P x p P ¬ m 0 i 1 N y i = 1 m x i + m p i
156 2 raleqi i I y i = 1 m x i + m p i i 1 N y i = 1 m x i + m p i
157 156 rexbii m 0 1 i I y i = 1 m x i + m p i m 0 1 i 1 N y i = 1 m x i + m p i
158 biorf ¬ m 0 i 1 N y i = 1 m x i + m p i m 0 1 i 1 N y i = 1 m x i + m p i m 0 i 1 N y i = 1 m x i + m p i m 0 1 i 1 N y i = 1 m x i + m p i
159 157 158 syl5bb ¬ m 0 i 1 N y i = 1 m x i + m p i m 0 1 i I y i = 1 m x i + m p i m 0 i 1 N y i = 1 m x i + m p i m 0 1 i 1 N y i = 1 m x i + m p i
160 155 159 syl N x P y P x p P m 0 1 i I y i = 1 m x i + m p i m 0 i 1 N y i = 1 m x i + m p i m 0 1 i 1 N y i = 1 m x i + m p i
161 125 160 bitr4id N x P y P x p P m 0 0 1 i 1 N y i = 1 m x i + m p i m 0 1 i I y i = 1 m x i + m p i
162 119 124 161 3bitrd N x P y P x p P y x Itv 𝔼 𝒢 N p m 0 1 i I y i = 1 m x i + m p i
163 32 115 162 3orbi123d N x P y P x p P p x Itv 𝔼 𝒢 N y x p Itv 𝔼 𝒢 N y y x Itv 𝔼 𝒢 N p k 0 1 i I p i = 1 k x i + k y i l 0 1 i I x i = 1 l p i + l y i m 0 1 i I y i = 1 m x i + m p i
164 163 rabbidva N x P y P x p P | p x Itv 𝔼 𝒢 N y x p Itv 𝔼 𝒢 N y y x Itv 𝔼 𝒢 N p = p P | k 0 1 i I p i = 1 k x i + k y i l 0 1 i I x i = 1 l p i + l y i m 0 1 i I y i = 1 m x i + m p i
165 164 mpoeq3dva N x P , y P x p P | p x Itv 𝔼 𝒢 N y x p Itv 𝔼 𝒢 N y y x Itv 𝔼 𝒢 N p = x P , y P x p P | k 0 1 i I p i = 1 k x i + k y i l 0 1 i I x i = 1 l p i + l y i m 0 1 i I y i = 1 m x i + m p i
166 4 165 eqtrd N Line 𝒢 𝔼 𝒢 N = x P , y P x p P | k 0 1 i I p i = 1 k x i + k y i l 0 1 i I x i = 1 l p i + l y i m 0 1 i I y i = 1 m x i + m p i