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 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) ≤ ( 𝐹 ( ℝⁿ ‘ 𝐼 ) 𝐺 ) )

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 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 ( ℝⁿ ‘ 𝐼 ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
43	42	3expb	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 ( ℝⁿ ‘ 𝐼 ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
44	43	adantlr	⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 ( ℝⁿ ‘ 𝐼 ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
45	39 41 44	3brtr4d	⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) ≤ ( 𝐹 ( ℝⁿ ‘ 𝐼 ) 𝐺 ) )

Metamath Proof Explorer

Theorem rrndstprj1

Proof