Theorem tcphcphlem1

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

	Ref	Expression
Hypotheses	tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
	tcphcph.v	$$⊢V={\mathrm{Base}}_W$$
	tcphcph.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	tcphcph.1	$$⊢\phi \to W\in \mathrm{PreHil}$$
	tcphcph.2	$$⊢\phi \to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
	tcphcph.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	tcphcph.3	$$⊢\left(\phi \wedge \left(x\in K\wedge x\in ℝ\wedge 0\le x\right)\right)\to \sqrt{x}\in K$$
	tcphcph.4	$$⊢\left(\phi \wedge x\in V\right)\to 0\le x\underset{\dot{}}{,}x$$
	tcphcph.k	$$⊢K={\mathrm{Base}}_F$$
	tcphcph.m	$$⊢\underset{\dot{}}{-}={-}_W$$
	tcphcphlem1.3	$$⊢\phi \to X\in V$$
	tcphcphlem1.4	$$⊢\phi \to Y\in V$$
Assertion	tcphcphlem1	$$⊢\phi \to \sqrt{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)}\le \sqrt{X\underset{\dot{}}{,}X}+\sqrt{Y\underset{\dot{}}{,}Y}$$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
2		tcphcph.v	$$⊢V={\mathrm{Base}}_W$$
3		tcphcph.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		tcphcph.1	$$⊢\phi \to W\in \mathrm{PreHil}$$
5		tcphcph.2	$$⊢\phi \to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
6		tcphcph.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
7		tcphcph.3	$$⊢\left(\phi \wedge \left(x\in K\wedge x\in ℝ\wedge 0\le x\right)\right)\to \sqrt{x}\in K$$
8		tcphcph.4	$$⊢\left(\phi \wedge x\in V\right)\to 0\le x\underset{\dot{}}{,}x$$
9		tcphcph.k	$$⊢K={\mathrm{Base}}_F$$
10		tcphcph.m	$$⊢\underset{\dot{}}{-}={-}_W$$
11		tcphcphlem1.3	$$⊢\phi \to X\in V$$
12		tcphcphlem1.4	$$⊢\phi \to Y\in V$$
13		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
14		lmodgrp	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Grp}$$
15	4 13 14	3syl	$$⊢\phi \to W\in \mathrm{Grp}$$
16	2 10	grpsubcl	$$⊢\left(W\in \mathrm{Grp}\wedge X\in V\wedge Y\in V\right)\to X\underset{\dot{}}{-}Y\in V$$
17	15 11 12 16	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}Y\in V$$
18	1 2 3 4 5 6	tcphcphlem3	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}Y\in V\right)\to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)\in ℝ$$
19	17 18	mpdan	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)\in ℝ$$
20	1 2 3 4 5 6	tcphcphlem3	$$⊢\left(\phi \wedge X\in V\right)\to X\underset{\dot{}}{,}X\in ℝ$$
21	11 20	mpdan	$$⊢\phi \to X\underset{\dot{}}{,}X\in ℝ$$
22	1 2 3 4 5 6	tcphcphlem3	$$⊢\left(\phi \wedge Y\in V\right)\to Y\underset{\dot{}}{,}Y\in ℝ$$
23	12 22	mpdan	$$⊢\phi \to Y\underset{\dot{}}{,}Y\in ℝ$$
24	21 23	readdcld	$$⊢\phi \to \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)\in ℝ$$
25	1 2 3 4 5	phclm	$$⊢\phi \to W\in \mathrm{CMod}$$
26	3 9	clmsscn	$$⊢W\in \mathrm{CMod}\to K\subseteq ℂ$$
27	25 26	syl	$$⊢\phi \to K\subseteq ℂ$$
28	3 6 2 9	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge X\in V\wedge Y\in V\right)\to X\underset{\dot{}}{,}Y\in K$$
29	4 11 12 28	syl3anc	$$⊢\phi \to X\underset{\dot{}}{,}Y\in K$$
30	27 29	sseldd	$$⊢\phi \to X\underset{\dot{}}{,}Y\in ℂ$$
31	3 6 2 9	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge Y\in V\wedge X\in V\right)\to Y\underset{\dot{}}{,}X\in K$$
32	4 12 11 31	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{,}X\in K$$
33	27 32	sseldd	$$⊢\phi \to Y\underset{\dot{}}{,}X\in ℂ$$
34	30 33	addcld	$$⊢\phi \to \left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\in ℂ$$
35	34	abscld	$$⊢\phi \to \left|\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right|\in ℝ$$
36	24 35	readdcld	$$⊢\phi \to \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)+\left|\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right|\in ℝ$$
37	21	recnd	$$⊢\phi \to X\underset{\dot{}}{,}X\in ℂ$$
38		2re	$$⊢2\in ℝ$$
39		oveq12	$$⊢\left(x=X\wedge x=X\right)\to x\underset{\dot{}}{,}x=X\underset{\dot{}}{,}X$$
40	39	anidms	$$⊢x=X\to x\underset{\dot{}}{,}x=X\underset{\dot{}}{,}X$$
41	40	breq2d	$$⊢x=X\to \left(0\le x\underset{\dot{}}{,}x\leftrightarrow 0\le X\underset{\dot{}}{,}X\right)$$
42	8	ralrimiva	$$⊢\phi \to \forall x\in V0\le x\underset{\dot{}}{,}x$$
43	41 42 11	rspcdva	$$⊢\phi \to 0\le X\underset{\dot{}}{,}X$$
44	21 43	resqrtcld	$$⊢\phi \to \sqrt{X\underset{\dot{}}{,}X}\in ℝ$$
45		oveq12	$$⊢\left(x=Y\wedge x=Y\right)\to x\underset{\dot{}}{,}x=Y\underset{\dot{}}{,}Y$$
46	45	anidms	$$⊢x=Y\to x\underset{\dot{}}{,}x=Y\underset{\dot{}}{,}Y$$
47	46	breq2d	$$⊢x=Y\to \left(0\le x\underset{\dot{}}{,}x\leftrightarrow 0\le Y\underset{\dot{}}{,}Y\right)$$
48	47 42 12	rspcdva	$$⊢\phi \to 0\le Y\underset{\dot{}}{,}Y$$
49	23 48	resqrtcld	$$⊢\phi \to \sqrt{Y\underset{\dot{}}{,}Y}\in ℝ$$
50	44 49	remulcld	$$⊢\phi \to \sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}\in ℝ$$
51		remulcl	$$⊢\left(2\in ℝ\wedge \sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}\in ℝ\right)\to 2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}\in ℝ$$
52	38 50 51	sylancr	$$⊢\phi \to 2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}\in ℝ$$
53	52	recnd	$$⊢\phi \to 2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}\in ℂ$$
54	23	recnd	$$⊢\phi \to Y\underset{\dot{}}{,}Y\in ℂ$$
55	37 53 54	add32d	$$⊢\phi \to \left(X\underset{\dot{}}{,}X\right)+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}+\left(Y\underset{\dot{}}{,}Y\right)=\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}$$
56	24 52	readdcld	$$⊢\phi \to \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}\in ℝ$$
57	55 56	eqeltrd	$$⊢\phi \to \left(X\underset{\dot{}}{,}X\right)+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}+\left(Y\underset{\dot{}}{,}Y\right)\in ℝ$$
58		oveq12	$$⊢\left(x=X\underset{\dot{}}{-}Y\wedge x=X\underset{\dot{}}{-}Y\right)\to x\underset{\dot{}}{,}x=\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)$$
59	58	anidms	$$⊢x=X\underset{\dot{}}{-}Y\to x\underset{\dot{}}{,}x=\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)$$
60	59	breq2d	$$⊢x=X\underset{\dot{}}{-}Y\to \left(0\le x\underset{\dot{}}{,}x\leftrightarrow 0\le \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)\right)$$
61	60 42 17	rspcdva	$$⊢\phi \to 0\le \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)$$
62	19 61	absidd	$$⊢\phi \to \left|\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)\right|=\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)$$
63	3	clmadd	$$⊢W\in \mathrm{CMod}\to +={+}_F$$
64	25 63	syl	$$⊢\phi \to +={+}_F$$
65	64	oveqd	$$⊢\phi \to \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)=\left(X\underset{\dot{}}{,}X\right){+}_F\left(Y\underset{\dot{}}{,}Y\right)$$
66	64	oveqd	$$⊢\phi \to \left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)=\left(X\underset{\dot{}}{,}Y\right){+}_F\left(Y\underset{\dot{}}{,}X\right)$$
67	65 66	oveq12d	$$⊢\phi \to \left(\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)\right){-}_F\left(\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right)=\left(\left(X\underset{\dot{}}{,}X\right){+}_F\left(Y\underset{\dot{}}{,}Y\right)\right){-}_F\left(\left(X\underset{\dot{}}{,}Y\right){+}_F\left(Y\underset{\dot{}}{,}X\right)\right)$$
68	3 6 2 9	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge X\in V\wedge X\in V\right)\to X\underset{\dot{}}{,}X\in K$$
69	4 11 11 68	syl3anc	$$⊢\phi \to X\underset{\dot{}}{,}X\in K$$
70	3 6 2 9	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge Y\in V\wedge Y\in V\right)\to Y\underset{\dot{}}{,}Y\in K$$
71	4 12 12 70	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{,}Y\in K$$
72	3 9	clmacl	$$⊢\left(W\in \mathrm{CMod}\wedge X\underset{\dot{}}{,}X\in K\wedge Y\underset{\dot{}}{,}Y\in K\right)\to \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)\in K$$
73	25 69 71 72	syl3anc	$$⊢\phi \to \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)\in K$$
74	3 9	clmacl	$$⊢\left(W\in \mathrm{CMod}\wedge X\underset{\dot{}}{,}Y\in K\wedge Y\underset{\dot{}}{,}X\in K\right)\to \left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\in K$$
75	25 29 32 74	syl3anc	$$⊢\phi \to \left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\in K$$
76	3 9	clmsub	$$⊢\left(W\in \mathrm{CMod}\wedge \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)\in K\wedge \left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\in K\right)\to \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)-\left(\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right)=\left(\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)\right){-}_F\left(\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right)$$
77	25 73 75 76	syl3anc	$$⊢\phi \to \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)-\left(\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right)=\left(\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)\right){-}_F\left(\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right)$$
78		eqid	$$⊢{-}_F={-}_F$$
79		eqid	$$⊢{+}_F={+}_F$$
80	3 6 2 10 78 79 4 11 12 11 12	ip2subdi	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)=\left(\left(X\underset{\dot{}}{,}X\right){+}_F\left(Y\underset{\dot{}}{,}Y\right)\right){-}_F\left(\left(X\underset{\dot{}}{,}Y\right){+}_F\left(Y\underset{\dot{}}{,}X\right)\right)$$
81	67 77 80	3eqtr4rd	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)=\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)-\left(\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right)$$
82	81	fveq2d	$$⊢\phi \to \left|\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)\right|=\left|\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)-\left(\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right)\right|$$
83	62 82	eqtr3d	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)=\left|\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)-\left(\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right)\right|$$
84	27 73	sseldd	$$⊢\phi \to \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)\in ℂ$$
85	84 34	abs2dif2d	$$⊢\phi \to \left|\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)-\left(\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right)\right|\le \left|\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)\right|+\left|\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right|$$
86	83 85	eqbrtrd	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)\le \left|\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)\right|+\left|\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right|$$
87	21 23 43 48	addge0d	$$⊢\phi \to 0\le \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)$$
88	24 87	absidd	$$⊢\phi \to \left|\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)\right|=\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)$$
89	88	oveq1d	$$⊢\phi \to \left|\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)\right|+\left|\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right|=\left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)+\left|\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right|$$
90	86 89	breqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)\le \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)+\left|\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right|$$
91	30	abscld	$$⊢\phi \to \left|X\underset{\dot{}}{,}Y\right|\in ℝ$$
92		remulcl	$$⊢\left(2\in ℝ\wedge \left|X\underset{\dot{}}{,}Y\right|\in ℝ\right)\to 2\left|X\underset{\dot{}}{,}Y\right|\in ℝ$$
93	38 91 92	sylancr	$$⊢\phi \to 2\left|X\underset{\dot{}}{,}Y\right|\in ℝ$$
94	30 33	abstrid	$$⊢\phi \to \left|\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right|\le \left|X\underset{\dot{}}{,}Y\right|+\left|Y\underset{\dot{}}{,}X\right|$$
95	91	recnd	$$⊢\phi \to \left|X\underset{\dot{}}{,}Y\right|\in ℂ$$
96	95	2timesd	$$⊢\phi \to 2\left|X\underset{\dot{}}{,}Y\right|=\left|X\underset{\dot{}}{,}Y\right|+\left|X\underset{\dot{}}{,}Y\right|$$
97	30	abscjd	$$⊢\phi \to \left|\overline{X\underset{\dot{}}{,}Y}\right|=\left|X\underset{\dot{}}{,}Y\right|$$
98	3	clmcj	$$⊢W\in \mathrm{CMod}\to *={\mathrm{*}}_F$$
99	25 98	syl	$$⊢\phi \to *={\mathrm{*}}_F$$
100	99	fveq1d	$$⊢\phi \to \overline{X\underset{\dot{}}{,}Y}={\left(X\underset{\dot{}}{,}Y\right)}^{{\mathrm{*}}_F}$$
101		eqid	$$⊢{\mathrm{*}}_F={\mathrm{*}}_F$$
102	3 6 2 101	ipcj	$$⊢\left(W\in \mathrm{PreHil}\wedge X\in V\wedge Y\in V\right)\to {\left(X\underset{\dot{}}{,}Y\right)}^{{\mathrm{*}}_F}=Y\underset{\dot{}}{,}X$$
103	4 11 12 102	syl3anc	$$⊢\phi \to {\left(X\underset{\dot{}}{,}Y\right)}^{{\mathrm{*}}_F}=Y\underset{\dot{}}{,}X$$
104	100 103	eqtrd	$$⊢\phi \to \overline{X\underset{\dot{}}{,}Y}=Y\underset{\dot{}}{,}X$$
105	104	fveq2d	$$⊢\phi \to \left|\overline{X\underset{\dot{}}{,}Y}\right|=\left|Y\underset{\dot{}}{,}X\right|$$
106	97 105	eqtr3d	$$⊢\phi \to \left|X\underset{\dot{}}{,}Y\right|=\left|Y\underset{\dot{}}{,}X\right|$$
107	106	oveq2d	$$⊢\phi \to \left|X\underset{\dot{}}{,}Y\right|+\left|X\underset{\dot{}}{,}Y\right|=\left|X\underset{\dot{}}{,}Y\right|+\left|Y\underset{\dot{}}{,}X\right|$$
108	96 107	eqtrd	$$⊢\phi \to 2\left|X\underset{\dot{}}{,}Y\right|=\left|X\underset{\dot{}}{,}Y\right|+\left|Y\underset{\dot{}}{,}X\right|$$
109	94 108	breqtrrd	$$⊢\phi \to \left|\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right|\le 2\left|X\underset{\dot{}}{,}Y\right|$$
110		eqid	$$⊢\mathrm{norm}\left(G\right)=\mathrm{norm}\left(G\right)$$
111		eqid	$$⊢\frac{Y\underset{\dot{}}{,}X}{Y\underset{\dot{}}{,}Y}=\frac{Y\underset{\dot{}}{,}X}{Y\underset{\dot{}}{,}Y}$$
112	1 2 3 4 5 6 7 8 9 110 111 11 12	ipcau2	$$⊢\phi \to \left|X\underset{\dot{}}{,}Y\right|\le \mathrm{norm}\left(G\right)\left(X\right)\mathrm{norm}\left(G\right)\left(Y\right)$$
113	1 110 2 6	tcphnmval	$$⊢\left(W\in \mathrm{Grp}\wedge X\in V\right)\to \mathrm{norm}\left(G\right)\left(X\right)=\sqrt{X\underset{\dot{}}{,}X}$$
114	15 11 113	syl2anc	$$⊢\phi \to \mathrm{norm}\left(G\right)\left(X\right)=\sqrt{X\underset{\dot{}}{,}X}$$
115	1 110 2 6	tcphnmval	$$⊢\left(W\in \mathrm{Grp}\wedge Y\in V\right)\to \mathrm{norm}\left(G\right)\left(Y\right)=\sqrt{Y\underset{\dot{}}{,}Y}$$
116	15 12 115	syl2anc	$$⊢\phi \to \mathrm{norm}\left(G\right)\left(Y\right)=\sqrt{Y\underset{\dot{}}{,}Y}$$
117	114 116	oveq12d	$$⊢\phi \to \mathrm{norm}\left(G\right)\left(X\right)\mathrm{norm}\left(G\right)\left(Y\right)=\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}$$
118	112 117	breqtrd	$$⊢\phi \to \left|X\underset{\dot{}}{,}Y\right|\le \sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}$$
119	38	a1i	$$⊢\phi \to 2\in ℝ$$
120		2pos	$$⊢0<2$$
121	120	a1i	$$⊢\phi \to 0<2$$
122		lemul2	$$⊢\left(\left|X\underset{\dot{}}{,}Y\right|\in ℝ\wedge \sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\left|X\underset{\dot{}}{,}Y\right|\le \sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}\leftrightarrow 2\left|X\underset{\dot{}}{,}Y\right|\le 2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}\right)$$
123	91 50 119 121 122	syl112anc	$$⊢\phi \to \left(\left|X\underset{\dot{}}{,}Y\right|\le \sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}\leftrightarrow 2\left|X\underset{\dot{}}{,}Y\right|\le 2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}\right)$$
124	118 123	mpbid	$$⊢\phi \to 2\left|X\underset{\dot{}}{,}Y\right|\le 2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}$$
125	35 93 52 109 124	letrd	$$⊢\phi \to \left|\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right|\le 2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}$$
126	35 52 24 125	leadd2dd	$$⊢\phi \to \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)+\left|\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right|\le \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}$$
127	126 55	breqtrrd	$$⊢\phi \to \left(X\underset{\dot{}}{,}X\right)+\left(Y\underset{\dot{}}{,}Y\right)+\left|\left(X\underset{\dot{}}{,}Y\right)+\left(Y\underset{\dot{}}{,}X\right)\right|\le \left(X\underset{\dot{}}{,}X\right)+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}+\left(Y\underset{\dot{}}{,}Y\right)$$
128	19 36 57 90 127	letrd	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)\le \left(X\underset{\dot{}}{,}X\right)+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}+\left(Y\underset{\dot{}}{,}Y\right)$$
129	19	recnd	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)\in ℂ$$
130	129	sqsqrtd	$$⊢\phi \to {\sqrt{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)}}^2=\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)$$
131	37	sqrtcld	$$⊢\phi \to \sqrt{X\underset{\dot{}}{,}X}\in ℂ$$
132	49	recnd	$$⊢\phi \to \sqrt{Y\underset{\dot{}}{,}Y}\in ℂ$$
133		binom2	$$⊢\left(\sqrt{X\underset{\dot{}}{,}X}\in ℂ\wedge \sqrt{Y\underset{\dot{}}{,}Y}\in ℂ\right)\to {\left(\sqrt{X\underset{\dot{}}{,}X}+\sqrt{Y\underset{\dot{}}{,}Y}\right)}^2={\sqrt{X\underset{\dot{}}{,}X}}^2+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}+{\sqrt{Y\underset{\dot{}}{,}Y}}^2$$
134	131 132 133	syl2anc	$$⊢\phi \to {\left(\sqrt{X\underset{\dot{}}{,}X}+\sqrt{Y\underset{\dot{}}{,}Y}\right)}^2={\sqrt{X\underset{\dot{}}{,}X}}^2+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}+{\sqrt{Y\underset{\dot{}}{,}Y}}^2$$
135	37	sqsqrtd	$$⊢\phi \to {\sqrt{X\underset{\dot{}}{,}X}}^2=X\underset{\dot{}}{,}X$$
136	135	oveq1d	$$⊢\phi \to {\sqrt{X\underset{\dot{}}{,}X}}^2+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}=\left(X\underset{\dot{}}{,}X\right)+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}$$
137	54	sqsqrtd	$$⊢\phi \to {\sqrt{Y\underset{\dot{}}{,}Y}}^2=Y\underset{\dot{}}{,}Y$$
138	136 137	oveq12d	$$⊢\phi \to {\sqrt{X\underset{\dot{}}{,}X}}^2+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}+{\sqrt{Y\underset{\dot{}}{,}Y}}^2=\left(X\underset{\dot{}}{,}X\right)+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}+\left(Y\underset{\dot{}}{,}Y\right)$$
139	134 138	eqtrd	$$⊢\phi \to {\left(\sqrt{X\underset{\dot{}}{,}X}+\sqrt{Y\underset{\dot{}}{,}Y}\right)}^2=\left(X\underset{\dot{}}{,}X\right)+2\sqrt{X\underset{\dot{}}{,}X}\sqrt{Y\underset{\dot{}}{,}Y}+\left(Y\underset{\dot{}}{,}Y\right)$$
140	128 130 139	3brtr4d	$$⊢\phi \to {\sqrt{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)}}^2\le {\left(\sqrt{X\underset{\dot{}}{,}X}+\sqrt{Y\underset{\dot{}}{,}Y}\right)}^2$$
141	19 61	resqrtcld	$$⊢\phi \to \sqrt{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)}\in ℝ$$
142	44 49	readdcld	$$⊢\phi \to \sqrt{X\underset{\dot{}}{,}X}+\sqrt{Y\underset{\dot{}}{,}Y}\in ℝ$$
143	19 61	sqrtge0d	$$⊢\phi \to 0\le \sqrt{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)}$$
144	21 43	sqrtge0d	$$⊢\phi \to 0\le \sqrt{X\underset{\dot{}}{,}X}$$
145	23 48	sqrtge0d	$$⊢\phi \to 0\le \sqrt{Y\underset{\dot{}}{,}Y}$$
146	44 49 144 145	addge0d	$$⊢\phi \to 0\le \sqrt{X\underset{\dot{}}{,}X}+\sqrt{Y\underset{\dot{}}{,}Y}$$
147	141 142 143 146	le2sqd	$$⊢\phi \to \left(\sqrt{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)}\le \sqrt{X\underset{\dot{}}{,}X}+\sqrt{Y\underset{\dot{}}{,}Y}\leftrightarrow {\sqrt{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)}}^2\le {\left(\sqrt{X\underset{\dot{}}{,}X}+\sqrt{Y\underset{\dot{}}{,}Y}\right)}^2\right)$$
148	140 147	mpbird	$$⊢\phi \to \sqrt{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{-}Y\right)}\le \sqrt{X\underset{\dot{}}{,}X}+\sqrt{Y\underset{\dot{}}{,}Y}$$