tchcphlem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tchcphlem1		Structured version Visualization version GIF version

Theorem tchcphlem1 22842

Description: Lemma for tchcph 22844: the triangle inequality. (Contributed by Mario Carneiro, 8-Oct-2015.)

**Hypotheses**
Ref	Expression
tchval.n	⊢ 𝐺 = (toℂHil‘𝑊)
tchcph.v	⊢ 𝑉 = (Base‘𝑊)
tchcph.f	⊢ 𝐹 = (Scalar‘𝑊)
tchcph.1	⊢ (𝜑 → 𝑊 ∈ PreHil)
tchcph.2	⊢ (𝜑 → 𝐹 = (ℂ_fld ↾_s 𝐾))
tchcph.h	⊢ , = (·_𝑖‘𝑊)
tchcph.3	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾)
tchcph.4	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥))
tchcph.k	⊢ 𝐾 = (Base‘𝐹)
tchcph.m	⊢ − = (-_g‘𝑊)
tchcphlem1.3	⊢ (𝜑 → 𝑋 ∈ 𝑉)
tchcphlem1.4	⊢ (𝜑 → 𝑌 ∈ 𝑉)

**Assertion**
Ref	Expression
tchcphlem1	⊢ (𝜑 → (√‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) ≤ ((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌))))

Distinct variable groups: 𝑥, − 𝑥, , 𝑥,𝐹 𝑥,𝐺 𝑥,𝑉 𝜑,𝑥 𝑥,𝑊 𝑥,𝑋 𝑥,𝑌 Allowed substitution hint: 𝐾(𝑥)

**Proof of Theorem tchcphlem1**
Step	Hyp	Ref	Expression
1		tchcph.1	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ PreHil)
2		phllmod 19794	. . . . . . 7 ⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod)
3		lmodgrp 18693	. . . . . . 7 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
4	1, 2, 3	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ Grp)
5		tchcphlem1.3	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
6		tchcphlem1.4	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
7		tchcph.v	. . . . . . 7 ⊢ 𝑉 = (Base‘𝑊)
8		tchcph.m	. . . . . . 7 ⊢ − = (-_g‘𝑊)
9	7, 8	grpsubcl 17318	. . . . . 6 ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 − 𝑌) ∈ 𝑉)
10	4, 5, 6, 9	syl3anc 1318	. . . . 5 ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑉)
11		tchval.n	. . . . . 6 ⊢ 𝐺 = (toℂHil‘𝑊)
12		tchcph.f	. . . . . 6 ⊢ 𝐹 = (Scalar‘𝑊)
13		tchcph.2	. . . . . 6 ⊢ (𝜑 → 𝐹 = (ℂ_fld ↾_s 𝐾))
14		tchcph.h	. . . . . 6 ⊢ , = (·_𝑖‘𝑊)
15	11, 7, 12, 1, 13, 14	tchcphlem3 22840	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 − 𝑌) ∈ 𝑉) → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) ∈ ℝ)
16	10, 15	mpdan 699	. . . 4 ⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) ∈ ℝ)
17	11, 7, 12, 1, 13, 14	tchcphlem3 22840	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉) → (𝑋 , 𝑋) ∈ ℝ)
18	5, 17	mpdan 699	. . . . . 6 ⊢ (𝜑 → (𝑋 , 𝑋) ∈ ℝ)
19	11, 7, 12, 1, 13, 14	tchcphlem3 22840	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑌 ∈ 𝑉) → (𝑌 , 𝑌) ∈ ℝ)
20	6, 19	mpdan 699	. . . . . 6 ⊢ (𝜑 → (𝑌 , 𝑌) ∈ ℝ)
21	18, 20	readdcld 9948	. . . . 5 ⊢ (𝜑 → ((𝑋 , 𝑋) + (𝑌 , 𝑌)) ∈ ℝ)
22	11, 7, 12, 1, 13	tchclm 22839	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ℂMod)
23		tchcph.k	. . . . . . . . . 10 ⊢ 𝐾 = (Base‘𝐹)
24	12, 23	clmsscn 22687	. . . . . . . . 9 ⊢ (𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ)
25	22, 24	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ⊆ ℂ)
26	12, 14, 7, 23	ipcl 19797	. . . . . . . . 9 ⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 , 𝑌) ∈ 𝐾)
27	1, 5, 6, 26	syl3anc 1318	. . . . . . . 8 ⊢ (𝜑 → (𝑋 , 𝑌) ∈ 𝐾)
28	25, 27	sseldd 3569	. . . . . . 7 ⊢ (𝜑 → (𝑋 , 𝑌) ∈ ℂ)
29	12, 14, 7, 23	ipcl 19797	. . . . . . . . 9 ⊢ ((𝑊 ∈ PreHil ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑌 , 𝑋) ∈ 𝐾)
30	1, 6, 5, 29	syl3anc 1318	. . . . . . . 8 ⊢ (𝜑 → (𝑌 , 𝑋) ∈ 𝐾)
31	25, 30	sseldd 3569	. . . . . . 7 ⊢ (𝜑 → (𝑌 , 𝑋) ∈ ℂ)
32	28, 31	addcld 9938	. . . . . 6 ⊢ (𝜑 → ((𝑋 , 𝑌) + (𝑌 , 𝑋)) ∈ ℂ)
33	32	abscld 14023	. . . . 5 ⊢ (𝜑 → (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋))) ∈ ℝ)
34	21, 33	readdcld 9948	. . . 4 ⊢ (𝜑 → (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋)))) ∈ ℝ)
35	18	recnd 9947	. . . . . 6 ⊢ (𝜑 → (𝑋 , 𝑋) ∈ ℂ)
36		2re 10967	. . . . . . . 8 ⊢ 2 ∈ ℝ
37		tchcph.4	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥))
38	37	ralrimiva 2949	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝑉 0 ≤ (𝑥 , 𝑥))
39		oveq12 6558	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑋 ∧ 𝑥 = 𝑋) → (𝑥 , 𝑥) = (𝑋 , 𝑋))
40	39	anidms 675	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (𝑥 , 𝑥) = (𝑋 , 𝑋))
41	40	breq2d 4595	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ (𝑋 , 𝑋)))
42	41	rspcv 3278	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝑉 → (∀𝑥 ∈ 𝑉 0 ≤ (𝑥 , 𝑥) → 0 ≤ (𝑋 , 𝑋)))
43	5, 38, 42	sylc 63	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (𝑋 , 𝑋))
44	18, 43	resqrtcld 14004	. . . . . . . . 9 ⊢ (𝜑 → (√‘(𝑋 , 𝑋)) ∈ ℝ)
45		oveq12 6558	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑌 ∧ 𝑥 = 𝑌) → (𝑥 , 𝑥) = (𝑌 , 𝑌))
46	45	anidms 675	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → (𝑥 , 𝑥) = (𝑌 , 𝑌))
47	46	breq2d 4595	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑌 → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ (𝑌 , 𝑌)))
48	47	rspcv 3278	. . . . . . . . . . 11 ⊢ (𝑌 ∈ 𝑉 → (∀𝑥 ∈ 𝑉 0 ≤ (𝑥 , 𝑥) → 0 ≤ (𝑌 , 𝑌)))
49	6, 38, 48	sylc 63	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (𝑌 , 𝑌))
50	20, 49	resqrtcld 14004	. . . . . . . . 9 ⊢ (𝜑 → (√‘(𝑌 , 𝑌)) ∈ ℝ)
51	44, 50	remulcld 9949	. . . . . . . 8 ⊢ (𝜑 → ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ∈ ℝ)
52		remulcl 9900	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ∈ ℝ) → (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))) ∈ ℝ)
53	36, 51, 52	sylancr 694	. . . . . . 7 ⊢ (𝜑 → (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))) ∈ ℝ)
54	53	recnd 9947	. . . . . 6 ⊢ (𝜑 → (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))) ∈ ℂ)
55	20	recnd 9947	. . . . . 6 ⊢ (𝜑 → (𝑌 , 𝑌) ∈ ℂ)
56	35, 54, 55	add32d 10142	. . . . 5 ⊢ (𝜑 → (((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + (𝑌 , 𝑌)) = (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))))
57	21, 53	readdcld 9948	. . . . 5 ⊢ (𝜑 → (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) ∈ ℝ)
58	56, 57	eqeltrd 2688	. . . 4 ⊢ (𝜑 → (((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + (𝑌 , 𝑌)) ∈ ℝ)
59		oveq12 6558	. . . . . . . . . . . 12 ⊢ ((𝑥 = (𝑋 − 𝑌) ∧ 𝑥 = (𝑋 − 𝑌)) → (𝑥 , 𝑥) = ((𝑋 − 𝑌) , (𝑋 − 𝑌)))
60	59	anidms 675	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑋 − 𝑌) → (𝑥 , 𝑥) = ((𝑋 − 𝑌) , (𝑋 − 𝑌)))
61	60	breq2d 4595	. . . . . . . . . 10 ⊢ (𝑥 = (𝑋 − 𝑌) → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ ((𝑋 − 𝑌) , (𝑋 − 𝑌))))
62	61	rspcv 3278	. . . . . . . . 9 ⊢ ((𝑋 − 𝑌) ∈ 𝑉 → (∀𝑥 ∈ 𝑉 0 ≤ (𝑥 , 𝑥) → 0 ≤ ((𝑋 − 𝑌) , (𝑋 − 𝑌))))
63	10, 38, 62	sylc 63	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ ((𝑋 − 𝑌) , (𝑋 − 𝑌)))
64	16, 63	absidd 14009	. . . . . . 7 ⊢ (𝜑 → (abs‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) = ((𝑋 − 𝑌) , (𝑋 − 𝑌)))
65	12	clmadd 22682	. . . . . . . . . . . 12 ⊢ (𝑊 ∈ ℂMod → + = (+_g‘𝐹))
66	22, 65	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → + = (+_g‘𝐹))
67	66	oveqd 6566	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 , 𝑋) + (𝑌 , 𝑌)) = ((𝑋 , 𝑋)(+_g‘𝐹)(𝑌 , 𝑌)))
68	66	oveqd 6566	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 , 𝑌) + (𝑌 , 𝑋)) = ((𝑋 , 𝑌)(+_g‘𝐹)(𝑌 , 𝑋)))
69	67, 68	oveq12d 6567	. . . . . . . . 9 ⊢ (𝜑 → (((𝑋 , 𝑋) + (𝑌 , 𝑌))(-_g‘𝐹)((𝑋 , 𝑌) + (𝑌 , 𝑋))) = (((𝑋 , 𝑋)(+_g‘𝐹)(𝑌 , 𝑌))(-_g‘𝐹)((𝑋 , 𝑌)(+_g‘𝐹)(𝑌 , 𝑋))))
70	12, 14, 7, 23	ipcl 19797	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑋 , 𝑋) ∈ 𝐾)
71	1, 5, 5, 70	syl3anc 1318	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 , 𝑋) ∈ 𝐾)
72	12, 14, 7, 23	ipcl 19797	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ PreHil ∧ 𝑌 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑌 , 𝑌) ∈ 𝐾)
73	1, 6, 6, 72	syl3anc 1318	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 , 𝑌) ∈ 𝐾)
74	12, 23	clmacl 22692	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑋) ∈ 𝐾 ∧ (𝑌 , 𝑌) ∈ 𝐾) → ((𝑋 , 𝑋) + (𝑌 , 𝑌)) ∈ 𝐾)
75	22, 71, 73, 74	syl3anc 1318	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 , 𝑋) + (𝑌 , 𝑌)) ∈ 𝐾)
76	12, 23	clmacl 22692	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑌) ∈ 𝐾 ∧ (𝑌 , 𝑋) ∈ 𝐾) → ((𝑋 , 𝑌) + (𝑌 , 𝑋)) ∈ 𝐾)
77	22, 27, 30, 76	syl3anc 1318	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 , 𝑌) + (𝑌 , 𝑋)) ∈ 𝐾)
78	12, 23	clmsub 22688	. . . . . . . . . 10 ⊢ ((𝑊 ∈ ℂMod ∧ ((𝑋 , 𝑋) + (𝑌 , 𝑌)) ∈ 𝐾 ∧ ((𝑋 , 𝑌) + (𝑌 , 𝑋)) ∈ 𝐾) → (((𝑋 , 𝑋) + (𝑌 , 𝑌)) − ((𝑋 , 𝑌) + (𝑌 , 𝑋))) = (((𝑋 , 𝑋) + (𝑌 , 𝑌))(-_g‘𝐹)((𝑋 , 𝑌) + (𝑌 , 𝑋))))
79	22, 75, 77, 78	syl3anc 1318	. . . . . . . . 9 ⊢ (𝜑 → (((𝑋 , 𝑋) + (𝑌 , 𝑌)) − ((𝑋 , 𝑌) + (𝑌 , 𝑋))) = (((𝑋 , 𝑋) + (𝑌 , 𝑌))(-_g‘𝐹)((𝑋 , 𝑌) + (𝑌 , 𝑋))))
80		eqid 2610	. . . . . . . . . 10 ⊢ (-_g‘𝐹) = (-_g‘𝐹)
81		eqid 2610	. . . . . . . . . 10 ⊢ (+_g‘𝐹) = (+_g‘𝐹)
82	12, 14, 7, 8, 80, 81, 1, 5, 6, 5, 6	ip2subdi 19808	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) = (((𝑋 , 𝑋)(+_g‘𝐹)(𝑌 , 𝑌))(-_g‘𝐹)((𝑋 , 𝑌)(+_g‘𝐹)(𝑌 , 𝑋))))
83	69, 79, 82	3eqtr4rd 2655	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) = (((𝑋 , 𝑋) + (𝑌 , 𝑌)) − ((𝑋 , 𝑌) + (𝑌 , 𝑋))))
84	83	fveq2d 6107	. . . . . . 7 ⊢ (𝜑 → (abs‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) = (abs‘(((𝑋 , 𝑋) + (𝑌 , 𝑌)) − ((𝑋 , 𝑌) + (𝑌 , 𝑋)))))
85	64, 84	eqtr3d 2646	. . . . . 6 ⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) = (abs‘(((𝑋 , 𝑋) + (𝑌 , 𝑌)) − ((𝑋 , 𝑌) + (𝑌 , 𝑋)))))
86	25, 75	sseldd 3569	. . . . . . 7 ⊢ (𝜑 → ((𝑋 , 𝑋) + (𝑌 , 𝑌)) ∈ ℂ)
87	86, 32	abs2dif2d 14045	. . . . . 6 ⊢ (𝜑 → (abs‘(((𝑋 , 𝑋) + (𝑌 , 𝑌)) − ((𝑋 , 𝑌) + (𝑌 , 𝑋)))) ≤ ((abs‘((𝑋 , 𝑋) + (𝑌 , 𝑌))) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋)))))
88	85, 87	eqbrtrd 4605	. . . . 5 ⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) ≤ ((abs‘((𝑋 , 𝑋) + (𝑌 , 𝑌))) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋)))))
89	18, 20, 43, 49	addge0d 10482	. . . . . . 7 ⊢ (𝜑 → 0 ≤ ((𝑋 , 𝑋) + (𝑌 , 𝑌)))
90	21, 89	absidd 14009	. . . . . 6 ⊢ (𝜑 → (abs‘((𝑋 , 𝑋) + (𝑌 , 𝑌))) = ((𝑋 , 𝑋) + (𝑌 , 𝑌)))
91	90	oveq1d 6564	. . . . 5 ⊢ (𝜑 → ((abs‘((𝑋 , 𝑋) + (𝑌 , 𝑌))) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋)))) = (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋)))))
92	88, 91	breqtrd 4609	. . . 4 ⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) ≤ (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋)))))
93	28	abscld 14023	. . . . . . . 8 ⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ∈ ℝ)
94		remulcl 9900	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ (abs‘(𝑋 , 𝑌)) ∈ ℝ) → (2 · (abs‘(𝑋 , 𝑌))) ∈ ℝ)
95	36, 93, 94	sylancr 694	. . . . . . 7 ⊢ (𝜑 → (2 · (abs‘(𝑋 , 𝑌))) ∈ ℝ)
96	28, 31	abstrid 14043	. . . . . . . 8 ⊢ (𝜑 → (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋))) ≤ ((abs‘(𝑋 , 𝑌)) + (abs‘(𝑌 , 𝑋))))
97	93	recnd 9947	. . . . . . . . . 10 ⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ∈ ℂ)
98	97	2timesd 11152	. . . . . . . . 9 ⊢ (𝜑 → (2 · (abs‘(𝑋 , 𝑌))) = ((abs‘(𝑋 , 𝑌)) + (abs‘(𝑋 , 𝑌))))
99	28	abscjd 14037	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(∗‘(𝑋 , 𝑌))) = (abs‘(𝑋 , 𝑌)))
100	12	clmcj 22684	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ ℂMod → ∗ = (*_𝑟‘𝐹))
101	22, 100	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∗ = (*_𝑟‘𝐹))
102	101	fveq1d 6105	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∗‘(𝑋 , 𝑌)) = ((*_𝑟‘𝐹)‘(𝑋 , 𝑌)))
103		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ (_𝑟‘𝐹) = (_𝑟‘𝐹)
104	12, 14, 7, 103	ipcj 19798	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((*_𝑟‘𝐹)‘(𝑋 , 𝑌)) = (𝑌 , 𝑋))
105	1, 5, 6, 104	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((*_𝑟‘𝐹)‘(𝑋 , 𝑌)) = (𝑌 , 𝑋))
106	102, 105	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(𝑋 , 𝑌)) = (𝑌 , 𝑋))
107	106	fveq2d 6107	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(∗‘(𝑋 , 𝑌))) = (abs‘(𝑌 , 𝑋)))
108	99, 107	eqtr3d 2646	. . . . . . . . . 10 ⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) = (abs‘(𝑌 , 𝑋)))
109	108	oveq2d 6565	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘(𝑋 , 𝑌)) + (abs‘(𝑋 , 𝑌))) = ((abs‘(𝑋 , 𝑌)) + (abs‘(𝑌 , 𝑋))))
110	98, 109	eqtrd 2644	. . . . . . . 8 ⊢ (𝜑 → (2 · (abs‘(𝑋 , 𝑌))) = ((abs‘(𝑋 , 𝑌)) + (abs‘(𝑌 , 𝑋))))
111	96, 110	breqtrrd 4611	. . . . . . 7 ⊢ (𝜑 → (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋))) ≤ (2 · (abs‘(𝑋 , 𝑌))))
112		tchcph.3	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾)
113		eqid 2610	. . . . . . . . . 10 ⊢ (norm‘𝐺) = (norm‘𝐺)
114		eqid 2610	. . . . . . . . . 10 ⊢ ((𝑌 , 𝑋) / (𝑌 , 𝑌)) = ((𝑌 , 𝑋) / (𝑌 , 𝑌))
115	11, 7, 12, 1, 13, 14, 112, 37, 23, 113, 114, 5, 6	ipcau2 22841	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ (((norm‘𝐺)‘𝑋) · ((norm‘𝐺)‘𝑌)))
116	11, 113, 7, 14	tchnmval 22836	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉) → ((norm‘𝐺)‘𝑋) = (√‘(𝑋 , 𝑋)))
117	4, 5, 116	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → ((norm‘𝐺)‘𝑋) = (√‘(𝑋 , 𝑋)))
118	11, 113, 7, 14	tchnmval 22836	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝑉) → ((norm‘𝐺)‘𝑌) = (√‘(𝑌 , 𝑌)))
119	4, 6, 118	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → ((norm‘𝐺)‘𝑌) = (√‘(𝑌 , 𝑌)))
120	117, 119	oveq12d 6567	. . . . . . . . 9 ⊢ (𝜑 → (((norm‘𝐺)‘𝑋) · ((norm‘𝐺)‘𝑌)) = ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))
121	115, 120	breqtrd 4609	. . . . . . . 8 ⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))
122	36	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 2 ∈ ℝ)
123		2pos 10989	. . . . . . . . . 10 ⊢ 0 < 2
124	123	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 < 2)
125		lemul2 10755	. . . . . . . . 9 ⊢ (((abs‘(𝑋 , 𝑌)) ∈ ℝ ∧ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ↔ (2 · (abs‘(𝑋 , 𝑌))) ≤ (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))))
126	93, 51, 122, 124, 125	syl112anc 1322	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ↔ (2 · (abs‘(𝑋 , 𝑌))) ≤ (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))))
127	121, 126	mpbid 221	. . . . . . 7 ⊢ (𝜑 → (2 · (abs‘(𝑋 , 𝑌))) ≤ (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))))
128	33, 95, 53, 111, 127	letrd 10073	. . . . . 6 ⊢ (𝜑 → (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋))) ≤ (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))))
129	33, 53, 21, 128	leadd2dd 10521	. . . . 5 ⊢ (𝜑 → (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋)))) ≤ (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))))
130	129, 56	breqtrrd 4611	. . . 4 ⊢ (𝜑 → (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋)))) ≤ (((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + (𝑌 , 𝑌)))
131	16, 34, 58, 92, 130	letrd 10073	. . 3 ⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) ≤ (((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + (𝑌 , 𝑌)))
132	16	recnd 9947	. . . 4 ⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) ∈ ℂ)
133	132	sqsqrtd 14026	. . 3 ⊢ (𝜑 → ((√‘((𝑋 − 𝑌) , (𝑋 − 𝑌)))↑2) = ((𝑋 − 𝑌) , (𝑋 − 𝑌)))
134	35	sqrtcld 14024	. . . . 5 ⊢ (𝜑 → (√‘(𝑋 , 𝑋)) ∈ ℂ)
135	50	recnd 9947	. . . . 5 ⊢ (𝜑 → (√‘(𝑌 , 𝑌)) ∈ ℂ)
136		binom2 12841	. . . . 5 ⊢ (((√‘(𝑋 , 𝑋)) ∈ ℂ ∧ (√‘(𝑌 , 𝑌)) ∈ ℂ) → (((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))↑2) = ((((√‘(𝑋 , 𝑋))↑2) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + ((√‘(𝑌 , 𝑌))↑2)))
137	134, 135, 136	syl2anc 691	. . . 4 ⊢ (𝜑 → (((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))↑2) = ((((√‘(𝑋 , 𝑋))↑2) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + ((√‘(𝑌 , 𝑌))↑2)))
138	35	sqsqrtd 14026	. . . . . 6 ⊢ (𝜑 → ((√‘(𝑋 , 𝑋))↑2) = (𝑋 , 𝑋))
139	138	oveq1d 6564	. . . . 5 ⊢ (𝜑 → (((√‘(𝑋 , 𝑋))↑2) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) = ((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))))
140	55	sqsqrtd 14026	. . . . 5 ⊢ (𝜑 → ((√‘(𝑌 , 𝑌))↑2) = (𝑌 , 𝑌))
141	139, 140	oveq12d 6567	. . . 4 ⊢ (𝜑 → ((((√‘(𝑋 , 𝑋))↑2) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + ((√‘(𝑌 , 𝑌))↑2)) = (((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + (𝑌 , 𝑌)))
142	137, 141	eqtrd 2644	. . 3 ⊢ (𝜑 → (((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))↑2) = (((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + (𝑌 , 𝑌)))
143	131, 133, 142	3brtr4d 4615	. 2 ⊢ (𝜑 → ((√‘((𝑋 − 𝑌) , (𝑋 − 𝑌)))↑2) ≤ (((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))↑2))
144	16, 63	resqrtcld 14004	. . 3 ⊢ (𝜑 → (√‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) ∈ ℝ)
145	44, 50	readdcld 9948	. . 3 ⊢ (𝜑 → ((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌))) ∈ ℝ)
146	16, 63	sqrtge0d 14007	. . 3 ⊢ (𝜑 → 0 ≤ (√‘((𝑋 − 𝑌) , (𝑋 − 𝑌))))
147	18, 43	sqrtge0d 14007	. . . 4 ⊢ (𝜑 → 0 ≤ (√‘(𝑋 , 𝑋)))
148	20, 49	sqrtge0d 14007	. . . 4 ⊢ (𝜑 → 0 ≤ (√‘(𝑌 , 𝑌)))
149	44, 50, 147, 148	addge0d 10482	. . 3 ⊢ (𝜑 → 0 ≤ ((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌))))
150	144, 145, 146, 149	le2sqd 12906	. 2 ⊢ (𝜑 → ((√‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) ≤ ((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌))) ↔ ((√‘((𝑋 − 𝑌) , (𝑋 − 𝑌)))↑2) ≤ (((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))↑2)))
151	143, 150	mpbird 246	1 ⊢ (𝜑 → (√‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) ≤ ((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ⊆ wss 3540 class class class wbr 4583 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 + caddc 9818 · cmul 9820 < clt 9953 ≤ cle 9954 − cmin 10145 / cdiv 10563 2c2 10947 ↑cexp 12722 ∗ccj 13684 √csqrt 13821 abscabs 13822 Basecbs 15695 ↾_s cress 15696 +_gcplusg 15768 *_𝑟cstv 15770 Scalarcsca 15771 ·_𝑖cip 15773 Grpcgrp 17245 -_gcsg 17247 LModclmod 18686 ℂ_fldccnfld 19567 PreHilcphl 19788 normcnm 22191 ℂModcclm 22670 toℂHilctch 22775

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894 ax-mulf 9895

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-tpos 7239 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-map 7746 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-z 11255 df-dec 11370 df-uz 11564 df-rp 11709 df-fz 12198 df-seq 12664 df-exp 12723 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-struct 15697 df-ndx 15698 df-slot 15699 df-base 15700 df-sets 15701 df-ress 15702 df-plusg 15781 df-mulr 15782 df-starv 15783 df-sca 15784 df-vsca 15785 df-ip 15786 df-tset 15787 df-ple 15788 df-ds 15791 df-unif 15792 df-0g 15925 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-mhm 17158 df-grp 17248 df-minusg 17249 df-sbg 17250 df-subg 17414 df-ghm 17481 df-cmn 18018 df-abl 18019 df-mgp 18313 df-ur 18325 df-ring 18372 df-cring 18373 df-oppr 18446 df-dvdsr 18464 df-unit 18465 df-invr 18495 df-dvr 18506 df-rnghom 18538 df-drng 18572 df-subrg 18601 df-staf 18668 df-srng 18669 df-lmod 18688 df-lmhm 18843 df-lvec 18924 df-sra 18993 df-rgmod 18994 df-cnfld 19568 df-phl 19790 df-nm 22197 df-tng 22199 df-clm 22671 df-tch 22777

This theorem is referenced by: tchcph 22844

W3C validator