Theorem norm-ii-i

Description: Triangle inequality for norms. Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 11-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	norm-ii.1	$$⊢A\in \mathscr{H}$$
	norm-ii.2	$$⊢B\in \mathscr{H}$$
Assertion	norm-ii-i	$$⊢{norm}_{ℎ}\left(A{+}_{ℎ}B\right)\le {norm}_{ℎ}\left(A\right)+{norm}_{ℎ}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		norm-ii.1	$$⊢A\in \mathscr{H}$$
2		norm-ii.2	$$⊢B\in \mathscr{H}$$
3		1re	$$⊢1\in ℝ$$
4		ax-1cn	$$⊢1\in ℂ$$
5	4	cjrebi	$$⊢1\in ℝ\leftrightarrow \bar{1}=1$$
6	3 5	mpbi	$$⊢\bar{1}=1$$
7	6	oveq1i	$$⊢\bar{1}\left(B{\cdot }_{\mathrm{ih}}A\right)=1\left(B{\cdot }_{\mathrm{ih}}A\right)$$
8	2 1	hicli	$$⊢B{\cdot }_{\mathrm{ih}}A\in ℂ$$
9	8	mullidi	$$⊢1\left(B{\cdot }_{\mathrm{ih}}A\right)=B{\cdot }_{\mathrm{ih}}A$$
10	7 9	eqtri	$$⊢\bar{1}\left(B{\cdot }_{\mathrm{ih}}A\right)=B{\cdot }_{\mathrm{ih}}A$$
11	1 2	hicli	$$⊢A{\cdot }_{\mathrm{ih}}B\in ℂ$$
12	11	mullidi	$$⊢1\left(A{\cdot }_{\mathrm{ih}}B\right)=A{\cdot }_{\mathrm{ih}}B$$
13	10 12	oveq12i	$$⊢\bar{1}\left(B{\cdot }_{\mathrm{ih}}A\right)+1\left(A{\cdot }_{\mathrm{ih}}B\right)=\left(B{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)$$
14		abs1	$$⊢\left|1\right|=1$$
15	4 2 1 14	normlem7	$$⊢\bar{1}\left(B{\cdot }_{\mathrm{ih}}A\right)+1\left(A{\cdot }_{\mathrm{ih}}B\right)\le 2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
16	13 15	eqbrtrri	$$⊢\left(B{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)\le 2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
17		eqid	$$⊢-\left(\bar{1}\left(B{\cdot }_{\mathrm{ih}}A\right)+1\left(A{\cdot }_{\mathrm{ih}}B\right)\right)=-\left(\bar{1}\left(B{\cdot }_{\mathrm{ih}}A\right)+1\left(A{\cdot }_{\mathrm{ih}}B\right)\right)$$
18	4 2 1 17	normlem2	$$⊢-\left(\bar{1}\left(B{\cdot }_{\mathrm{ih}}A\right)+1\left(A{\cdot }_{\mathrm{ih}}B\right)\right)\in ℝ$$
19	4	cjcli	$$⊢\bar{1}\in ℂ$$
20	19 8	mulcli	$$⊢\bar{1}\left(B{\cdot }_{\mathrm{ih}}A\right)\in ℂ$$
21	4 11	mulcli	$$⊢1\left(A{\cdot }_{\mathrm{ih}}B\right)\in ℂ$$
22	20 21	addcli	$$⊢\bar{1}\left(B{\cdot }_{\mathrm{ih}}A\right)+1\left(A{\cdot }_{\mathrm{ih}}B\right)\in ℂ$$
23	22	negrebi	$$⊢-\left(\bar{1}\left(B{\cdot }_{\mathrm{ih}}A\right)+1\left(A{\cdot }_{\mathrm{ih}}B\right)\right)\in ℝ\leftrightarrow \bar{1}\left(B{\cdot }_{\mathrm{ih}}A\right)+1\left(A{\cdot }_{\mathrm{ih}}B\right)\in ℝ$$
24	18 23	mpbi	$$⊢\bar{1}\left(B{\cdot }_{\mathrm{ih}}A\right)+1\left(A{\cdot }_{\mathrm{ih}}B\right)\in ℝ$$
25	13 24	eqeltrri	$$⊢\left(B{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)\in ℝ$$
26		2re	$$⊢2\in ℝ$$
27		hiidge0	$$⊢A\in \mathscr{H}\to 0\le A{\cdot }_{\mathrm{ih}}A$$
28	1 27	ax-mp	$$⊢0\le A{\cdot }_{\mathrm{ih}}A$$
29		hiidrcl	$$⊢A\in \mathscr{H}\to A{\cdot }_{\mathrm{ih}}A\in ℝ$$
30	1 29	ax-mp	$$⊢A{\cdot }_{\mathrm{ih}}A\in ℝ$$
31	30	sqrtcli	$$⊢0\le A{\cdot }_{\mathrm{ih}}A\to \sqrt{A{\cdot }_{\mathrm{ih}}A}\in ℝ$$
32	28 31	ax-mp	$$⊢\sqrt{A{\cdot }_{\mathrm{ih}}A}\in ℝ$$
33		hiidge0	$$⊢B\in \mathscr{H}\to 0\le B{\cdot }_{\mathrm{ih}}B$$
34	2 33	ax-mp	$$⊢0\le B{\cdot }_{\mathrm{ih}}B$$
35		hiidrcl	$$⊢B\in \mathscr{H}\to B{\cdot }_{\mathrm{ih}}B\in ℝ$$
36	2 35	ax-mp	$$⊢B{\cdot }_{\mathrm{ih}}B\in ℝ$$
37	36	sqrtcli	$$⊢0\le B{\cdot }_{\mathrm{ih}}B\to \sqrt{B{\cdot }_{\mathrm{ih}}B}\in ℝ$$
38	34 37	ax-mp	$$⊢\sqrt{B{\cdot }_{\mathrm{ih}}B}\in ℝ$$
39	32 38	remulcli	$$⊢\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}\in ℝ$$
40	26 39	remulcli	$$⊢2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}\in ℝ$$
41	30 36	readdcli	$$⊢\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\in ℝ$$
42	25 40 41	leadd2i	$$⊢\left(B{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)\le 2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}\leftrightarrow \left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)\le \left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
43	16 42	mpbi	$$⊢\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)\le \left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
44	1 2 1 2	normlem8	$$⊢\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)$$
45	11 8	addcomi	$$⊢\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)=\left(B{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)$$
46	45	oveq2i	$$⊢\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)$$
47	44 46	eqtri	$$⊢\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)$$
48	32	recni	$$⊢\sqrt{A{\cdot }_{\mathrm{ih}}A}\in ℂ$$
49	38	recni	$$⊢\sqrt{B{\cdot }_{\mathrm{ih}}B}\in ℂ$$
50	48 49	binom2i	$$⊢{\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2={\sqrt{A{\cdot }_{\mathrm{ih}}A}}^2+2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}+{\sqrt{B{\cdot }_{\mathrm{ih}}B}}^2$$
51	48	sqcli	$$⊢{\sqrt{A{\cdot }_{\mathrm{ih}}A}}^2\in ℂ$$
52		2cn	$$⊢2\in ℂ$$
53	48 49	mulcli	$$⊢\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}\in ℂ$$
54	52 53	mulcli	$$⊢2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}\in ℂ$$
55	49	sqcli	$$⊢{\sqrt{B{\cdot }_{\mathrm{ih}}B}}^2\in ℂ$$
56	51 54 55	add32i	$$⊢{\sqrt{A{\cdot }_{\mathrm{ih}}A}}^2+2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}+{\sqrt{B{\cdot }_{\mathrm{ih}}B}}^2={\sqrt{A{\cdot }_{\mathrm{ih}}A}}^2+{\sqrt{B{\cdot }_{\mathrm{ih}}B}}^2+2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
57	30	sqsqrti	$$⊢0\le A{\cdot }_{\mathrm{ih}}A\to {\sqrt{A{\cdot }_{\mathrm{ih}}A}}^2=A{\cdot }_{\mathrm{ih}}A$$
58	28 57	ax-mp	$$⊢{\sqrt{A{\cdot }_{\mathrm{ih}}A}}^2=A{\cdot }_{\mathrm{ih}}A$$
59	36	sqsqrti	$$⊢0\le B{\cdot }_{\mathrm{ih}}B\to {\sqrt{B{\cdot }_{\mathrm{ih}}B}}^2=B{\cdot }_{\mathrm{ih}}B$$
60	34 59	ax-mp	$$⊢{\sqrt{B{\cdot }_{\mathrm{ih}}B}}^2=B{\cdot }_{\mathrm{ih}}B$$
61	58 60	oveq12i	$$⊢{\sqrt{A{\cdot }_{\mathrm{ih}}A}}^2+{\sqrt{B{\cdot }_{\mathrm{ih}}B}}^2=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)$$
62	61	oveq1i	$$⊢{\sqrt{A{\cdot }_{\mathrm{ih}}A}}^2+{\sqrt{B{\cdot }_{\mathrm{ih}}B}}^2+2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
63	50 56 62	3eqtri	$$⊢{\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+2\sqrt{A{\cdot }_{\mathrm{ih}}A}\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
64	43 47 63	3brtr4i	$$⊢\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\le {\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2$$
65	1 2	hvaddcli	$$⊢A{+}_{ℎ}B\in \mathscr{H}$$
66		hiidge0	$$⊢A{+}_{ℎ}B\in \mathscr{H}\to 0\le \left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)$$
67	65 66	ax-mp	$$⊢0\le \left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)$$
68	32 38	readdcli	$$⊢\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\in ℝ$$
69	68	sqge0i	$$⊢0\le {\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2$$
70		hiidrcl	$$⊢A{+}_{ℎ}B\in \mathscr{H}\to \left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\in ℝ$$
71	65 70	ax-mp	$$⊢\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\in ℝ$$
72	68	resqcli	$$⊢{\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2\in ℝ$$
73	71 72	sqrtlei	$$⊢\left(0\le \left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\wedge 0\le {\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2\right)\to \left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\le {\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2\leftrightarrow \sqrt{\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)}\le \sqrt{{\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2}\right)$$
74	67 69 73	mp2an	$$⊢\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\le {\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2\leftrightarrow \sqrt{\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)}\le \sqrt{{\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2}$$
75	64 74	mpbi	$$⊢\sqrt{\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)}\le \sqrt{{\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2}$$
76	30	sqrtge0i	$$⊢0\le A{\cdot }_{\mathrm{ih}}A\to 0\le \sqrt{A{\cdot }_{\mathrm{ih}}A}$$
77	28 76	ax-mp	$$⊢0\le \sqrt{A{\cdot }_{\mathrm{ih}}A}$$
78	36	sqrtge0i	$$⊢0\le B{\cdot }_{\mathrm{ih}}B\to 0\le \sqrt{B{\cdot }_{\mathrm{ih}}B}$$
79	34 78	ax-mp	$$⊢0\le \sqrt{B{\cdot }_{\mathrm{ih}}B}$$
80	32 38	addge0i	$$⊢\left(0\le \sqrt{A{\cdot }_{\mathrm{ih}}A}\wedge 0\le \sqrt{B{\cdot }_{\mathrm{ih}}B}\right)\to 0\le \sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
81	77 79 80	mp2an	$$⊢0\le \sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
82	68	sqrtsqi	$$⊢0\le \sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\to \sqrt{{\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2}=\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
83	81 82	ax-mp	$$⊢\sqrt{{\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}\right)}^2}=\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
84	75 83	breqtri	$$⊢\sqrt{\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)}\le \sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
85		normval	$$⊢A{+}_{ℎ}B\in \mathscr{H}\to {norm}_{ℎ}\left(A{+}_{ℎ}B\right)=\sqrt{\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)}$$
86	65 85	ax-mp	$$⊢{norm}_{ℎ}\left(A{+}_{ℎ}B\right)=\sqrt{\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)}$$
87		normval	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(A\right)=\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
88	1 87	ax-mp	$$⊢{norm}_{ℎ}\left(A\right)=\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
89		normval	$$⊢B\in \mathscr{H}\to {norm}_{ℎ}\left(B\right)=\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
90	2 89	ax-mp	$$⊢{norm}_{ℎ}\left(B\right)=\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
91	88 90	oveq12i	$$⊢{norm}_{ℎ}\left(A\right)+{norm}_{ℎ}\left(B\right)=\sqrt{A{\cdot }_{\mathrm{ih}}A}+\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
92	84 86 91	3brtr4i	$$⊢{norm}_{ℎ}\left(A{+}_{ℎ}B\right)\le {norm}_{ℎ}\left(A\right)+{norm}_{ℎ}\left(B\right)$$