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 = ( Base ` W )
	lines.l	|- L = ( LineM ` W )
	lines.s	|- S = ( Scalar ` W )
	lines.k	|- K = ( Base ` S )
	lines.p	|- .x. = ( .s ` W )
	lines.a	|- .+ = ( +g ` W )
	lines.m	|- .- = ( -g ` S )
	lines.1	|- .1. = ( 1r ` S )
Assertion	line	|- ( ( W e. V /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> ( X L Y ) = { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. X ) .+ ( t .x. Y ) ) } )

Proof

Step	Hyp	Ref	Expression
1		lines.b	|- B = ( Base ` W )
2		lines.l	|- L = ( LineM ` W )
3		lines.s	|- S = ( Scalar ` W )
4		lines.k	|- K = ( Base ` S )
5		lines.p	|- .x. = ( .s ` W )
6		lines.a	|- .+ = ( +g ` W )
7		lines.m	|- .- = ( -g ` S )
8		lines.1	|- .1. = ( 1r ` S )
9	1 2 3 4 5 6 7 8	lines	|- ( W e. V -> L = ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) )
10	9	oveqd	|- ( W e. V -> ( X L Y ) = ( X ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) Y ) )
11	10	adantr	|- ( ( W e. V /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> ( X L Y ) = ( X ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) Y ) )
12		eqidd	|- ( ( W e. V /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) = ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) )
13		oveq2	|- ( x = X -> ( ( .1. .- t ) .x. x ) = ( ( .1. .- t ) .x. X ) )
14		oveq2	|- ( y = Y -> ( t .x. y ) = ( t .x. Y ) )
15	13 14	oveqan12d	|- ( ( x = X /\ y = Y ) -> ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) = ( ( ( .1. .- t ) .x. X ) .+ ( t .x. Y ) ) )
16	15	eqeq2d	|- ( ( x = X /\ y = Y ) -> ( p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) <-> p = ( ( ( .1. .- t ) .x. X ) .+ ( t .x. Y ) ) ) )
17	16	rexbidv	|- ( ( x = X /\ y = Y ) -> ( E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) <-> E. t e. K p = ( ( ( .1. .- t ) .x. X ) .+ ( t .x. Y ) ) ) )
18	17	rabbidv	|- ( ( x = X /\ y = Y ) -> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } = { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. X ) .+ ( t .x. Y ) ) } )
19	18	adantl	|- ( ( ( W e. V /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( x = X /\ y = Y ) ) -> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } = { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. X ) .+ ( t .x. Y ) ) } )
20		sneq	|- ( x = X -> { x } = { X } )
21	20	difeq2d	|- ( x = X -> ( B \ { x } ) = ( B \ { X } ) )
22	21	adantl	|- ( ( ( W e. V /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ x = X ) -> ( B \ { x } ) = ( B \ { X } ) )
23		simpr1	|- ( ( W e. V /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> X e. B )
24		id	|- ( X =/= Y -> X =/= Y )
25	24	necomd	|- ( X =/= Y -> Y =/= X )
26	25	anim2i	|- ( ( Y e. B /\ X =/= Y ) -> ( Y e. B /\ Y =/= X ) )
27	26	3adant1	|- ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( Y e. B /\ Y =/= X ) )
28		eldifsn	|- ( Y e. ( B \ { X } ) <-> ( Y e. B /\ Y =/= X ) )
29	27 28	sylibr	|- ( ( X e. B /\ Y e. B /\ X =/= Y ) -> Y e. ( B \ { X } ) )
30	29	adantl	|- ( ( W e. V /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> Y e. ( B \ { X } ) )
31	1	fvexi	|- B e. _V
32	31	rabex	|- { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. X ) .+ ( t .x. Y ) ) } e. _V
33	32	a1i	|- ( ( W e. V /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. X ) .+ ( t .x. Y ) ) } e. _V )
34	12 19 22 23 30 33	ovmpodx	|- ( ( W e. V /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> ( X ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) Y ) = { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. X ) .+ ( t .x. Y ) ) } )
35	11 34	eqtrd	|- ( ( W e. V /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> ( X L Y ) = { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. X ) .+ ( t .x. Y ) ) } )