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	⊢ 𝐼 = { 1 , 2 }
	rrx2linest2.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	rrx2linest2.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
	rrx2linest2.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
	rrx2linest2.a	⊢ 𝐴 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
	rrx2linest2.b	⊢ 𝐵 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
	rrx2linest2.c	⊢ 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
Assertion	elrrx2linest2	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐺 ∈ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐺 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝐺 ‘ 1 ) ) + ( 𝐵 · ( 𝐺 ‘ 2 ) ) ) = 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrx2linest2.i	⊢ 𝐼 = { 1 , 2 }
2		rrx2linest2.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3		rrx2linest2.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4		rrx2linest2.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
5		rrx2linest2.a	⊢ 𝐴 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
6		rrx2linest2.b	⊢ 𝐵 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
7		rrx2linest2.c	⊢ 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
8	1 2 3 4 5 6 7	rrx2linest2	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )
9	8	eleq2d	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐺 ∈ ( 𝑋 𝐿 𝑌 ) ↔ 𝐺 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ) )
10		fveq1	⊢ ( 𝑝 = 𝐺 → ( 𝑝 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
11	10	oveq2d	⊢ ( 𝑝 = 𝐺 → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 𝐴 · ( 𝐺 ‘ 1 ) ) )
12		fveq1	⊢ ( 𝑝 = 𝐺 → ( 𝑝 ‘ 2 ) = ( 𝐺 ‘ 2 ) )
13	12	oveq2d	⊢ ( 𝑝 = 𝐺 → ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( 𝐵 · ( 𝐺 ‘ 2 ) ) )
14	11 13	oveq12d	⊢ ( 𝑝 = 𝐺 → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐴 · ( 𝐺 ‘ 1 ) ) + ( 𝐵 · ( 𝐺 ‘ 2 ) ) ) )
15	14	eqeq1d	⊢ ( 𝑝 = 𝐺 → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( 𝐴 · ( 𝐺 ‘ 1 ) ) + ( 𝐵 · ( 𝐺 ‘ 2 ) ) ) = 𝐶 ) )
16	15	elrab	⊢ ( 𝐺 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } ↔ ( 𝐺 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝐺 ‘ 1 ) ) + ( 𝐵 · ( 𝐺 ‘ 2 ) ) ) = 𝐶 ) )
17	9 16	bitrdi	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐺 ∈ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐺 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝐺 ‘ 1 ) ) + ( 𝐵 · ( 𝐺 ‘ 2 ) ) ) = 𝐶 ) ) )