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	$$⊢B={\mathrm{Base}}_W$$
	lines.l	$$⊢L={Line}_M\left(W\right)$$
	lines.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
	lines.k	$$⊢K={\mathrm{Base}}_S$$
	lines.p	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lines.a	$$⊢\underset{\dot{}}{+}={+}_W$$
	lines.m	$$⊢\underset{\dot{}}{-}={-}_S$$
	lines.1	$$⊢\underset{\dot{}}{1}=1_S$$
Assertion	line	$$⊢\left(W\in V\wedge \left(X\in B\wedge Y\in B\wedge X\ne Y\right)\right)\to XLY=\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}Y\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lines.b	$$⊢B={\mathrm{Base}}_W$$
2		lines.l	$$⊢L={Line}_M\left(W\right)$$
3		lines.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
4		lines.k	$$⊢K={\mathrm{Base}}_S$$
5		lines.p	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		lines.a	$$⊢\underset{\dot{}}{+}={+}_W$$
7		lines.m	$$⊢\underset{\dot{}}{-}={-}_S$$
8		lines.1	$$⊢\underset{\dot{}}{1}=1_S$$
9	1 2 3 4 5 6 7 8	lines	$$⊢W\in V\to L=\left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)$$
10	9	oveqd	$$⊢W\in V\to XLY=X\left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)Y$$
11	10	adantr	$$⊢\left(W\in V\wedge \left(X\in B\wedge Y\in B\wedge X\ne Y\right)\right)\to XLY=X\left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)Y$$
12		eqidd	$$⊢\left(W\in V\wedge \left(X\in B\wedge Y\in B\wedge X\ne Y\right)\right)\to \left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)=\left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)$$
13		oveq2	$$⊢x=X\to \left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x=\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}X$$
14		oveq2	$$⊢y=Y\to t\underset{\dot{}}{·}y=t\underset{\dot{}}{·}Y$$
15	13 14	oveqan12d	$$⊢\left(x=X\wedge y=Y\right)\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}Y\right)$$
16	15	eqeq2d	$$⊢\left(x=X\wedge y=Y\right)\to \left(p=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\leftrightarrow p=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}Y\right)\right)$$
17	16	rexbidv	$$⊢\left(x=X\wedge y=Y\right)\to \left(\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\leftrightarrow \exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}Y\right)\right)$$
18	17	rabbidv	$$⊢\left(x=X\wedge y=Y\right)\to \left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}=\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}Y\right)\right\}$$
19	18	adantl	$$⊢\left(\left(W\in V\wedge \left(X\in B\wedge Y\in B\wedge X\ne Y\right)\right)\wedge \left(x=X\wedge y=Y\right)\right)\to \left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}=\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}Y\right)\right\}$$
20		sneq	$$⊢x=X\to \left\{x\right\}=\left\{X\right\}$$
21	20	difeq2d	$$⊢x=X\to B\setminus \left\{x\right\}=B\setminus \left\{X\right\}$$
22	21	adantl	$$⊢\left(\left(W\in V\wedge \left(X\in B\wedge Y\in B\wedge X\ne Y\right)\right)\wedge x=X\right)\to B\setminus \left\{x\right\}=B\setminus \left\{X\right\}$$
23		simpr1	$$⊢\left(W\in V\wedge \left(X\in B\wedge Y\in B\wedge X\ne Y\right)\right)\to X\in B$$
24		id	$$⊢X\ne Y\to X\ne Y$$
25	24	necomd	$$⊢X\ne Y\to Y\ne X$$
26	25	anim2i	$$⊢\left(Y\in B\wedge X\ne Y\right)\to \left(Y\in B\wedge Y\ne X\right)$$
27	26	3adant1	$$⊢\left(X\in B\wedge Y\in B\wedge X\ne Y\right)\to \left(Y\in B\wedge Y\ne X\right)$$
28		eldifsn	$$⊢Y\in \left(B\setminus \left\{X\right\}\right)\leftrightarrow \left(Y\in B\wedge Y\ne X\right)$$
29	27 28	sylibr	$$⊢\left(X\in B\wedge Y\in B\wedge X\ne Y\right)\to Y\in \left(B\setminus \left\{X\right\}\right)$$
30	29	adantl	$$⊢\left(W\in V\wedge \left(X\in B\wedge Y\in B\wedge X\ne Y\right)\right)\to Y\in \left(B\setminus \left\{X\right\}\right)$$
31	1	fvexi	$$⊢B\in \mathrm{V}$$
32	31	rabex	$$⊢\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}Y\right)\right\}\in \mathrm{V}$$
33	32	a1i	$$⊢\left(W\in V\wedge \left(X\in B\wedge Y\in B\wedge X\ne Y\right)\right)\to \left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}Y\right)\right\}\in \mathrm{V}$$
34	12 19 22 23 30 33	ovmpodx	$$⊢\left(W\in V\wedge \left(X\in B\wedge Y\in B\wedge X\ne Y\right)\right)\to X\left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)Y=\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}Y\right)\right\}$$
35	11 34	eqtrd	$$⊢\left(W\in V\wedge \left(X\in B\wedge Y\in B\wedge X\ne Y\right)\right)\to XLY=\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}Y\right)\right\}$$