Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem norm-ii 5086

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

**Hypotheses**
Ref	Expression
norm-ii.1	⊢ A ∈ ℋ
norm-ii.2	⊢ B ∈ ℋ

**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 ∈ ℝ
2		1cn 4101	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
3	2	cjre 4811	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ ↔ (∗ ‘1) = 1)
4	1, 3	mpbi 164	. . . . . . . . . 10 ⊢ (∗ ‘1) = 1
5	4	opreq1i 3009	. . . . . . . . 9 ⊢ ((∗ ‘1) · (B ·_i A)) = (1 · (B ·_i A))
6		norm-ii.2	. . . . . . . . . . 11 ⊢ B ∈ ℋ
7		norm-ii.1	. . . . . . . . . . 11 ⊢ A ∈ ℋ
8	6, 7	hicl 5044	. . . . . . . . . 10 ⊢ (B ·_i A) ∈ ℂ
9	8	mulid2 4115	. . . . . . . . 9 ⊢ (1 · (B ·_i A)) = (B ·_i A)
10	5, 9	eqtr 1119	. . . . . . . 8 ⊢ ((∗ ‘1) · (B ·_i A)) = (B ·_i A)
11	7, 6	hicl 5044	. . . . . . . . 9 ⊢ (A ·_i B) ∈ ℂ
12	11	mulid2 4115	. . . . . . . 8 ⊢ (1 · (A ·_i B)) = (A ·_i B)
13	10, 12	opreq12i 3011	. . . . . . 7 ⊢ (((∗ ‘1) · (B ·_i A)) + (1 · (A ·_i B))) = ((B ·_i A) + (A ·_i B))
14		ax0re 4063	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
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) · (B ·_i A)) + (1 · (A ·_i B))) ≤ (2 · ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B))))
20	13, 19	eqbrtrr 2078	. . . . . 6 ⊢ ((B ·_i A) + (A ·_i B)) ≤ (2 · ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B))))
21		cleqid 1102	. . . . . . . . . 10 ⊢ -(((∗ ‘1) · (B ·_i A)) + (1 · (A ·_i B))) = -(((∗ ‘1) · (B ·_i A)) + (1 · (A ·_i B)))
22	2, 6, 7, 21	normlem2 5064	. . . . . . . . 9 ⊢ -(((∗ ‘1) · (B ·_i A)) + (1 · (A ·_i B))) ∈ ℝ
23	2	cjcl 4804	. . . . . . . . . . . 12 ⊢ (∗ ‘1) ∈ ℂ
24	23, 8	mulcl 4105	. . . . . . . . . . 11 ⊢ ((∗ ‘1) · (B ·_i A)) ∈ ℂ
25	2, 11	mulcl 4105	. . . . . . . . . . 11 ⊢ (1 · (A ·_i B)) ∈ ℂ
26	24, 25	addcl 4104	. . . . . . . . . 10 ⊢ (((∗ ‘1) · (B ·_i A)) + (1 · (A ·_i B))) ∈ ℂ
27	26	negre 4825	. . . . . . . . 9 ⊢ (-(((∗ ‘1) · (B ·_i A)) + (1 · (A ·_i B))) ∈ ℝ ↔ (((∗ ‘1) · (B ·_i A)) + (1 · (A ·_i B))) ∈ ℝ)
28	22, 27	mpbi 164	. . . . . . . 8 ⊢ (((∗ ‘1) · (B ·_i A)) + (1 · (A ·_i B))) ∈ ℝ
29	13, 28	eqeltrr 1160	. . . . . . 7 ⊢ ((B ·_i A) + (A ·_i B)) ∈ ℝ
30		2re 4470	. . . . . . . 8 ⊢ 2 ∈ ℝ
31		hiidge0t 5056	. . . . . . . . . . 11 ⊢ (A ∈ ℋ → 0 ≤ (A ·_i A))
32	7, 31	ax-mp 6	. . . . . . . . . 10 ⊢ 0 ≤ (A ·_i A)
33		hiidrclt 5053	. . . . . . . . . . . 12 ⊢ (A ∈ ℋ → (A ·_i A) ∈ ℝ)
34	7, 33	ax-mp 6	. . . . . . . . . . 11 ⊢ (A ·_i A) ∈ ℝ
35	34	sqrcl 4758	. . . . . . . . . 10 ⊢ (0 ≤ (A ·_i A) → (√ ‘(A ·_i A)) ∈ ℝ)
36	32, 35	ax-mp 6	. . . . . . . . 9 ⊢ (√ ‘(A ·_i A)) ∈ ℝ
37		hiidge0t 5056	. . . . . . . . . . 11 ⊢ (B ∈ ℋ → 0 ≤ (B ·_i B))
38	6, 37	ax-mp 6	. . . . . . . . . 10 ⊢ 0 ≤ (B ·_i B)
39		hiidrclt 5053	. . . . . . . . . . . 12 ⊢ (B ∈ ℋ → (B ·_i B) ∈ ℝ)
40	6, 39	ax-mp 6	. . . . . . . . . . 11 ⊢ (B ·_i B) ∈ ℝ
41	40	sqrcl 4758	. . . . . . . . . 10 ⊢ (0 ≤ (B ·_i B) → (√ ‘(B ·_i B)) ∈ ℝ)
42	38, 41	ax-mp 6	. . . . . . . . 9 ⊢ (√ ‘(B ·_i B)) ∈ ℝ
43	36, 42	remulcl 4119	. . . . . . . 8 ⊢ ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B))) ∈ ℝ
44	30, 43	remulcl 4119	. . . . . . 7 ⊢ (2 · ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B)))) ∈ ℝ
45	34, 40	readdcl 4118	. . . . . . 7 ⊢ ((A ·_i A) + (B ·_i B)) ∈ ℝ
46	29, 44, 45	leadd2 4315	. . . . . 6 ⊢ (((B ·_i A) + (A ·_i B)) ≤ (2 · ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B)))) ↔ (((A ·_i A) + (B ·_i B)) + ((B ·_i A) + (A ·_i B))) ≤ (((A ·_i A) + (B ·_i B)) + (2 · ((√ ‘(A ·_i A)) · (√ ‘(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 · ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B)))))
48	7, 6	hvaddcl 4999	. . . . . . 7 ⊢ (A +_v B) ∈ ℋ
49		his7 5051	. . . . . . 7 ⊢ (((A +_v B) ∈ ℋ ∧ A ∈ ℋ ∧ B ∈ ℋ ) → ((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 ∈ ℋ ∧ B ∈ ℋ ∧ A ∈ ℋ ) → ((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 ∈ ℋ ∧ B ∈ ℋ ∧ B ∈ ℋ ) → ((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) ∈ ℂ
57	56, 8	addcl 4104	. . . . . . . 8 ⊢ ((A ·_i A) + (B ·_i A)) ∈ ℂ
58	6, 6	hicl 5044	. . . . . . . 8 ⊢ (B ·_i B) ∈ ℂ
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)) ∈ ℂ
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 ⊢ (√ ‘(A ·_i A)) ∈ ℂ
68	42	recn 4098	. . . . . . 7 ⊢ (√ ‘(B ·_i B)) ∈ ℂ
69	67, 68	binom 4712	. . . . . 6 ⊢ (((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2) = ((((√ ‘(A ·_i A))↑2) + (2 · ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B))))) + ((√ ‘(B ·_i B))↑2))
70	67	sqcl 4686	. . . . . . 7 ⊢ ((√ ‘(A ·_i A))↑2) ∈ ℂ
71		2cn 4471	. . . . . . . 8 ⊢ 2 ∈ ℂ
72	67, 68	mulcl 4105	. . . . . . . 8 ⊢ ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B))) ∈ ℂ
73	71, 72	mulcl 4105	. . . . . . 7 ⊢ (2 · ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B)))) ∈ ℂ
74	68	sqcl 4686	. . . . . . 7 ⊢ ((√ ‘(B ·_i B))↑2) ∈ ℂ
75	70, 73, 74	add23 4129	. . . . . 6 ⊢ ((((√ ‘(A ·_i A))↑2) + (2 · ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B))))) + ((√ ‘(B ·_i B))↑2)) = ((((√ ‘(A ·_i A))↑2) + ((√ ‘(B ·_i B))↑2)) + (2 · ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B)))))
76	34	sqsqr 4775	. . . . . . . . 9 ⊢ (0 ≤ (A ·_i A) → ((√ ‘(A ·_i A))↑2) = (A ·_i A))
77	32, 76	ax-mp 6	. . . . . . . 8 ⊢ ((√ ‘(A ·_i A))↑2) = (A ·_i A)
78	40	sqsqr 4775	. . . . . . . . 9 ⊢ (0 ≤ (B ·_i B) → ((√ ‘(B ·_i B))↑2) = (B ·_i B))
79	38, 78	ax-mp 6	. . . . . . . 8 ⊢ ((√ ‘(B ·_i B))↑2) = (B ·_i B)
80	77, 79	opreq12i 3011	. . . . . . 7 ⊢ (((√ ‘(A ·_i A))↑2) + ((√ ‘(B ·_i B))↑2)) = ((A ·_i A) + (B ·_i B))
81	80	opreq1i 3009	. . . . . 6 ⊢ ((((√ ‘(A ·_i A))↑2) + ((√ ‘(B ·_i B))↑2)) + (2 · ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B))))) = (((A ·_i A) + (B ·_i B)) + (2 · ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B)))))
82	69, 75, 81	3eqtr 1123	. . . . 5 ⊢ (((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2) = (((A ·_i A) + (B ·_i B)) + (2 · ((√ ‘(A ·_i A)) · (√ ‘(B ·_i B)))))
83	47, 66, 82	3brtr4 2085	. . . 4 ⊢ ((A +_v B) ·_i (A +_v B)) ≤ (((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2)
84		hiidge0t 5056	. . . . . 6 ⊢ ((A +_v B) ∈ ℋ → 0 ≤ ((A +_v B) ·_i (A +_v B)))
85	48, 84	ax-mp 6	. . . . 5 ⊢ 0 ≤ ((A +_v B) ·_i (A +_v B))
86	36, 42	readdcl 4118	. . . . . 6 ⊢ ((√ ‘(A ·_i A)) + (√ ‘(B ·_i B))) ∈ ℝ
87	86	sqege0 4704	. . . . 5 ⊢ 0 ≤ (((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2)
88		hiidrclt 5053	. . . . . . 7 ⊢ ((A +_v B) ∈ ℋ → ((A +_v B) ·_i (A +_v B)) ∈ ℝ)
89	48, 88	ax-mp 6	. . . . . 6 ⊢ ((A +_v B) ·_i (A +_v B)) ∈ ℝ
90	86	sqrecl 4699	. . . . . 6 ⊢ (((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2) ∈ ℝ
91	89, 90	sqrle 4765	. . . . 5 ⊢ ((0 ≤ ((A +_v B) ·_i (A +_v B)) ∧ 0 ≤ (((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2)) → (((A +_v B) ·_i (A +_v B)) ≤ (((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2) ↔ (√ ‘((A +_v B) ·_i (A +_v B))) ≤ (√ ‘(((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2))))
92	85, 87, 91	mp2an 520	. . . 4 ⊢ (((A +_v B) ·_i (A +_v B)) ≤ (((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2) ↔ (√ ‘((A +_v B) ·_i (A +_v B))) ≤ (√ ‘(((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2)))
93	83, 92	mpbi 164	. . 3 ⊢ (√ ‘((A +_v B) ·_i (A +_v B))) ≤ (√ ‘(((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2))
94	34	sqrge0 4760	. . . . . 6 ⊢ (0 ≤ (A ·_i A) → 0 ≤ (√ ‘(A ·_i A)))
95	32, 94	ax-mp 6	. . . . 5 ⊢ 0 ≤ (√ ‘(A ·_i A))
96	40	sqrge0 4760	. . . . . 6 ⊢ (0 ≤ (B ·_i B) → 0 ≤ (√ ‘(B ·_i B)))
97	38, 96	ax-mp 6	. . . . 5 ⊢ 0 ≤ (√ ‘(B ·_i B))
98	36, 42	addge0 4324	. . . . 5 ⊢ ((0 ≤ (√ ‘(A ·_i A)) ∧ 0 ≤ (√ ‘(B ·_i B))) → 0 ≤ ((√ ‘(A ·_i A)) + (√ ‘(B ·_i B))))
99	95, 97, 98	mp2an 520	. . . 4 ⊢ 0 ≤ ((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))
100	86	sqrsqe 4774	. . . 4 ⊢ (0 ≤ ((√ ‘(A ·_i A)) + (√ ‘(B ·_i B))) → (√ ‘(((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2)) = ((√ ‘(A ·_i A)) + (√ ‘(B ·_i B))))
101	99, 100	ax-mp 6	. . 3 ⊢ (√ ‘(((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))↑2)) = ((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))
102	93, 101	breqtr 2080	. 2 ⊢ (√ ‘((A +_v B) ·_i (A +_v B))) ≤ ((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))
103		normvalt 5075	. . 3 ⊢ ((A +_v B) ∈ ℋ → (norm ‘(A +_v B)) = (√ ‘((A +_v B) ·_i (A +_v B))))
104	48, 103	ax-mp 6	. 2 ⊢ (norm ‘(A +_v B)) = (√ ‘((A +_v B) ·_i (A +_v B)))
105		normvalt 5075	. . . 4 ⊢ (A ∈ ℋ → (norm ‘A) = (√ ‘(A ·_i A)))
106	7, 105	ax-mp 6	. . 3 ⊢ (norm ‘A) = (√ ‘(A ·_i A))
107		normvalt 5075	. . . 4 ⊢ (B ∈ ℋ → (norm ‘B) = (√ ‘(B ·_i B)))
108	6, 107	ax-mp 6	. . 3 ⊢ (norm ‘B) = (√ ‘(B ·_i B))
109	106, 108	opreq12i 3011	. 2 ⊢ ((norm ‘A) + (norm ‘B)) = ((√ ‘(A ·_i A)) + (√ ‘(B ·_i B)))
110	102, 104, 109	3brtr4 2085	1 ⊢ (norm ‘(A +_v B)) ≤ ((norm ‘A) + (norm ‘B))

Colors of variables: wff set class

Syntax hints: ↔ wb 127 = wceq 1091 ∈ wcel 1092 class class class wbr 2054 ‘cfv 2422 (class class class)co 3001 ℝcr 4027 0cc0 4028 1c1 4029 + caddc 4031 · cmulc 4032 -cneg 4090 ≤ cle 4092 2c2 4454 ↑cexp 4675 √csqr 4727 ∗ccj 4788 abscabs 4789 ℋ chil 4958 +_v cva 4959 ·_i csp 4963 normcno 4964

This theorem is referenced by: norm3dif 5094

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079 ax-hvaddcl 4984 ax-hvzercl 4987 ax-hvmulcl 4989 ax-hvmulass 4992 ax-hvmulzer 4995 ax-hicl 5043 ax-his1 5045 ax-his2 5046 ax-his3 5047 ax-his4 5048

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-sup 2154 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1st 3087 df-2nd 3088 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-i 4037 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-div 4216 df-le 4277 df-n 4423 df-2 4462 df-3 4463 df-4 4464 df-n0 4535 df-z 4564 df-seq 4661 df-exp 4676 df-sqr 4728 df-re 4790 df-im 4791 df-cj 4792 df-abs 4793 df-hvsub 4996 df-hnorm 5074

metamath.org