Metamath Proof Explorer


Theorem rrxlines

Description: Definition of lines passing through two different points in a generalized real Euclidean space of finite dimension. (Contributed by AV, 14-Jan-2023)

Ref Expression
Hypotheses rrxlines.e 𝐸 = ( ℝ^ ‘ 𝐼 )
rrxlines.p 𝑃 = ( ℝ ↑m 𝐼 )
rrxlines.l 𝐿 = ( LineM𝐸 )
rrxlines.m · = ( ·𝑠𝐸 )
rrxlines.a + = ( +g𝐸 )
Assertion rrxlines ( 𝐼 ∈ Fin → 𝐿 = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )

Proof

Step Hyp Ref Expression
1 rrxlines.e 𝐸 = ( ℝ^ ‘ 𝐼 )
2 rrxlines.p 𝑃 = ( ℝ ↑m 𝐼 )
3 rrxlines.l 𝐿 = ( LineM𝐸 )
4 rrxlines.m · = ( ·𝑠𝐸 )
5 rrxlines.a + = ( +g𝐸 )
6 1 fvexi 𝐸 ∈ V
7 eqid ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
8 eqid ( Scalar ‘ 𝐸 ) = ( Scalar ‘ 𝐸 )
9 eqid ( Base ‘ ( Scalar ‘ 𝐸 ) ) = ( Base ‘ ( Scalar ‘ 𝐸 ) )
10 eqid ( -g ‘ ( Scalar ‘ 𝐸 ) ) = ( -g ‘ ( Scalar ‘ 𝐸 ) )
11 eqid ( 1r ‘ ( Scalar ‘ 𝐸 ) ) = ( 1r ‘ ( Scalar ‘ 𝐸 ) )
12 7 3 8 9 4 5 10 11 lines ( 𝐸 ∈ V → 𝐿 = ( 𝑥 ∈ ( Base ‘ 𝐸 ) , 𝑦 ∈ ( ( Base ‘ 𝐸 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )
13 6 12 mp1i ( 𝐼 ∈ Fin → 𝐿 = ( 𝑥 ∈ ( Base ‘ 𝐸 ) , 𝑦 ∈ ( ( Base ‘ 𝐸 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )
14 id ( 𝐼 ∈ Fin → 𝐼 ∈ Fin )
15 14 1 7 rrxbasefi ( 𝐼 ∈ Fin → ( Base ‘ 𝐸 ) = ( ℝ ↑m 𝐼 ) )
16 15 2 eqtr4di ( 𝐼 ∈ Fin → ( Base ‘ 𝐸 ) = 𝑃 )
17 16 difeq1d ( 𝐼 ∈ Fin → ( ( Base ‘ 𝐸 ) ∖ { 𝑥 } ) = ( 𝑃 ∖ { 𝑥 } ) )
18 1 rrxsca ( 𝐼 ∈ Fin → ( Scalar ‘ 𝐸 ) = ℝfld )
19 18 fveq2d ( 𝐼 ∈ Fin → ( Base ‘ ( Scalar ‘ 𝐸 ) ) = ( Base ‘ ℝfld ) )
20 rebase ℝ = ( Base ‘ ℝfld )
21 19 20 eqtr4di ( 𝐼 ∈ Fin → ( Base ‘ ( Scalar ‘ 𝐸 ) ) = ℝ )
22 18 fveq2d ( 𝐼 ∈ Fin → ( 1r ‘ ( Scalar ‘ 𝐸 ) ) = ( 1r ‘ ℝfld ) )
23 re1r 1 = ( 1r ‘ ℝfld )
24 22 23 eqtr4di ( 𝐼 ∈ Fin → ( 1r ‘ ( Scalar ‘ 𝐸 ) ) = 1 )
25 24 oveq1d ( 𝐼 ∈ Fin → ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) = ( 1 ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) )
26 25 adantr ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) = ( 1 ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) )
27 18 fveq2d ( 𝐼 ∈ Fin → ( -g ‘ ( Scalar ‘ 𝐸 ) ) = ( -g ‘ ℝfld ) )
28 27 oveqd ( 𝐼 ∈ Fin → ( 1 ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) = ( 1 ( -g ‘ ℝfld ) 𝑡 ) )
29 28 adantr ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( 1 ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) = ( 1 ( -g ‘ ℝfld ) 𝑡 ) )
30 21 eleq2d ( 𝐼 ∈ Fin → ( 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ↔ 𝑡 ∈ ℝ ) )
31 1re 1 ∈ ℝ
32 eqid ( -g ‘ ℝfld ) = ( -g ‘ ℝfld )
33 32 resubgval ( ( 1 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 1 − 𝑡 ) = ( 1 ( -g ‘ ℝfld ) 𝑡 ) )
34 33 eqcomd ( ( 1 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 1 ( -g ‘ ℝfld ) 𝑡 ) = ( 1 − 𝑡 ) )
35 31 34 mpan ( 𝑡 ∈ ℝ → ( 1 ( -g ‘ ℝfld ) 𝑡 ) = ( 1 − 𝑡 ) )
36 30 35 syl6bi ( 𝐼 ∈ Fin → ( 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) → ( 1 ( -g ‘ ℝfld ) 𝑡 ) = ( 1 − 𝑡 ) ) )
37 36 imp ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( 1 ( -g ‘ ℝfld ) 𝑡 ) = ( 1 − 𝑡 ) )
38 26 29 37 3eqtrd ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) = ( 1 − 𝑡 ) )
39 38 oveq1d ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) = ( ( 1 − 𝑡 ) · 𝑥 ) )
40 39 oveq1d ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) )
41 40 eqeq2d ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ↔ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ) )
42 21 41 rexeqbidva ( 𝐼 ∈ Fin → ( ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ↔ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ) )
43 16 42 rabeqbidv ( 𝐼 ∈ Fin → { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } = { 𝑝𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } )
44 16 17 43 mpoeq123dv ( 𝐼 ∈ Fin → ( 𝑥 ∈ ( Base ‘ 𝐸 ) , 𝑦 ∈ ( ( Base ‘ 𝐸 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )
45 13 44 eqtrd ( 𝐼 ∈ Fin → 𝐿 = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )