rrnprjdstle

Description: The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	rrnprjdstle.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	rrnprjdstle.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
	rrnprjdstle.g	⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℝ )
	rrnprjdstle.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
	rrnprjdstle.d	⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝑋 ) )
Assertion	rrnprjdstle	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝐼 ) − ( 𝐺 ‘ 𝐼 ) ) ) ≤ ( 𝐹 𝐷 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		rrnprjdstle.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		rrnprjdstle.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
3		rrnprjdstle.g	⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℝ )
4		rrnprjdstle.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
5		rrnprjdstle.d	⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝑋 ) )
6	2 4	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) ∈ ℝ )
7	3 4	ffvelcdmd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐼 ) ∈ ℝ )
8		eqid	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
9	8	remetdval	⊢ ( ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝐼 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐼 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝐼 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝐼 ) − ( 𝐺 ‘ 𝐼 ) ) ) )
10	6 7 9	syl2anc	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐼 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝐼 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝐼 ) − ( 𝐺 ‘ 𝐼 ) ) ) )
11	10	eqcomd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝐼 ) − ( 𝐺 ‘ 𝐼 ) ) ) = ( ( 𝐹 ‘ 𝐼 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝐼 ) ) )
12		reex	⊢ ℝ ∈ V
13	12	a1i	⊢ ( 𝜑 → ℝ ∈ V )
14	13 1	elmapd	⊢ ( 𝜑 → ( 𝐹 ∈ ( ℝ ↑_m 𝑋 ) ↔ 𝐹 : 𝑋 ⟶ ℝ ) )
15	2 14	mpbird	⊢ ( 𝜑 → 𝐹 ∈ ( ℝ ↑_m 𝑋 ) )
16		eqid	⊢ ( ℝ^ ‘ 𝑋 ) = ( ℝ^ ‘ 𝑋 )
17		eqid	⊢ ( Base ‘ ( ℝ^ ‘ 𝑋 ) ) = ( Base ‘ ( ℝ^ ‘ 𝑋 ) )
18	1 16 17	rrxbasefi	⊢ ( 𝜑 → ( Base ‘ ( ℝ^ ‘ 𝑋 ) ) = ( ℝ ↑_m 𝑋 ) )
19	16 17	rrxbase	⊢ ( 𝑋 ∈ Fin → ( Base ‘ ( ℝ^ ‘ 𝑋 ) ) = { ℎ ∈ ( ℝ ↑_m 𝑋 ) ∣ ℎ finSupp 0 } )
20	1 19	syl	⊢ ( 𝜑 → ( Base ‘ ( ℝ^ ‘ 𝑋 ) ) = { ℎ ∈ ( ℝ ↑_m 𝑋 ) ∣ ℎ finSupp 0 } )
21	18 20	eqtr3d	⊢ ( 𝜑 → ( ℝ ↑_m 𝑋 ) = { ℎ ∈ ( ℝ ↑_m 𝑋 ) ∣ ℎ finSupp 0 } )
22	15 21	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ { ℎ ∈ ( ℝ ↑_m 𝑋 ) ∣ ℎ finSupp 0 } )
23	13 1	elmapd	⊢ ( 𝜑 → ( 𝐺 ∈ ( ℝ ↑_m 𝑋 ) ↔ 𝐺 : 𝑋 ⟶ ℝ ) )
24	3 23	mpbird	⊢ ( 𝜑 → 𝐺 ∈ ( ℝ ↑_m 𝑋 ) )
25	24 21	eleqtrd	⊢ ( 𝜑 → 𝐺 ∈ { ℎ ∈ ( ℝ ↑_m 𝑋 ) ∣ ℎ finSupp 0 } )
26		eqid	⊢ { ℎ ∈ ( ℝ ↑_m 𝑋 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℝ ↑_m 𝑋 ) ∣ ℎ finSupp 0 }
27	26 5 8	rrxdstprj1	⊢ ( ( ( 𝑋 ∈ Fin ∧ 𝐼 ∈ 𝑋 ) ∧ ( 𝐹 ∈ { ℎ ∈ ( ℝ ↑_m 𝑋 ) ∣ ℎ finSupp 0 } ∧ 𝐺 ∈ { ℎ ∈ ( ℝ ↑_m 𝑋 ) ∣ ℎ finSupp 0 } ) ) → ( ( 𝐹 ‘ 𝐼 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝐼 ) ) ≤ ( 𝐹 𝐷 𝐺 ) )
28	1 4 22 25 27	syl22anc	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐼 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝐼 ) ) ≤ ( 𝐹 𝐷 𝐺 ) )
29	11 28	eqbrtrd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝐼 ) − ( 𝐺 ‘ 𝐼 ) ) ) ≤ ( 𝐹 𝐷 𝐺 ) )

Metamath Proof Explorer

Theorem rrnprjdstle

Proof