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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	lines.l	⊢ 𝐿 = ( LineM ‘ 𝑊 )
	lines.s	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
	lines.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	lines.p	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lines.a	⊢ + = ( +g ‘ 𝑊 )
	lines.m	⊢ − = ( -g ‘ 𝑆 )
	lines.1	⊢ 1 = ( 1r ‘ 𝑆 )
Assertion	lines	⊢ ( 𝑊 ∈ 𝑉 → 𝐿 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		lines.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		lines.l	⊢ 𝐿 = ( LineM ‘ 𝑊 )
3		lines.s	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
4		lines.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
5		lines.p	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		lines.a	⊢ + = ( +g ‘ 𝑊 )
7		lines.m	⊢ − = ( -g ‘ 𝑆 )
8		lines.1	⊢ 1 = ( 1r ‘ 𝑆 )
9		df-line	⊢ LineM = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) } ) )
10		fveq2	⊢ ( 𝑊 = 𝑤 → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑤 ) )
11	1 10	eqtrid	⊢ ( 𝑊 = 𝑤 → 𝐵 = ( Base ‘ 𝑤 ) )
12	11	difeq1d	⊢ ( 𝑊 = 𝑤 → ( 𝐵 ∖ { 𝑥 } ) = ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) )
13		fveq2	⊢ ( 𝑊 = 𝑤 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑤 ) )
14	3 13	eqtrid	⊢ ( 𝑊 = 𝑤 → 𝑆 = ( Scalar ‘ 𝑤 ) )
15	14	fveq2d	⊢ ( 𝑊 = 𝑤 → ( Base ‘ 𝑆 ) = ( Base ‘ ( Scalar ‘ 𝑤 ) ) )
16	4 15	eqtrid	⊢ ( 𝑊 = 𝑤 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑤 ) ) )
17		fveq2	⊢ ( 𝑊 = 𝑤 → ( +g ‘ 𝑊 ) = ( +g ‘ 𝑤 ) )
18	6 17	eqtrid	⊢ ( 𝑊 = 𝑤 → + = ( +g ‘ 𝑤 ) )
19		fveq2	⊢ ( 𝑊 = 𝑤 → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑤 ) )
20	5 19	eqtrid	⊢ ( 𝑊 = 𝑤 → · = ( ·𝑠 ‘ 𝑤 ) )
21	3	fveq2i	⊢ ( -g ‘ 𝑆 ) = ( -g ‘ ( Scalar ‘ 𝑊 ) )
22	7 21	eqtri	⊢ − = ( -g ‘ ( Scalar ‘ 𝑊 ) )
23		2fveq3	⊢ ( 𝑊 = 𝑤 → ( -g ‘ ( Scalar ‘ 𝑊 ) ) = ( -g ‘ ( Scalar ‘ 𝑤 ) ) )
24	22 23	eqtrid	⊢ ( 𝑊 = 𝑤 → − = ( -g ‘ ( Scalar ‘ 𝑤 ) ) )
25	3	fveq2i	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
26	8 25	eqtri	⊢ 1 = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
27		2fveq3	⊢ ( 𝑊 = 𝑤 → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑤 ) ) )
28	26 27	eqtrid	⊢ ( 𝑊 = 𝑤 → 1 = ( 1r ‘ ( Scalar ‘ 𝑤 ) ) )
29		eqidd	⊢ ( 𝑊 = 𝑤 → 𝑡 = 𝑡 )
30	24 28 29	oveq123d	⊢ ( 𝑊 = 𝑤 → ( 1 − 𝑡 ) = ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) )
31		eqidd	⊢ ( 𝑊 = 𝑤 → 𝑥 = 𝑥 )
32	20 30 31	oveq123d	⊢ ( 𝑊 = 𝑤 → ( ( 1 − 𝑡 ) · 𝑥 ) = ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) )
33	20	oveqd	⊢ ( 𝑊 = 𝑤 → ( 𝑡 · 𝑦 ) = ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) )
34	18 32 33	oveq123d	⊢ ( 𝑊 = 𝑤 → ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) )
35	34	eqeq2d	⊢ ( 𝑊 = 𝑤 → ( 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ↔ 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) ) )
36	16 35	rexeqbidv	⊢ ( 𝑊 = 𝑤 → ( ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ↔ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) ) )
37	11 36	rabeqbidv	⊢ ( 𝑊 = 𝑤 → { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } = { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) } )
38	11 12 37	mpoeq123dv	⊢ ( 𝑊 = 𝑤 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) } ) )
39	38	eqcomd	⊢ ( 𝑊 = 𝑤 → ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )
40	39	eqcoms	⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )
41		elex	⊢ ( 𝑊 ∈ 𝑉 → 𝑊 ∈ V )
42	1	fvexi	⊢ 𝐵 ∈ V
43	42	difexi	⊢ ( 𝐵 ∖ { 𝑥 } ) ∈ V
44	42 43	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) ∈ V
45	44	a1i	⊢ ( 𝑊 ∈ 𝑉 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) ∈ V )
46	9 40 41 45	fvmptd3	⊢ ( 𝑊 ∈ 𝑉 → ( LineM ‘ 𝑊 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )
47	2 46	eqtrid	⊢ ( 𝑊 ∈ 𝑉 → 𝐿 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )