Metamath Proof Explorer

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 ( p0 ) = x and ( p1 ) = y ). (Contributed by AV, 23-Feb-2023)

Ref Expression
Hypotheses rrx2linest2.i ⊢ I = 0 ..^ 2
rrx2linest2.e ⊢ E = I
rrx2linest2.p ⊢ P = ℝ I
rrx2linest2.l ⊢ L = Line M ⁡ E
rrx2linest2.a ⊢ A = X ⁡ 1 − Y ⁡ 1
rrx2linest2.b ⊢ B = Y ⁡ 0 − X ⁡ 0
rrx2linest2.c ⊢ C = X ⁡ 1 ⁢ Y ⁡ 0 − X ⁡ 0 ⁢ Y ⁡ 1
Assertion elrrx2linest2 ⊢ X ∈ P ∧ Y ∈ P ∧ X ≠ Y → G ∈ X L Y ↔ G ∈ P ∧ A ⁢ G ⁡ 0 + B ⁢ G ⁡ 1 = C

Proof

Step Hyp Ref Expression
1 rrx2linest2.i ⊢ I = 0 ..^ 2
2 rrx2linest2.e ⊢ E = I
3 rrx2linest2.p ⊢ P = ℝ I
4 rrx2linest2.l ⊢ L = Line M ⁡ E
5 rrx2linest2.a ⊢ A = X ⁡ 1 − Y ⁡ 1
6 rrx2linest2.b ⊢ B = Y ⁡ 0 − X ⁡ 0
7 rrx2linest2.c ⊢ C = X ⁡ 1 ⁢ Y ⁡ 0 − X ⁡ 0 ⁢ Y ⁡ 1
8 1 2 3 4 5 6 7 rrx2linest2 ⊢ X ∈ P ∧ Y ∈ P ∧ X ≠ Y → X L Y = p ∈ P | A ⁢ p ⁡ 0 + B ⁢ p ⁡ 1 = C
9 8 eleq2d ⊢ X ∈ P ∧ Y ∈ P ∧ X ≠ Y → G ∈ X L Y ↔ G ∈ p ∈ P | A ⁢ p ⁡ 0 + B ⁢ p ⁡ 1 = C
10 fveq1 ⊢ p = G → p ⁡ 0 = G ⁡ 0
11 10 oveq2d ⊢ p = G → A ⁢ p ⁡ 0 = A ⁢ G ⁡ 0
12 fveq1 ⊢ p = G → p ⁡ 1 = G ⁡ 1
13 12 oveq2d ⊢ p = G → B ⁢ p ⁡ 1 = B ⁢ G ⁡ 1
14 11 13 oveq12d ⊢ p = G → A ⁢ p ⁡ 0 + B ⁢ p ⁡ 1 = A ⁢ G ⁡ 0 + B ⁢ G ⁡ 1
15 14 eqeq1d ⊢ p = G → A ⁢ p ⁡ 0 + B ⁢ p ⁡ 1 = C ↔ A ⁢ G ⁡ 0 + B ⁢ G ⁡ 1 = C
16 15 elrab ⊢ G ∈ p ∈ P | A ⁢ p ⁡ 0 + B ⁢ p ⁡ 1 = C ↔ G ∈ P ∧ A ⁢ G ⁡ 0 + B ⁢ G ⁡ 1 = C
17 9 16 bitrdi ⊢ X ∈ P ∧ Y ∈ P ∧ X ≠ Y → G ∈ X L Y ↔ G ∈ P ∧ A ⁢ G ⁡ 0 + B ⁢ G ⁡ 1 = C