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 ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) } ) )