Metamath Proof Explorer


Theorem rrxlinec

Description: The line passing through the two different points X and Y in a generalized real Euclidean space of finite dimension, expressed by its coordinates. Remark: This proof is shorter and requires less distinct variables than the proof using rrxlinesc . (Contributed by AV, 13-Feb-2023)

Ref Expression
Hypotheses rrxlinesc.e 𝐸 = ( ℝ^ ‘ 𝐼 )
rrxlinesc.p 𝑃 = ( ℝ ↑m 𝐼 )
rrxlinesc.l 𝐿 = ( LineM𝐸 )
Assertion rrxlinec ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖𝐼 ( 𝑝𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋𝑖 ) ) + ( 𝑡 · ( 𝑌𝑖 ) ) ) } )

Proof

Step Hyp Ref Expression
1 rrxlinesc.e 𝐸 = ( ℝ^ ‘ 𝐼 )
2 rrxlinesc.p 𝑃 = ( ℝ ↑m 𝐼 )
3 rrxlinesc.l 𝐿 = ( LineM𝐸 )
4 eqid ( ·𝑠𝐸 ) = ( ·𝑠𝐸 )
5 eqid ( +g𝐸 ) = ( +g𝐸 )
6 1 2 3 4 5 rrxline ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠𝐸 ) 𝑋 ) ( +g𝐸 ) ( 𝑡 ( ·𝑠𝐸 ) 𝑌 ) ) } )
7 eqid ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
8 simplll ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) ∧ 𝑝𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝐼 ∈ Fin )
9 1red ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) ∧ 𝑝𝑃 ) ∧ 𝑡 ∈ ℝ ) → 1 ∈ ℝ )
10 simpr ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) ∧ 𝑝𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
11 9 10 resubcld ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) ∧ 𝑝𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( 1 − 𝑡 ) ∈ ℝ )
12 id ( 𝐼 ∈ Fin → 𝐼 ∈ Fin )
13 12 1 7 rrxbasefi ( 𝐼 ∈ Fin → ( Base ‘ 𝐸 ) = ( ℝ ↑m 𝐼 ) )
14 13 2 syl6reqr ( 𝐼 ∈ Fin → 𝑃 = ( Base ‘ 𝐸 ) )
15 14 eleq2d ( 𝐼 ∈ Fin → ( 𝑋𝑃𝑋 ∈ ( Base ‘ 𝐸 ) ) )
16 15 biimpcd ( 𝑋𝑃 → ( 𝐼 ∈ Fin → 𝑋 ∈ ( Base ‘ 𝐸 ) ) )
17 16 3ad2ant1 ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( 𝐼 ∈ Fin → 𝑋 ∈ ( Base ‘ 𝐸 ) ) )
18 17 impcom ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) → 𝑋 ∈ ( Base ‘ 𝐸 ) )
19 18 ad2antrr ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) ∧ 𝑝𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑋 ∈ ( Base ‘ 𝐸 ) )
20 14 eleq2d ( 𝐼 ∈ Fin → ( 𝑌𝑃𝑌 ∈ ( Base ‘ 𝐸 ) ) )
21 20 biimpcd ( 𝑌𝑃 → ( 𝐼 ∈ Fin → 𝑌 ∈ ( Base ‘ 𝐸 ) ) )
22 21 3ad2ant2 ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( 𝐼 ∈ Fin → 𝑌 ∈ ( Base ‘ 𝐸 ) ) )
23 22 impcom ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) → 𝑌 ∈ ( Base ‘ 𝐸 ) )
24 23 ad2antrr ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) ∧ 𝑝𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑌 ∈ ( Base ‘ 𝐸 ) )
25 14 adantr ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) → 𝑃 = ( Base ‘ 𝐸 ) )
26 25 eleq2d ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) → ( 𝑝𝑃𝑝 ∈ ( Base ‘ 𝐸 ) ) )
27 26 biimpa ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) ∧ 𝑝𝑃 ) → 𝑝 ∈ ( Base ‘ 𝐸 ) )
28 27 adantr ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) ∧ 𝑝𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑝 ∈ ( Base ‘ 𝐸 ) )
29 1 7 4 8 11 19 24 28 5 10 rrxplusgvscavalb ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) ∧ 𝑝𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠𝐸 ) 𝑋 ) ( +g𝐸 ) ( 𝑡 ( ·𝑠𝐸 ) 𝑌 ) ) ↔ ∀ 𝑖𝐼 ( 𝑝𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋𝑖 ) ) + ( 𝑡 · ( 𝑌𝑖 ) ) ) ) )
30 29 rexbidva ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) ∧ 𝑝𝑃 ) → ( ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠𝐸 ) 𝑋 ) ( +g𝐸 ) ( 𝑡 ( ·𝑠𝐸 ) 𝑌 ) ) ↔ ∃ 𝑡 ∈ ℝ ∀ 𝑖𝐼 ( 𝑝𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋𝑖 ) ) + ( 𝑡 · ( 𝑌𝑖 ) ) ) ) )
31 30 rabbidva ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) → { 𝑝𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠𝐸 ) 𝑋 ) ( +g𝐸 ) ( 𝑡 ( ·𝑠𝐸 ) 𝑌 ) ) } = { 𝑝𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖𝐼 ( 𝑝𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋𝑖 ) ) + ( 𝑡 · ( 𝑌𝑖 ) ) ) } )
32 6 31 eqtrd ( ( 𝐼 ∈ Fin ∧ ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖𝐼 ( 𝑝𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋𝑖 ) ) + ( 𝑡 · ( 𝑌𝑖 ) ) ) } )