Metamath Proof Explorer


Theorem rrx2line

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2. (Contributed by AV, 22-Jan-2023) (Proof shortened by AV, 13-Feb-2023)

Ref Expression
Hypotheses rrx2line.i I = 1 2
rrx2line.e E = I
rrx2line.b P = I
rrx2line.l L = Line M E
Assertion rrx2line X P Y P X Y X L Y = p P | t p 1 = 1 t X 1 + t Y 1 p 2 = 1 t X 2 + t Y 2

Proof

Step Hyp Ref Expression
1 rrx2line.i I = 1 2
2 rrx2line.e E = I
3 rrx2line.b P = I
4 rrx2line.l L = Line M E
5 prfi 1 2 Fin
6 1 5 eqeltri I Fin
7 2 3 4 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
8 6 7 mpan X P Y P X Y X L Y = p P | t i I p i = 1 t X i + t Y i
9 1 a1i X P Y P X Y p P t I = 1 2
10 9 raleqdv X P Y P X Y p P t i I p i = 1 t X i + t Y i i 1 2 p i = 1 t X i + t Y i
11 1ex 1 V
12 2ex 2 V
13 fveq2 i = 1 p i = p 1
14 fveq2 i = 1 X i = X 1
15 14 oveq2d i = 1 1 t X i = 1 t X 1
16 fveq2 i = 1 Y i = Y 1
17 16 oveq2d i = 1 t Y i = t Y 1
18 15 17 oveq12d i = 1 1 t X i + t Y i = 1 t X 1 + t Y 1
19 13 18 eqeq12d i = 1 p i = 1 t X i + t Y i p 1 = 1 t X 1 + t Y 1
20 fveq2 i = 2 p i = p 2
21 fveq2 i = 2 X i = X 2
22 21 oveq2d i = 2 1 t X i = 1 t X 2
23 fveq2 i = 2 Y i = Y 2
24 23 oveq2d i = 2 t Y i = t Y 2
25 22 24 oveq12d i = 2 1 t X i + t Y i = 1 t X 2 + t Y 2
26 20 25 eqeq12d i = 2 p i = 1 t X i + t Y i p 2 = 1 t X 2 + t Y 2
27 11 12 19 26 ralpr i 1 2 p i = 1 t X i + t Y i p 1 = 1 t X 1 + t Y 1 p 2 = 1 t X 2 + t Y 2
28 10 27 bitrdi X P Y P X Y p P t i I p i = 1 t X i + t Y i p 1 = 1 t X 1 + t Y 1 p 2 = 1 t X 2 + t Y 2
29 28 rexbidva X P Y P X Y p P t i I p i = 1 t X i + t Y i t p 1 = 1 t X 1 + t Y 1 p 2 = 1 t X 2 + t Y 2
30 29 rabbidva X P Y P X Y p P | t i I p i = 1 t X i + t Y i = p P | t p 1 = 1 t X 1 + t Y 1 p 2 = 1 t X 2 + t Y 2
31 8 30 eqtrd X P Y P X Y X L Y = p P | t p 1 = 1 t X 1 + t Y 1 p 2 = 1 t X 2 + t Y 2