Theorem norm-ii 8925

Description: Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97.

Hypotheses

Ref	Expression
norm-ii.1	|- A e. H~
norm-ii.2	|- B e. H~

Assertion

Ref	Expression
norm-ii	|- (normh` (A +h B)) <_ ((normh` A) + (normh` B))

Proof of Theorem norm-ii

Step	Hyp	Ref	Expression
1		1re 5407	. . . . . . . . . . 11 |- 1 e. RR
2		ax1cn 5241	. . . . . . . . . . . 12 |- 1 e. CC
3	2	cjreb 6716	. . . . . . . . . . 11 |- (1 e. RR <-> (*` 1) = 1)
4	1, 3	mpbi 189	. . . . . . . . . 10 |- (*` 1) = 1
5	4	opreq1i 3956	. . . . . . . . 9 |- ((*` 1) x. (B .ih A)) = (1 x. (B .ih A))
6		norm-ii.2	. . . . . . . . . . 11 |- B e. H~
7		norm-ii.1	. . . . . . . . . . 11 |- A e. H~
8	6, 7	hicl 8869	. . . . . . . . . 10 |- (B .ih A) e. CC
9	8	mulid2 5305	. . . . . . . . 9 |- (1 x. (B .ih A)) = (B .ih A)
10	5, 9	eqtr 1487	. . . . . . . 8 |- ((*` 1) x. (B .ih A)) = (B .ih A)
11	7, 6	hicl 8869	. . . . . . . . 9 |- (A .ih B) e. CC
12	11	mulid2 5305	. . . . . . . 8 |- (1 x. (A .ih B)) = (A .ih B)
13	10, 12	opreq12i 3958	. . . . . . 7 |- (((*` 1) x. (B .ih A)) + (1 x. (A .ih B))) = ((B .ih A) + (A .ih B))
14		0re 5412	. . . . . . . . . 10 |- 0 e. RR
15		lt01 5653	. . . . . . . . . 10 |- 0 < 1
16	14, 1, 15	ltlei 5554	. . . . . . . . 9 |- 0 <_ 1
17	1	absid 6796	. . . . . . . . 9 |- (0 <_ 1 -> (abs` 1) = 1)
18	16, 17	ax-mp 7	. . . . . . . 8 |- (abs` 1) = 1
19	2, 6, 7, 18	normlem7 8903	. . . . . . 7 |- (((*` 1) x. (B .ih A)) + (1 x. (A .ih B))) <_ (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B))))
20	13, 19	eqbrtrr 2626	. . . . . 6 |- ((B .ih A) + (A .ih B)) <_ (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B))))
21		eqid 1468	. . . . . . . . . 10 |- -u(((*` 1) x. (B .ih A)) + (1 x. (A .ih B))) = -u(((*` 1) x. (B .ih A)) + (1 x. (A .ih B)))
22	2, 6, 7, 21	normlem2 8898	. . . . . . . . 9 |- -u(((*` 1) x. (B .ih A)) + (1 x. (A .ih B))) e. RR
23	2	cjcl 6699	. . . . . . . . . . . 12 |- (*` 1) e. CC
24	23, 8	mulcl 5293	. . . . . . . . . . 11 |- ((*` 1) x. (B .ih A)) e. CC
25	2, 11	mulcl 5293	. . . . . . . . . . 11 |- (1 x. (A .ih B)) e. CC
26	24, 25	addcl 5292	. . . . . . . . . 10 |- (((*` 1) x. (B .ih A)) + (1 x. (A .ih B))) e. CC
27	26	negreb 6730	. . . . . . . . 9 |- (-u(((*` 1) x. (B .ih A)) + (1 x. (A .ih B))) e. RR <-> (((*` 1) x. (B .ih A)) + (1 x. (A .ih B))) e. RR)
28	22, 27	mpbi 189	. . . . . . . 8 |- (((*` 1) x. (B .ih A)) + (1 x. (A .ih B))) e. RR
29	13, 28	eqeltrr 1537	. . . . . . 7 |- ((B .ih A) + (A .ih B)) e. RR
30		2re 5926	. . . . . . . 8 |- 2 e. RR
31		hiidge0t 8885	. . . . . . . . . . 11 |- (A e. H~ -> 0 <_ (A .ih A))
32	7, 31	ax-mp 7	. . . . . . . . . 10 |- 0 <_ (A .ih A)
33		hiidrclt 8882	. . . . . . . . . . . 12 |- (A e. H~ -> (A .ih A) e. RR)
34	7, 33	ax-mp 7	. . . . . . . . . . 11 |- (A .ih A) e. RR
35	34	sqrcl 6630	. . . . . . . . . 10 |- (0 <_ (A .ih A) -> (sqr` (A .ih A)) e. RR)
36	32, 35	ax-mp 7	. . . . . . . . 9 |- (sqr` (A .ih A)) e. RR
37		hiidge0t 8885	. . . . . . . . . . 11 |- (B e. H~ -> 0 <_ (B .ih B))
38	6, 37	ax-mp 7	. . . . . . . . . 10 |- 0 <_ (B .ih B)
39		hiidrclt 8882	. . . . . . . . . . . 12 |- (B e. H~ -> (B .ih B) e. RR)
40	6, 39	ax-mp 7	. . . . . . . . . . 11 |- (B .ih B) e. RR
41	40	sqrcl 6630	. . . . . . . . . 10 |- (0 <_ (B .ih B) -> (sqr` (B .ih B)) e. RR)
42	38, 41	ax-mp 7	. . . . . . . . 9 |- (sqr` (B .ih B)) e. RR
43	36, 42	remulcl 5307	. . . . . . . 8 |- ((sqr` (A .ih A)) x. (sqr` (B .ih B))) e. RR
44	30, 43	remulcl 5307	. . . . . . 7 |- (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B)))) e. RR
45	34, 40	readdcl 5306	. . . . . . 7 |- ((A .ih A) + (B .ih B)) e. RR
46	29, 44, 45	leadd2 5567	. . . . . 6 |- (((B .ih A) + (A .ih B)) <_ (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B)))) <-> (((A .ih A) + (B .ih B)) + ((B .ih A) + (A .ih B))) <_ (((A .ih A) + (B .ih B)) + (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B))))))
47	20, 46	mpbi 189	. . . . 5 |- (((A .ih A) + (B .ih B)) + ((B .ih A) + (A .ih B))) <_ (((A .ih A) + (B .ih B)) + (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B)))))
48	7, 6, 7, 6	normlem8 8904	. . . . . 6 |- ((A +h B) .ih (A +h B)) = (((A .ih A) + (B .ih B)) + ((A .ih B) + (B .ih A)))
49	11, 8	addcom 5294	. . . . . . 7 |- ((A .ih B) + (B .ih A)) = ((B .ih A) + (A .ih B))
50	49	opreq2i 3957	. . . . . 6 |- (((A .ih A) + (B .ih B)) + ((A .ih B) + (B .ih A))) = (((A .ih A) + (B .ih B)) + ((B .ih A) + (A .ih B)))
51	48, 50	eqtr 1487	. . . . 5 |- ((A +h B) .ih (A +h B)) = (((A .ih A) + (B .ih B)) + ((B .ih A) + (A .ih B)))
52	36	recn 5286	. . . . . . 7 |- (sqr` (A .ih A)) e. CC
53	42	recn 5286	. . . . . . 7 |- (sqr` (B .ih B)) e. CC
54	52, 53	binom2 6575	. . . . . 6 |- (((sqr` (A .ih A)) + (sqr` (B .ih B)))^2) = ((((sqr` (A .ih A))^2) + (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B))))) + ((sqr` (B .ih B))^2))
55	52	sqcl 6545	. . . . . . 7 |- ((sqr` (A .ih A))^2) e. CC
56		2cn 5927	. . . . . . . 8 |- 2 e. CC
57	52, 53	mulcl 5293	. . . . . . . 8 |- ((sqr` (A .ih A)) x. (sqr` (B .ih B))) e. CC
58	56, 57	mulcl 5293	. . . . . . 7 |- (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B)))) e. CC
59	53	sqcl 6545	. . . . . . 7 |- ((sqr` (B .ih B))^2) e. CC
60	55, 58, 59	add23 5313	. . . . . 6 |- ((((sqr` (A .ih A))^2) + (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B))))) + ((sqr` (B .ih B))^2)) = ((((sqr` (A .ih A))^2) + ((sqr` (B .ih B))^2)) + (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B)))))
61	34	sqsqr 6651	. . . . . . . . 9 |- (0 <_ (A .ih A) -> ((sqr` (A .ih A))^2) = (A .ih A))
62	32, 61	ax-mp 7	. . . . . . . 8 |- ((sqr` (A .ih A))^2) = (A .ih A)
63	40	sqsqr 6651	. . . . . . . . 9 |- (0 <_ (B .ih B) -> ((sqr` (B .ih B))^2) = (B .ih B))
64	38, 63	ax-mp 7	. . . . . . . 8 |- ((sqr` (B .ih B))^2) = (B .ih B)
65	62, 64	opreq12i 3958	. . . . . . 7 |- (((sqr` (A .ih A))^2) + ((sqr` (B .ih B))^2)) = ((A .ih A) + (B .ih B))
66	65	opreq1i 3956	. . . . . 6 |- ((((sqr` (A .ih A))^2) + ((sqr` (B .ih B))^2)) + (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B))))) = (((A .ih A) + (B .ih B)) + (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B)))))
67	54, 60, 66	3eqtr 1491	. . . . 5 |- (((sqr` (A .ih A)) + (sqr` (B .ih B)))^2) = (((A .ih A) + (B .ih B)) + (2 x. ((sqr` (A .ih A)) x. (sqr` (B .ih B)))))
68	47, 51, 67	3brtr4 2633	. . . 4 |- ((A +h B) .ih (A +h B)) <_ (((sqr` (A .ih A)) + (sqr` (B .ih B)))^2)
69	7, 6	hvaddcl 8809	. . . . . 6 |- (A +h B) e. H~
70		hiidge0t 8885	. . . . . 6 |- ((A +h B) e. H~ -> 0 <_ ((A +h B) .ih (A +h B)))
71	69, 70	ax-mp 7	. . . . 5 |- 0 <_ ((A +h B) .ih (A +h B))
72	36, 42	readdcl 5306	. . . . . 6 |- ((sqr` (A .ih A)) + (sqr` (B .ih B))) e. RR
73	72	sqge0 6559	. . . . 5 |- 0 <_ (((sqr` (A .ih A)) + (sqr` (B .ih B)))^2)
74		hiidrclt 8882	. . . . . . 7 |- ((A +h B) e. H~ -> ((A +h B) .ih (A +h B))