Metamath Proof Explorer


Definition df-line

Description: Definition of 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
Assertion df-line LineM = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠𝑤 ) 𝑥 ) ( +g𝑤 ) ( 𝑡 ( ·𝑠𝑤 ) 𝑦 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cline LineM
1 vw 𝑤
2 cvv V
3 vx 𝑥
4 cbs Base
5 1 cv 𝑤
6 5 4 cfv ( Base ‘ 𝑤 )
7 vy 𝑦
8 3 cv 𝑥
9 8 csn { 𝑥 }
10 6 9 cdif ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } )
11 vp 𝑝
12 vt 𝑡
13 csca Scalar
14 5 13 cfv ( Scalar ‘ 𝑤 )
15 14 4 cfv ( Base ‘ ( Scalar ‘ 𝑤 ) )
16 11 cv 𝑝
17 cur 1r
18 14 17 cfv ( 1r ‘ ( Scalar ‘ 𝑤 ) )
19 csg -g
20 14 19 cfv ( -g ‘ ( Scalar ‘ 𝑤 ) )
21 12 cv 𝑡
22 18 21 20 co ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 )
23 cvsca ·𝑠
24 5 23 cfv ( ·𝑠𝑤 )
25 22 8 24 co ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠𝑤 ) 𝑥 )
26 cplusg +g
27 5 26 cfv ( +g𝑤 )
28 7 cv 𝑦
29 21 28 24 co ( 𝑡 ( ·𝑠𝑤 ) 𝑦 )
30 25 29 27 co ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠𝑤 ) 𝑥 ) ( +g𝑤 ) ( 𝑡 ( ·𝑠𝑤 ) 𝑦 ) )
31 16 30 wceq 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠𝑤 ) 𝑥 ) ( +g𝑤 ) ( 𝑡 ( ·𝑠𝑤 ) 𝑦 ) )
32 31 12 15 wrex 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠𝑤 ) 𝑥 ) ( +g𝑤 ) ( 𝑡 ( ·𝑠𝑤 ) 𝑦 ) )
33 32 11 6 crab { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠𝑤 ) 𝑥 ) ( +g𝑤 ) ( 𝑡 ( ·𝑠𝑤 ) 𝑦 ) ) }
34 3 7 6 10 33 cmpo ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠𝑤 ) 𝑥 ) ( +g𝑤 ) ( 𝑡 ( ·𝑠𝑤 ) 𝑦 ) ) } )
35 1 2 34 cmpt ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠𝑤 ) 𝑥 ) ( +g𝑤 ) ( 𝑡 ( ·𝑠𝑤 ) 𝑦 ) ) } ) )
36 0 35 wceq LineM = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠𝑤 ) 𝑥 ) ( +g𝑤 ) ( 𝑡 ( ·𝑠𝑤 ) 𝑦 ) ) } ) )