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	⊢ 𝐴 ∈ ℋ
	norm-ii.2	⊢ 𝐵 ∈ ℋ
Assertion	norm-ii-i	⊢ ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ≤ ( ( normℎ ‘ 𝐴 ) + ( normℎ ‘ 𝐵 ) )

Proof

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