Metamath Proof Explorer

Theorem rrx2line

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2. (Contributed by AV, 22-Jan-2023) (Proof shortened by AV, 13-Feb-2023)

Ref Expression
Hypotheses rrx2line.i ⊢ 𝐼 = ( 0 ..^ 2 )
rrx2line.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
rrx2line.b ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
rrx2line.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
Assertion rrx2line ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 rrx2line.i ⊢ 𝐼 = ( 0 ..^ 2 )
2 rrx2line.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3 rrx2line.b ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4 rrx2line.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
5 fzofi ⊢ ( 0 ..^ 2 ) ∈ Fin
6 1 5 eqeltri ⊢ 𝐼 ∈ Fin
7 2 3 4 rrxlinec ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) } )
8 6 7 mpan ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) } )
9 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
10 1 9 eqtri ⊢ 𝐼 = { 0 , 1 }
11 10 a1i ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝐼 = { 0 , 1 } )
12 11 raleqdv ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ { 0 , 1 } ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ) )
13 c0ex ⊢ 0 ∈ V
14 1ex ⊢ 1 ∈ V
15 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑝 ‘ 𝑖 ) = ( 𝑝 ‘ 0 ) )
16 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑋 ‘ 𝑖 ) = ( 𝑋 ‘ 0 ) )
17 16 oveq2d ⊢ ( 𝑖 = 0 → ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) = ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) )
18 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 0 ) )
19 18 oveq2d ⊢ ( 𝑖 = 0 → ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) = ( 𝑡 · ( 𝑌 ‘ 0 ) ) )
20 17 19 oveq12d ⊢ ( 𝑖 = 0 → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) )
21 15 20 eqeq12d ⊢ ( 𝑖 = 0 → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ) )
22 fveq2 ⊢ ( 𝑖 = 1 → ( 𝑝 ‘ 𝑖 ) = ( 𝑝 ‘ 1 ) )
23 fveq2 ⊢ ( 𝑖 = 1 → ( 𝑋 ‘ 𝑖 ) = ( 𝑋 ‘ 1 ) )
24 23 oveq2d ⊢ ( 𝑖 = 1 → ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) = ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) )
25 fveq2 ⊢ ( 𝑖 = 1 → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 1 ) )
26 25 oveq2d ⊢ ( 𝑖 = 1 → ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) = ( 𝑡 · ( 𝑌 ‘ 1 ) ) )
27 24 26 oveq12d ⊢ ( 𝑖 = 1 → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) )
28 22 27 eqeq12d ⊢ ( 𝑖 = 1 → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) )
29 13 14 21 28 ralpr ⊢ ( ∀ 𝑖 ∈ { 0 , 1 } ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ↔ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) )
30 12 29 bitrdi ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ↔ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) ) )
31 30 rexbidva ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ↔ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) ) )
32 31 rabbidva ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) } = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) } )
33 8 32 eqtrd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) } )