This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rrndstprj1

Description: The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypotheses rrnval.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
rrndstprj1.1 ⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
Assertion rrndstprj1 ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )

Proof

Step Hyp Ref Expression
1 rrnval.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
2 rrndstprj1.1 ⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
3 simpll ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐼 ∈ Fin )
4 simprl ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐹 ∈ 𝑋 )
5 4 1 eleqtrdi ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐹 ∈ ( ℝ ↑m 𝐼 ) )
6 elmapi ⊢ ( 𝐹 ∈ ( ℝ ↑m 𝐼 ) → 𝐹 : 𝐼 ⟶ ℝ )
7 5 6 syl ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐹 : 𝐼 ⟶ ℝ )
8 7 ffvelcdmda ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
9 simprr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐺 ∈ 𝑋 )
10 9 1 eleqtrdi ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐺 ∈ ( ℝ ↑m 𝐼 ) )
11 elmapi ⊢ ( 𝐺 ∈ ( ℝ ↑m 𝐼 ) → 𝐺 : 𝐼 ⟶ ℝ )
12 10 11 syl ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐺 : 𝐼 ⟶ ℝ )
13 12 ffvelcdmda ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
14 8 13 resubcld ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
15 14 resqcld ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
16 14 sqge0d ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → 0 ≤ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
17 fveq2 ⊢ ( 𝑘 = 𝐴 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝐴 ) )
18 fveq2 ⊢ ( 𝑘 = 𝐴 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝐴 ) )
19 17 18 oveq12d ⊢ ( 𝑘 = 𝐴 → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) )
20 19 oveq1d ⊢ ( 𝑘 = 𝐴 → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ↑ 2 ) )
21 simplr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐴 ∈ 𝐼 )
22 3 15 16 20 21 fsumge1 ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ↑ 2 ) ≤ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
23 7 21 ffvelcdmd ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
24 12 21 ffvelcdmd ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐺 ‘ 𝐴 ) ∈ ℝ )
25 23 24 resubcld ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ )
26 absresq ⊢ ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ → ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ↑ 2 ) )
27 25 26 syl ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ↑ 2 ) )
28 3 15 fsumrecl ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
29 3 15 16 fsumge0 ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 0 ≤ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
30 resqrtth ⊢ ( ( Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
31 28 29 30 syl2anc ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
32 22 27 31 3brtr4d ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ↑ 2 ) ≤ ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↑ 2 ) )
33 25 recnd ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℂ )
34 33 abscld ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ∈ ℝ )
35 28 29 resqrtcld ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ ℝ )
36 33 absge0d ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) )
37 28 29 sqrtge0d ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 0 ≤ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
38 34 35 36 37 le2sqd ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ≤ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ↑ 2 ) ≤ ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↑ 2 ) ) )
39 32 38 mpbird ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ≤ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
40 2 remetdval ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝐴 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) )
41 23 24 40 syl2anc ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) )
42 1 rrnmval ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
43 42 3expb ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
44 43 adantlr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
45 39 41 44 3brtr4d ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )