Theorem norm-ii 5086

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	|- (norm` (A +v B)) <_ ((norm` A) + (norm` B))

Proof of Theorem norm-ii

Step	Hyp	Ref	Expression
1		ax1re 4064	. . . . . . . . . . 11 |- 1 e. RR
2		1cn 4101	. . . . . . . . . . . 12 |- 1 e. CC
3	2	cjre 4811	. . . . . . . . . . 11 |- (1 e. RR <-> (*` 1) = 1)
4	1, 3	mpbi 164	. . . . . . . . . 10 |- (*` 1) = 1
5	4	opreq1i 3009	. . . . . . . . 9 |- ((*` 1) x. (B .i A)) = (1 x. (B .i A))
6		norm-ii.2	. . . . . . . . . . 11 |- B e. H~
7		norm-ii.1	. . . . . . . . . . 11 |- A e. H~
8	6, 7	hicl 5044	. . . . . . . . . 10 |- (B .i A) e. CC
9	8	mulid2 4115	. . . . . . . . 9 |- (1 x. (B .i A)) = (B .i A)
10	5, 9	eqtr 1119	. . . . . . . 8 |- ((*` 1) x. (B .i A)) = (B .i A)
11	7, 6	hicl 5044	. . . . . . . . 9 |- (A .i B) e. CC
12	11	mulid2 4115	. . . . . . . 8 |- (1 x. (A .i B)) = (A .i B)
13	10, 12	opreq12i 3011	. . . . . . 7 |- (((*` 1) x. (B .i A)) + (1 x. (A .i B))) = ((B .i A) + (A .i B))
14		ax0re 4063	. . . . . . . . . 10 |- 0 e. RR
15		lt01 4377	. . . . . . . . . 10 |- 0 < 1
16	14, 1, 15	ltlei 4303	. . . . . . . . 9 |- 0 <_ 1
17	1	absid 4850	. . . . . . . . 9 |- (0 <_ 1 -> (abs` 1) = 1)
18	16, 17	ax-mp 6	. . . . . . . 8 |- (abs` 1) = 1
19	2, 6, 7, 18	normlem7 5069	. . . . . . 7 |- (((*` 1) x. (B .i A)) + (1 x. (A .i B))) <_ (2 x. ((sqr` (A .i A)) x. (sqr` (B .i B))))
20	13, 19	eqbrtrr 2078	. . . . . 6 |- ((B .i A) + (A .i B)) <_ (2 x. ((sqr` (A .i A)) x. (sqr` (B .i B))))
21		cleqid 1102	. . . . . . . . . 10 |- -u(((*` 1) x. (B .i A)) + (1 x. (A .i B))) = -u(((*` 1) x. (B .i A)) + (1 x. (A .i B)))
22	2, 6, 7, 21	normlem2 5064	. . . . . . . . 9 |- -u(((*` 1) x. (B .i A)) + (1 x. (A .i B))) e. RR
23	2	cjcl 4804	. . . . . . . . . . . 12 |- (*` 1) e. CC
24	23, 8	mulcl 4105	. . . . . . . . . . 11 |- ((*` 1) x. (B .i A)) e. CC
25	2, 11	mulcl 4105	. . . . . . . . . . 11 |- (1 x. (A .i B)) e. CC
26	24, 25	addcl 4104	. . . . . . . . . 10 |- (((*` 1) x. (B .i A)) + (1 x. (A .i B))) e. CC
27	26	negre 4825	. . . . . . . . 9 |- (-u(((*` 1) x. (B .i A)) + (1 x. (A .i B))) e. RR <-> (((*` 1) x. (B .i A)) + (1 x. (A .i B))) e. RR)
28	22, 27	mpbi 164	. . . . . . . 8 |- (((*` 1) x. (B .i A)) + (1 x. (A .i B))) e. RR
29	13, 28	eqeltrr 1160	. . . . . . 7 |- ((B .i A) + (A .i B)) e. RR
30		2re 4470	. . . . . . . 8 |- 2 e. RR
31		hiidge0t 5056	. . . . . . . . . . 11 |- (A e. H~ -> 0 <_ (A .i A))
32	7, 31	ax-mp 6	. . . . . . . . . 10 |- 0 <_ (A .i A)
33		hiidrclt 5053	. . . . . . . . . . . 12 |- (A e. H~ -> (A .i A) e. RR)
34	7, 33	ax-mp 6	. . . . . . . . . . 11 |- (A .i A) e. RR
35	34	sqrcl 4758	. . . . . . . . . 10 |- (0 <_ (A .i A) -> (sqr` (A .i A)) e. RR)
36	32, 35	ax-mp 6	. . . . . . . . 9 |- (sqr` (A .i A)) e. RR
37		hiidge0t 5056	. . . . . . . . . . 11 |- (B e. H~ -> 0 <_ (B .i B))
38	6, 37	ax-mp 6	. . . . . . . . . 10 |- 0 <_ (B .i B)
39		hiidrclt 5053	. . . . . . . . . . . 12 |- (B e. H~ -> (B .i B) e. RR)
40	6, 39	ax-mp 6	. . . . . . . . . . 11 |- (B .i B) e. RR
41	40	sqrcl 4758	. . . . . . . . . 10 |- (0 <_ (B .i B) -> (sqr` (B .i B)) e. RR)
42	38, 41	ax-mp 6	. . . . . . . . 9 |- (sqr` (B .i B)) e. RR
43	36, 42	remulcl 4119	. . . . . . . 8 |- ((sqr` (A .i A)) x. (sqr` (B .i B))) e. RR
44	30, 43	remulcl 4119	. . . . . . 7 |- (2 x. ((sqr` (A .i A)) x. (sqr` (B .i B)))) e. RR
45	34, 40	readdcl 4118	. . . . . . 7 |- ((A .i A) + (B .i B)) e. RR
46	29, 44, 45	leadd2 4315	. . . . . 6 |- (((B .i A) + (A .i B)) <_ (2 x. ((sqr` (A .i A)) x. (sqr` (B .i B)))) <-> (((A .i A) + (B .i B)) + ((B .i A) + (A .i B))) <_ (((A .i A) + (B .i B)) + (2 x. ((sqr` (A .i A)) x. (sqr` (B .i B))))))
47	20, 46	mpbi 164	. . . . 5 |- (((A .i A) + (B .i B)) + ((B .i A) + (A .i B))) <_ (((A .i A) + (B .i B)) + (2 x. ((sqr` (A .i A)) x. (sqr` (B .i B)))))
48	7, 6	hvaddcl 4999	. . . . . . 7 |- (A +v B) e. H~
49		his7 5051	. . . . . . 7 |- (((A +v B) e. H~ /\ A e. H~ /\ B e. H~) -> ((A +v B) .i (A +v B)) = (((A +v B) .i A) + ((A +v B) .i B)))
50	48, 7, 6, 49	mp3an 642	. . . . . 6 |- ((A +v B) .i (A +v B)) = (((A +v B) .i A) + ((A +v B) .i B))
51		ax-his2 5046	. . . . . . . . 9 |- ((A e. H~ /\ B e. H~ /\ A e. H~) -> ((A +v B) .i A) = ((A .i A) + (B .i A)))
52	7, 6, 7, 51	mp3an 642	. . . . . . . 8 |- ((A +v B) .i A) = ((A .i A) + (B .i A))
53		ax-his2 5046	. . . . . . . . 9 |- ((A e. H~ /\ B e. H~ /\ B e. H~) -> ((A +v B) .i B) = ((A .i B) + (B .i B)))
54	7, 6, 6, 53	mp3an 642	. . . . . . . 8 |- ((A +v B) .i B) = ((A .i B) + (B .i B))
55	52, 54	opreq12i 3011	. . . . . . 7 |- (((A +v B) .i A) + ((A +v B) .i B)) = (((A .i A) + (B .i A)) + ((A .i B) + (B .i B)))
56	7, 7	hicl 5044	. . . . . . . . 9 |- (A .i A) e. CC
57	56, 8	addcl 4104	. . . . . . . 8 |- ((A .i A) + (B .i A)) e. CC
58	6, 6	hicl 5044	. . . . . . . 8 |- (B .i B) e. CC
59	57, 11, 58	addass 4108	. . . . . . 7 |- ((((A .i A) + (B .i A)) + (A .i B)) + (B .i B)) = (((A .i A) + (B .i A)) + ((A .i B) + (B .i B)))
60	55, 59	eqtr4 1122	. . . . . 6 |- (((A +v B) .i A) + ((A +v B) .i B)) = ((((A .i A) + (B .i A)) + (A .i B)) + (B .i B))
61	56, 8, 11	addass 4108	. . . . . . . 8 |- (((A .i A) + (B .i A)) + (A .i B)) = ((A .i A) + ((B .i A) + (A .i B)))
62	61	opreq1i 3009	. . . . . . 7 |- ((((A .i A) + (B .i A)) + (A .i B)) + (B .i B)) = (((A .i A) + ((B .i A) + (A .i B))) + (B .i B))
63	8, 11	addcl 4104	. . . . . . . 8 |- ((B .i A) + (A .i B)) e. CC
64	56, 63, 58	add23 4129	. . . . . . 7 |- (((A .i A) + ((B .i A) + (A .i B))) + (B .i B)) = (((A .i A) + (B .i B)) + ((B .i A) + (A .i B)))
65	62, 64	eqtr 1119	. . . . . 6 |- ((((A .i A) + (B .i A)) + (A .i B)) + (B .i B)) = (((A .i A) + (B .i B)) + ((B .i A) + (A .i B)))
66	50, 60, 65	3eqtr 1123	. . . . 5 |- ((A +v B) .i (A +v B)) = (((A .i A) + (B .i B)) + ((B .i A) + (A .i B)))
67	36	recn 4098	. . . . . . 7 |- (sqr` (A .i A)) e. CC
68	42	recn 4098	. . . . . . 7 |- (sqr` (B .i B)) e. CC
69	67, 68	binom 4712	. . . . . 6 |- (((sqr` (A .i A)) + (sqr` (B .i B)))^2) = ((((sqr` (A .i A))^2) + (2 x. ((sqr` (A .i A)) x. (sqr` (B .i B))))) + ((sqr` (B .i B))^2))
70	67	sqcl 4686	. . . . . . 7 |- ((sqr` (A .i A))^2) e. CC
71		2cn 4471	. . . . . . . 8 |- 2 e. CC
72	67, 68	mulcl 4105	. . . . . . . 8 |- ((sqr` (A .i A)) x. (sqr` (B .i B))) e. CC
73	71, 72	mulcl 4105	. . . . . . 7 |- (2 x. ((sqr` (A .i A)) x. (sqr` (B .i B)))) e. CC
74	68	sqcl 4686	. . . . . . 7 |- ((sqr` (B .i B))^2) e. CC
75	70, 73, 74	add23 4129	. . . . . 6 |- ((((sqr` (A .i A))^2) + (2 x. ((sqr` (A .i A)) x. (sqr` (B .i B))))) + ((sqr` (B .i B))^2)) = ((((sqr` (A .i A))^2) + ((sqr` (B .i B))^2)) + (2 x. ((sqr` (A .i A)) x. (sqr` (B .i B)))))
76	34	sqsqr 4775	. . . . . . . . 9 |- (0 <_ (A .i A) -> ((sqr` (A .i A))^2