Metamath Proof Explorer


Theorem lines

Description: The lines passing through two different points in a left module (or any extended structure having a base set, an addition, and a scalar multiplication). (Contributed by AV, 14-Jan-2023)

Ref Expression
Hypotheses lines.b B = Base W
lines.l L = Line M W
lines.s S = Scalar W
lines.k K = Base S
lines.p · ˙ = W
lines.a + ˙ = + W
lines.m - ˙ = - S
lines.1 1 ˙ = 1 S
Assertion lines W V L = x B , y B x p B | t K p = 1 ˙ - ˙ t · ˙ x + ˙ t · ˙ y

Proof

Step Hyp Ref Expression
1 lines.b B = Base W
2 lines.l L = Line M W
3 lines.s S = Scalar W
4 lines.k K = Base S
5 lines.p · ˙ = W
6 lines.a + ˙ = + W
7 lines.m - ˙ = - S
8 lines.1 1 ˙ = 1 S
9 df-line Line M = w V x Base w , y Base w x p Base w | t Base Scalar w p = 1 Scalar w - Scalar w t w x + w t w y
10 fveq2 W = w Base W = Base w
11 1 10 syl5eq W = w B = Base w
12 11 difeq1d W = w B x = Base w x
13 fveq2 W = w Scalar W = Scalar w
14 3 13 syl5eq W = w S = Scalar w
15 14 fveq2d W = w Base S = Base Scalar w
16 4 15 syl5eq W = w K = Base Scalar w
17 fveq2 W = w + W = + w
18 6 17 syl5eq W = w + ˙ = + w
19 fveq2 W = w W = w
20 5 19 syl5eq W = w · ˙ = w
21 3 fveq2i - S = - Scalar W
22 7 21 eqtri - ˙ = - Scalar W
23 2fveq3 W = w - Scalar W = - Scalar w
24 22 23 syl5eq W = w - ˙ = - Scalar w
25 3 fveq2i 1 S = 1 Scalar W
26 8 25 eqtri 1 ˙ = 1 Scalar W
27 2fveq3 W = w 1 Scalar W = 1 Scalar w
28 26 27 syl5eq W = w 1 ˙ = 1 Scalar w
29 eqidd W = w t = t
30 24 28 29 oveq123d W = w 1 ˙ - ˙ t = 1 Scalar w - Scalar w t
31 eqidd W = w x = x
32 20 30 31 oveq123d W = w 1 ˙ - ˙ t · ˙ x = 1 Scalar w - Scalar w t w x
33 20 oveqd W = w t · ˙ y = t w y
34 18 32 33 oveq123d W = w 1 ˙ - ˙ t · ˙ x + ˙ t · ˙ y = 1 Scalar w - Scalar w t w x + w t w y
35 34 eqeq2d W = w p = 1 ˙ - ˙ t · ˙ x + ˙ t · ˙ y p = 1 Scalar w - Scalar w t w x + w t w y
36 16 35 rexeqbidv W = w t K p = 1 ˙ - ˙ t · ˙ x + ˙ t · ˙ y t Base Scalar w p = 1 Scalar w - Scalar w t w x + w t w y
37 11 36 rabeqbidv W = w p B | t K p = 1 ˙ - ˙ t · ˙ x + ˙ t · ˙ y = p Base w | t Base Scalar w p = 1 Scalar w - Scalar w t w x + w t w y
38 11 12 37 mpoeq123dv W = w x B , y B x p B | t K p = 1 ˙ - ˙ t · ˙ x + ˙ t · ˙ y = x Base w , y Base w x p Base w | t Base Scalar w p = 1 Scalar w - Scalar w t w x + w t w y
39 38 eqcomd W = w x Base w , y Base w x p Base w | t Base Scalar w p = 1 Scalar w - Scalar w t w x + w t w y = x B , y B x p B | t K p = 1 ˙ - ˙ t · ˙ x + ˙ t · ˙ y
40 39 eqcoms w = W x Base w , y Base w x p Base w | t Base Scalar w p = 1 Scalar w - Scalar w t w x + w t w y = x B , y B x p B | t K p = 1 ˙ - ˙ t · ˙ x + ˙ t · ˙ y
41 elex W V W V
42 1 fvexi B V
43 42 difexi B x V
44 42 43 mpoex x B , y B x p B | t K p = 1 ˙ - ˙ t · ˙ x + ˙ t · ˙ y V
45 44 a1i W V x B , y B x p B | t K p = 1 ˙ - ˙ t · ˙ x + ˙ t · ˙ y V
46 9 40 41 45 fvmptd3 W V Line M W = x B , y B x p B | t K p = 1 ˙ - ˙ t · ˙ x + ˙ t · ˙ y
47 2 46 syl5eq W V L = x B , y B x p B | t K p = 1 ˙ - ˙ t · ˙ x + ˙ t · ˙ y