Theorem line

Description: The line passing through the two different points X and Y 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	line	⊢ ( ( 𝑊 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 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	1 2 3 4 5 6 7 8	lines	⊢ ( 𝑊 ∈ 𝑉 → 𝐿 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )
10	9	oveqd	⊢ ( 𝑊 ∈ 𝑉 → ( 𝑋 𝐿 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) 𝑌 ) )
11	10	adantr	⊢ ( ( 𝑊 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) 𝑌 ) )
12		eqidd	⊢ ( ( 𝑊 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )
13		oveq2	⊢ ( 𝑥 = 𝑋 → ( ( 1 − 𝑡 ) · 𝑥 ) = ( ( 1 − 𝑡 ) · 𝑋 ) )
14		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑡 · 𝑦 ) = ( 𝑡 · 𝑌 ) )
15	13 14	oveqan12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) )
16	15	eqeq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ↔ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) ) )
17	16	rexbidv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ↔ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) ) )
18	17	rabbidv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } = { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } )
19	18	adantl	⊢ ( ( ( 𝑊 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } = { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } )
20		sneq	⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
21	20	difeq2d	⊢ ( 𝑥 = 𝑋 → ( 𝐵 ∖ { 𝑥 } ) = ( 𝐵 ∖ { 𝑋 } ) )
22	21	adantl	⊢ ( ( ( 𝑊 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑥 = 𝑋 ) → ( 𝐵 ∖ { 𝑥 } ) = ( 𝐵 ∖ { 𝑋 } ) )
23		simpr1	⊢ ( ( 𝑊 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑋 ∈ 𝐵 )
24		id	⊢ ( 𝑋 ≠ 𝑌 → 𝑋 ≠ 𝑌 )
25	24	necomd	⊢ ( 𝑋 ≠ 𝑌 → 𝑌 ≠ 𝑋 )
26	25	anim2i	⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 𝑋 ) )
27	26	3adant1	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 𝑋 ) )
28		eldifsn	⊢ ( 𝑌 ∈ ( 𝐵 ∖ { 𝑋 } ) ↔ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 𝑋 ) )
29	27 28	sylibr	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ ( 𝐵 ∖ { 𝑋 } ) )
30	29	adantl	⊢ ( ( 𝑊 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑌 ∈ ( 𝐵 ∖ { 𝑋 } ) )
31	1	fvexi	⊢ 𝐵 ∈ V
32	31	rabex	⊢ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } ∈ V
33	32	a1i	⊢ ( ( 𝑊 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } ∈ V )
34	12 19 22 23 30 33	ovmpodx	⊢ ( ( 𝑊 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) 𝑌 ) = { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } )
35	11 34	eqtrd	⊢ ( ( 𝑊 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } )