Theorem elrrx2linest2

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2 in another "standard form" (usually with ( p1 ) = x and ( p2 ) = y ). (Contributed by AV, 23-Feb-2023)

	Ref	Expression
Hypotheses	rrx2linest2.i	|- I = { 1 , 2 }
	rrx2linest2.e	|- E = ( RR^ ` I )
	rrx2linest2.p	|- P = ( RR ^m I )
	rrx2linest2.l	|- L = ( LineM ` E )
	rrx2linest2.a	|- A = ( ( X ` 2 ) - ( Y ` 2 ) )
	rrx2linest2.b	|- B = ( ( Y ` 1 ) - ( X ` 1 ) )
	rrx2linest2.c	|- C = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) )
Assertion	elrrx2linest2	|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( G e. ( X L Y ) <-> ( G e. P /\ ( ( A x. ( G ` 1 ) ) + ( B x. ( G ` 2 ) ) ) = C ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrx2linest2.i	|- I = { 1 , 2 }
2		rrx2linest2.e	|- E = ( RR^ ` I )
3		rrx2linest2.p	|- P = ( RR ^m I )
4		rrx2linest2.l	|- L = ( LineM ` E )
5		rrx2linest2.a	|- A = ( ( X ` 2 ) - ( Y ` 2 ) )
6		rrx2linest2.b	|- B = ( ( Y ` 1 ) - ( X ` 1 ) )
7		rrx2linest2.c	|- C = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) )
8	1 2 3 4 5 6 7	rrx2linest2	|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } )
9	8	eleq2d	|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( G e. ( X L Y ) <-> G e. { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } ) )
10		fveq1	|- ( p = G -> ( p ` 1 ) = ( G ` 1 ) )
11	10	oveq2d	|- ( p = G -> ( A x. ( p ` 1 ) ) = ( A x. ( G ` 1 ) ) )
12		fveq1	|- ( p = G -> ( p ` 2 ) = ( G ` 2 ) )
13	12	oveq2d	|- ( p = G -> ( B x. ( p ` 2 ) ) = ( B x. ( G ` 2 ) ) )
14	11 13	oveq12d	|- ( p = G -> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = ( ( A x. ( G ` 1 ) ) + ( B x. ( G ` 2 ) ) ) )
15	14	eqeq1d	|- ( p = G -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( ( A x. ( G ` 1 ) ) + ( B x. ( G ` 2 ) ) ) = C ) )
16	15	elrab	|- ( G e. { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } <-> ( G e. P /\ ( ( A x. ( G ` 1 ) ) + ( B x. ( G ` 2 ) ) ) = C ) )
17	9 16	bitrdi	|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( G e. ( X L Y ) <-> ( G e. P /\ ( ( A x. ( G ` 1 ) ) + ( B x. ( G ` 2 ) ) ) = C ) ) )