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

Metamath Proof Explorer

Theorem rrxdstprj1

Proof