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

Metamath Proof Explorer

Theorem rrxdstprj1

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) (Revised by Thierry Arnoux, 7-Jul-2019)

Ref Expression
Hypotheses rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
rrxmval.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
rrxdstprj1.1 ⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
Assertion rrxdstprj1 ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) ≤ ( 𝐹 𝐷 𝐺 ) )

Proof

Step Hyp Ref Expression
1 rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 rrxmval.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
3 rrxdstprj1.1 ⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
4 simplll ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) → 𝐼 ∈ 𝑉 )
5 simpr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) → 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )
6 simplr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) → ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) )
7 simprl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐹 ∈ 𝑋 )
8 1 7 rrxfsupp ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 supp 0 ) ∈ Fin )
9 simprr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐺 ∈ 𝑋 )
10 1 9 rrxfsupp ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐺 supp 0 ) ∈ Fin )
11 unfi ⊢ ( ( ( 𝐹 supp 0 ) ∈ Fin ∧ ( 𝐺 supp 0 ) ∈ Fin ) → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∈ Fin )
12 8 10 11 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∈ Fin )
13 1 7 rrxsuppss ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 supp 0 ) ⊆ 𝐼 )
14 1 9 rrxsuppss ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐺 supp 0 ) ⊆ 𝐼 )
15 13 14 unssd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ⊆ 𝐼 )
16 15 sselda ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) → 𝑘 ∈ 𝐼 )
17 1 7 rrxf ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐹 : 𝐼 ⟶ ℝ )
18 17 ffvelcdmda ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
19 1 9 rrxf ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐺 : 𝐼 ⟶ ℝ )
20 19 ffvelcdmda ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
21 18 20 resubcld ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
22 21 resqcld ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
23 16 22 syldan ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
24 21 sqge0d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → 0 ≤ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
25 16 24 syldan ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) → 0 ≤ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
26 fveq2 ⊢ ( 𝑘 = 𝐴 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝐴 ) )
27 fveq2 ⊢ ( 𝑘 = 𝐴 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝐴 ) )
28 26 27 oveq12d ⊢ ( 𝑘 = 𝐴 → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) )
29 28 oveq1d ⊢ ( 𝑘 = 𝐴 → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ↑ 2 ) )
30 simplr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )
31 12 23 25 29 30 fsumge1 ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ↑ 2 ) ≤ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
32 15 30 sseldd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐴 ∈ 𝐼 )
33 17 32 ffvelcdmd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
34 19 32 ffvelcdmd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐺 ‘ 𝐴 ) ∈ ℝ )
35 33 34 resubcld ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ )
36 absresq ⊢ ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ → ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ↑ 2 ) )
37 35 36 syl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ↑ 2 ) )
38 12 23 fsumrecl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
39 12 23 25 fsumge0 ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 0 ≤ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
40 resqrtth ⊢ ( ( Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) → ( ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↑ 2 ) = Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
41 38 39 40 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↑ 2 ) = Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
42 31 37 41 3brtr4d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ↑ 2 ) ≤ ( ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↑ 2 ) )
43 35 recnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℂ )
44 43 abscld ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ∈ ℝ )
45 38 39 resqrtcld ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ ℝ )
46 43 absge0d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) )
47 38 39 sqrtge0d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 0 ≤ ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
48 44 45 46 47 le2sqd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ≤ ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ↑ 2 ) ≤ ( ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↑ 2 ) ) )
49 42 48 mpbird ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) ≤ ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
50 3 remetdval ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝐴 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) )
51 33 34 50 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) )
52 1 2 rrxmval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
53 52 3expb ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 𝐷 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
54 53 adantlr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 𝐷 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
55 49 51 54 3brtr4d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) ≤ ( 𝐹 𝐷 𝐺 ) )
56 4 5 6 55 syl21anc ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) ≤ ( 𝐹 𝐷 𝐺 ) )
57 simplll ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → 𝐼 ∈ 𝑉 )
58 simplrl ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → 𝐹 ∈ 𝑋 )
59 ssun1 ⊢ ( 𝐹 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) )
60 59 a1i ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )
61 60 sscond ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ⊆ ( 𝐼 ∖ ( 𝐹 supp 0 ) ) )
62 61 sselda ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → 𝐴 ∈ ( 𝐼 ∖ ( 𝐹 supp 0 ) ) )
63 simpr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ) → 𝐹 ∈ 𝑋 )
64 1 63 rrxf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ) → 𝐹 : 𝐼 ⟶ ℝ )
65 ssidd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ) → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
66 simpl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ) → 𝐼 ∈ 𝑉 )
67 0red ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ) → 0 ∈ ℝ )
68 64 65 66 67 suppssr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ‘ 𝐴 ) = 0 )
69 57 58 62 68 syl21anc ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( 𝐹 ‘ 𝐴 ) = 0 )
70 0red ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → 0 ∈ ℝ )
71 69 70 eqeltrd ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
72 simplrr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → 𝐺 ∈ 𝑋 )
73 ssun2 ⊢ ( 𝐺 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) )
74 73 a1i ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐺 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )
75 74 sscond ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ⊆ ( 𝐼 ∖ ( 𝐺 supp 0 ) ) )
76 75 sselda ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → 𝐴 ∈ ( 𝐼 ∖ ( 𝐺 supp 0 ) ) )
77 simpr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋 ) → 𝐺 ∈ 𝑋 )
78 1 77 rrxf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋 ) → 𝐺 : 𝐼 ⟶ ℝ )
79 ssidd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐺 supp 0 ) ⊆ ( 𝐺 supp 0 ) )
80 simpl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋 ) → 𝐼 ∈ 𝑉 )
81 0red ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋 ) → 0 ∈ ℝ )
82 78 79 80 81 suppssr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( 𝐺 supp 0 ) ) ) → ( 𝐺 ‘ 𝐴 ) = 0 )
83 57 72 76 82 syl21anc ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( 𝐺 ‘ 𝐴 ) = 0 )
84 83 70 eqeltrd ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( 𝐺 ‘ 𝐴 ) ∈ ℝ )
85 71 84 50 syl2anc ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) )
86 69 83 oveq12d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) = ( 0 − 0 ) )
87 0m0e0 ⊢ ( 0 − 0 ) = 0
88 86 87 eqtrdi ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) = 0 )
89 88 abs00bd ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐺 ‘ 𝐴 ) ) ) = 0 )
90 85 89 eqtrd ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) = 0 )
91 1 2 rrxmet ⊢ ( 𝐼 ∈ 𝑉 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
92 91 ad3antrrr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
93 metge0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 0 ≤ ( 𝐹 𝐷 𝐺 ) )
94 92 58 72 93 syl3anc ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → 0 ≤ ( 𝐹 𝐷 𝐺 ) )
95 90 94 eqbrtrd ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) ≤ ( 𝐹 𝐷 𝐺 ) )
96 simplr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐴 ∈ 𝐼 )
97 simprl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐹 ∈ 𝑋 )
98 1 97 rrxsuppss ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 supp 0 ) ⊆ 𝐼 )
99 simprr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐺 ∈ 𝑋 )
100 1 99 rrxsuppss ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐺 supp 0 ) ⊆ 𝐼 )
101 98 100 unssd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ⊆ 𝐼 )
102 undif ⊢ ( ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ⊆ 𝐼 ↔ ( ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∪ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) = 𝐼 )
103 101 102 sylib ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∪ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) = 𝐼 )
104 96 103 eleqtrrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐴 ∈ ( ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∪ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) )
105 elun ⊢ ( 𝐴 ∈ ( ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∪ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) ↔ ( 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∨ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) )
106 104 105 sylib ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐴 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∨ 𝐴 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) )
107 56 95 106 mpjaodan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝑀 ( 𝐺 ‘ 𝐴 ) ) ≤ ( 𝐹 𝐷 𝐺 ) )