Metamath Proof Explorer

Theorem 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 ⊢ φ → X ∈ Fin
rrnprjdstle.f ⊢ φ → F : X ⟶ ℝ
rrnprjdstle.g ⊢ φ → G : X ⟶ ℝ
rrnprjdstle.i ⊢ φ → I ∈ X
rrnprjdstle.d ⊢ D = dist ⁡ X
Assertion rrnprjdstle ⊢ φ → F ⁡ I − G ⁡ I ≤ F D G

Proof

Step Hyp Ref Expression
1 rrnprjdstle.x ⊢ φ → X ∈ Fin
2 rrnprjdstle.f ⊢ φ → F : X ⟶ ℝ
3 rrnprjdstle.g ⊢ φ → G : X ⟶ ℝ
4 rrnprjdstle.i ⊢ φ → I ∈ X
5 rrnprjdstle.d ⊢ D = dist ⁡ X
6 2 4 ffvelcdmd ⊢ φ → F ⁡ I ∈ ℝ
7 3 4 ffvelcdmd ⊢ φ → G ⁡ I ∈ ℝ
8 eqid ⊢ abs ∘ − ↾ ℝ 2 = abs ∘ − ↾ ℝ 2
9 8 remetdval ⊢ F ⁡ I ∈ ℝ ∧ G ⁡ I ∈ ℝ → F ⁡ I abs ∘ − ↾ ℝ 2 G ⁡ I = F ⁡ I − G ⁡ I
10 6 7 9 syl2anc ⊢ φ → F ⁡ I abs ∘ − ↾ ℝ 2 G ⁡ I = F ⁡ I − G ⁡ I
11 10 eqcomd ⊢ φ → F ⁡ I − G ⁡ I = F ⁡ I abs ∘ − ↾ ℝ 2 G ⁡ I
12 reex ⊢ ℝ ∈ V
13 12 a1i ⊢ φ → ℝ ∈ V
14 13 1 elmapd ⊢ φ → F ∈ ℝ X ↔ F : X ⟶ ℝ
15 2 14 mpbird ⊢ φ → F ∈ ℝ X
16 eqid ⊢ X = X
17 eqid ⊢ Base X = Base X
18 1 16 17 rrxbasefi ⊢ φ → Base X = ℝ X
19 16 17 rrxbase ⊢ X ∈ Fin → Base X = h ∈ ℝ X | finSupp 0 ⁡ h
20 1 19 syl ⊢ φ → Base X = h ∈ ℝ X | finSupp 0 ⁡ h
21 18 20 eqtr3d ⊢ φ → ℝ X = h ∈ ℝ X | finSupp 0 ⁡ h
22 15 21 eleqtrd ⊢ φ → F ∈ h ∈ ℝ X | finSupp 0 ⁡ h
23 13 1 elmapd ⊢ φ → G ∈ ℝ X ↔ G : X ⟶ ℝ
24 3 23 mpbird ⊢ φ → G ∈ ℝ X
25 24 21 eleqtrd ⊢ φ → G ∈ h ∈ ℝ X | finSupp 0 ⁡ h
26 eqid ⊢ h ∈ ℝ X | finSupp 0 ⁡ h = h ∈ ℝ X | finSupp 0 ⁡ h
27 26 5 8 rrxdstprj1 ⊢ X ∈ Fin ∧ I ∈ X ∧ F ∈ h ∈ ℝ X | finSupp 0 ⁡ h ∧ G ∈ h ∈ ℝ X | finSupp 0 ⁡ h → F ⁡ I abs ∘ − ↾ ℝ 2 G ⁡ I ≤ F D G
28 1 4 22 25 27 syl22anc ⊢ φ → F ⁡ I abs ∘ − ↾ ℝ 2 G ⁡ I ≤ F D G
29 11 28 eqbrtrd ⊢ φ → F ⁡ I − G ⁡ I ≤ F D G