rrx2linesl

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2, expressed by the slope S between the two points ("point-slope form"), sometimes also written as ( ( p2 ) - ( X2 ) ) = ( S x. ( ( p1 ) - ( X1 ) ) ) . (Contributed by AV, 22-Jan-2023)

	Ref	Expression
Hypotheses	rrx2line.i	\|- I = { 1 , 2 }
	rrx2line.e	\|- E = ( RR^ ` I )
	rrx2line.b	\|- P = ( RR ^m I )
	rrx2line.l	\|- L = ( LineM ` E )
	rrx2linesl.s	\|- S = ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) )
Assertion	rrx2linesl	\|- ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X L Y ) = { p e. P \| ( p ` 2 ) = ( ( S x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		rrx2line.i	\|- I = { 1 , 2 }
2		rrx2line.e	\|- E = ( RR^ ` I )
3		rrx2line.b	\|- P = ( RR ^m I )
4		rrx2line.l	\|- L = ( LineM ` E )
5		rrx2linesl.s	\|- S = ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) )
6		fveq1	\|- ( X = Y -> ( X ` 1 ) = ( Y ` 1 ) )
7	6	necon3i	\|- ( ( X ` 1 ) =/= ( Y ` 1 ) -> X =/= Y )
8	1 2 3 4	rrx2line	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P \| E. t e. RR ( ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) } )
9	7 8	syl3an3	\|- ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X L Y ) = { p e. P \| E. t e. RR ( ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) } )
10		reex	\|- RR e. _V
11		prex	\|- { 1 , 2 } e. _V
12	1 11	eqeltri	\|- I e. _V
13	10 12	elmap	\|- ( p e. ( RR ^m I ) <-> p : I --> RR )
14		id	\|- ( p : I --> RR -> p : I --> RR )
15		1ex	\|- 1 e. _V
16	15	prid1	\|- 1 e. { 1 , 2 }
17	16 1	eleqtrri	\|- 1 e. I
18	17	a1i	\|- ( p : I --> RR -> 1 e. I )
19	14 18	ffvelcdmd	\|- ( p : I --> RR -> ( p ` 1 ) e. RR )
20	13 19	sylbi	\|- ( p e. ( RR ^m I ) -> ( p ` 1 ) e. RR )
21	20 3	eleq2s	\|- ( p e. P -> ( p ` 1 ) e. RR )
22	21	adantl	\|- ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( p ` 1 ) e. RR )
23	10 12	elmap	\|- ( X e. ( RR ^m I ) <-> X : I --> RR )
24		id	\|- ( X : I --> RR -> X : I --> RR )
25	17	a1i	\|- ( X : I --> RR -> 1 e. I )
26	24 25	ffvelcdmd	\|- ( X : I --> RR -> ( X ` 1 ) e. RR )
27	23 26	sylbi	\|- ( X e. ( RR ^m I ) -> ( X ` 1 ) e. RR )
28	27 3	eleq2s	\|- ( X e. P -> ( X ` 1 ) e. RR )
29	28	3ad2ant1	\|- ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X ` 1 ) e. RR )
30	29	adantr	\|- ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( X ` 1 ) e. RR )
31	10 12	elmap	\|- ( Y e. ( RR ^m I ) <-> Y : I --> RR )
32		id	\|- ( Y : I --> RR -> Y : I --> RR )
33	17	a1i	\|- ( Y : I --> RR -> 1 e. I )
34	32 33	ffvelcdmd	\|- ( Y : I --> RR -> ( Y ` 1 ) e. RR )
35	31 34	sylbi	\|- ( Y e. ( RR ^m I ) -> ( Y ` 1 ) e. RR )
36	35 3	eleq2s	\|- ( Y e. P -> ( Y ` 1 ) e. RR )
37	36	3ad2ant2	\|- ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( Y ` 1 ) e. RR )
38	37	adantr	\|- ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( Y ` 1 ) e. RR )
39		simpl3	\|- ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( X ` 1 ) =/= ( Y ` 1 ) )
40		2ex	\|- 2 e. _V
41	40	prid2	\|- 2 e. { 1 , 2 }
42	41 1	eleqtrri	\|- 2 e. I
43	42	a1i	\|- ( p : I --> RR -> 2 e. I )
44	14 43	ffvelcdmd	\|- ( p : I --> RR -> ( p ` 2 ) e. RR )
45	13 44	sylbi	\|- ( p e. ( RR ^m I ) -> ( p ` 2 ) e. RR )
46	45 3	eleq2s	\|- ( p e. P -> ( p ` 2 ) e. RR )
47	46	adantl	\|- ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( p ` 2 ) e. RR )
48	42	a1i	\|- ( X : I --> RR -> 2 e. I )
49	24 48	ffvelcdmd	\|- ( X : I --> RR -> ( X ` 2 ) e. RR )
50	23 49	sylbi	\|- ( X e. ( RR ^m I ) -> ( X ` 2 ) e. RR )
51	50 3	eleq2s	\|- ( X e. P -> ( X ` 2 ) e. RR )
52	51	3ad2ant1	\|- ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X ` 2 ) e. RR )
53	52	adantr	\|- ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( X ` 2 ) e. RR )
54	3	eleq2i	\|- ( Y e. P <-> Y e. ( RR ^m I ) )
55	54 31	bitri	\|- ( Y e. P <-> Y : I --> RR )
56	42	a1i	\|- ( Y : I --> RR -> 2 e. I )
57	32 56	ffvelcdmd	\|- ( Y : I --> RR -> ( Y ` 2 ) e. RR )
58	55 57	sylbi	\|- ( Y e. P -> ( Y ` 2 ) e. RR )
59	58	3ad2ant2	\|- ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( Y ` 2 ) e. RR )
60	59	adantr	\|- ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( Y ` 2 ) e. RR )
61	22 30 38 39 47 53 60 5	affinecomb1	\|- ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( E. t e. RR ( ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) <-> ( p ` 2 ) = ( ( S x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) ) )
62	61	rabbidva	\|- ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> { p e. P \| E. t e. RR ( ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) } = { p e. P \| ( p ` 2 ) = ( ( S x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) } )
63	9 62	eqtrd	\|- ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X L Y ) = { p e. P \| ( p ` 2 ) = ( ( S x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) } )

Metamath Proof Explorer

Theorem rrx2linesl

Proof