Metamath Proof Explorer


Theorem rrxlinec

Description: The line passing through the two different points X and Y in a generalized real Euclidean space of finite dimension, expressed by its coordinates. Remark: This proof is shorter and requires less distinct variables than the proof using rrxlinesc . (Contributed by AV, 13-Feb-2023)

Ref Expression
Hypotheses rrxlinesc.e E = I
rrxlinesc.p P = I
rrxlinesc.l L = Line M E
Assertion rrxlinec I Fin X P Y P X Y X L Y = 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 rrxline I Fin X P Y P X Y X L Y = p P | t p = 1 t E X + E t E Y
7 eqid Base E = Base E
8 simplll I Fin X P Y P X Y p P t I Fin
9 1red I Fin X P Y P X Y p P t 1
10 simpr I Fin X P Y P X Y p P t t
11 9 10 resubcld I Fin X P Y P X Y 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 biimpcd X P I Fin X Base E
17 16 3ad2ant1 X P Y P X Y I Fin X Base E
18 17 impcom I Fin X P Y P X Y X Base E
19 18 ad2antrr I Fin X P Y P X Y p P t X Base E
20 14 eleq2d I Fin Y P Y Base E
21 20 biimpcd Y P I Fin Y Base E
22 21 3ad2ant2 X P Y P X Y I Fin Y Base E
23 22 impcom I Fin X P Y P X Y Y Base E
24 23 ad2antrr I Fin X P Y P X Y p P t Y Base E
25 14 adantr I Fin X P Y P X Y P = Base E
26 25 eleq2d I Fin X P Y P X Y p P p Base E
27 26 biimpa I Fin X P Y P X Y p P p Base E
28 27 adantr I Fin X P Y P X Y p P t p Base E
29 1 7 4 8 11 19 24 28 5 10 rrxplusgvscavalb I Fin X P Y P X Y 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 Y 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 Y 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 6 31 eqtrd I Fin X P Y P X Y X L Y = p P | t i I p i = 1 t X i + t Y i