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 biimtrdi ⊢ ( 𝐼 ∈ 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 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )