Metamath Proof Explorer


Theorem rrxlinesc

Description: Definition of lines passing through two different points in a generalized real Euclidean space of finite dimension, expressed by their coordinates. (Contributed by AV, 13-Feb-2023)

Ref Expression
Hypotheses rrxlinesc.e E = I
rrxlinesc.p P = I
rrxlinesc.l L = Line M E
Assertion rrxlinesc I Fin L = x P , y P x p P | t i I p i = 1 t x i + t y i

Proof

Step Hyp Ref Expression
1 rrxlinesc.e E = I
2 rrxlinesc.p P = I
3 rrxlinesc.l L = Line M E
4 eqid E = E
5 eqid + E = + E
6 1 2 3 4 5 rrxlines I Fin L = x P , y P x p P | t p = 1 t E x + E t E y
7 eqid Base E = Base E
8 simpll1 I Fin x P y P x p P t I Fin
9 1red I Fin x P y P x p P t 1
10 simpr I Fin x P y P x p P t t
11 9 10 resubcld I Fin x P y P x p P t 1 t
12 id I Fin I Fin
13 12 1 7 rrxbasefi I Fin Base E = I
14 2 13 eqtr4id I Fin P = Base E
15 14 eleq2d I Fin x P x Base E
16 15 biimpa I Fin x P x Base E
17 16 3adant3 I Fin x P y P x x Base E
18 17 ad2antrr I Fin x P y P x p P t x Base E
19 eldifi y P x y P
20 14 eleq2d I Fin y P y Base E
21 19 20 syl5ib I Fin y P x y Base E
22 21 a1d I Fin x P y P x y Base E
23 22 3imp I Fin x P y P x y Base E
24 23 ad2antrr I Fin x P y P x p P t y Base E
25 14 3ad2ant1 I Fin x P y P x P = Base E
26 25 eleq2d I Fin x P y P x p P p Base E
27 26 biimpa I Fin x P y P x p P p Base E
28 27 adantr I Fin x P y P x p P t p Base E
29 1 7 4 8 11 18 24 28 5 10 rrxplusgvscavalb I Fin x P y P x p P t p = 1 t E x + E t E y i I p i = 1 t x i + t y i
30 29 rexbidva I Fin x P y P x p P t p = 1 t E x + E t E y t i I p i = 1 t x i + t y i
31 30 rabbidva I Fin x P y P x p P | t p = 1 t E x + E t E y = p P | t i I p i = 1 t x i + t y i
32 31 mpoeq3dva I Fin x P , y P x p P | t p = 1 t E x + E t E y = x P , y P x p P | t i I p i = 1 t x i + t y i
33 6 32 eqtrd I Fin L = x P , y P x p P | t i I p i = 1 t x i + t y i