Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem bcs 5101

Description: Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98.

**Hypotheses**
Ref	Expression
bcs.1	⊢ A ∈ ℋ
bcs.2	⊢ B ∈ ℋ

**Assertion**
Ref	Expression
bcs	⊢ (abs ‘(A ·_i B)) ≤ ((norm ‘A) · (norm ‘B))

**Proof of Theorem bcs**
Step	Hyp	Ref	Expression
1		fveq2 2832	. . 3 ⊢ ((A ·_i B) = 0 → (abs ‘(A ·_i B)) = (abs ‘0))
2		cleqid 1102	. . . . 5 ⊢ 0 = 0
3		0cn 4100	. . . . . 6 ⊢ 0 ∈ ℂ
4	3	abs00 4839	. . . . 5 ⊢ ((abs ‘0) = 0 ↔ 0 = 0)
5	2, 4	mpbir 165	. . . 4 ⊢ (abs ‘0) = 0
6		bcs.1	. . . . . 6 ⊢ A ∈ ℋ
7		normge0t 5077	. . . . . 6 ⊢ (A ∈ ℋ → 0 ≤ (norm ‘A))
8	6, 7	ax-mp 6	. . . . 5 ⊢ 0 ≤ (norm ‘A)
9		bcs.2	. . . . . 6 ⊢ B ∈ ℋ
10		normge0t 5077	. . . . . 6 ⊢ (B ∈ ℋ → 0 ≤ (norm ‘B))
11	9, 10	ax-mp 6	. . . . 5 ⊢ 0 ≤ (norm ‘B)
12	6	normcl 5081	. . . . . 6 ⊢ (norm ‘A) ∈ ℝ
13	9	normcl 5081	. . . . . 6 ⊢ (norm ‘B) ∈ ℝ
14	12, 13	mulge0 4335	. . . . 5 ⊢ ((0 ≤ (norm ‘A) ∧ 0 ≤ (norm ‘B)) → 0 ≤ ((norm ‘A) · (norm ‘B)))
15	8, 11, 14	mp2an 520	. . . 4 ⊢ 0 ≤ ((norm ‘A) · (norm ‘B))
16	5, 15	eqbrtr 2076	. . 3 ⊢ (abs ‘0) ≤ ((norm ‘A) · (norm ‘B))
17	1, 16	syl6eqbr 2092	. 2 ⊢ ((A ·_i B) = 0 → (abs ‘(A ·_i B)) ≤ ((norm ‘A) · (norm ‘B)))
18		df-ne 1192	. . . 4 ⊢ ((A ·_i B) ≠ 0 ↔ ¬ (A ·_i B) = 0)
19	6, 9	hicl 5044	. . . . . . 7 ⊢ (A ·_i B) ∈ ℂ
20	19	abslem2 4867	. . . . . 6 ⊢ ((A ·_i B) ≠ 0 → (((∗ ‘((A ·_i B) / (abs ‘(A ·_i B)))) · (A ·_i B)) + (((A ·_i B) / (abs ‘(A ·_i B))) · (∗ ‘(A ·_i B)))) = (2 · (abs ‘(A ·_i B))))
21		ax-his1 5045	. . . . . . . . 9 ⊢ ((B ∈ ℋ ∧ A ∈ ℋ ) → (B ·_i A) = (∗ ‘(A ·_i B)))
22	9, 6, 21	mp2an 520	. . . . . . . 8 ⊢ (B ·_i A) = (∗ ‘(A ·_i B))
23	22	opreq2i 3010	. . . . . . 7 ⊢ (((A ·_i B) / (abs ‘(A ·_i B))) · (B ·_i A)) = (((A ·_i B) / (abs ‘(A ·_i B))) · (∗ ‘(A ·_i B)))
24	23	opreq2i 3010	. . . . . 6 ⊢ (((∗ ‘((A ·_i B) / (abs ‘(A ·_i B)))) · (A ·_i B)) + (((A ·_i B) / (abs ‘(A ·_i B))) · (B ·_i A))) = (((∗ ‘((A ·_i B) / (abs ‘(A ·_i B)))) · (A ·_i B)) + (((A ·_i B) / (abs ‘(A ·_i B))) · (∗ ‘(A ·_i B))))
25	20, 24	syl5req 1137	. . . . 5 ⊢ ((A ·_i B) ≠ 0 → (2 · (abs ‘(A ·_i B))) = (((∗ ‘((A ·_i B) / (abs ‘(A ·_i B)))) · (A ·_i B)) + (((A ·_i B) / (abs ‘(A ·_i B))) · (B ·_i A))))
26	19	abs00 4839	. . . . . . . . 9 ⊢ ((abs ‘(A ·_i B)) = 0 ↔ (A ·_i B) = 0)
27	26	negbii 162	. . . . . . . 8 ⊢ (¬ (abs ‘(A ·_i B)) = 0 ↔ ¬ (A ·_i B) = 0)
28		df-ne 1192	. . . . . . . 8 ⊢ ((abs ‘(A ·_i B)) ≠ 0 ↔ ¬ (abs ‘(A ·_i B)) = 0)
29	27, 28, 18	3bitr4 158	. . . . . . 7 ⊢ ((abs ‘(A ·_i B)) ≠ 0 ↔ (A ·_i B) ≠ 0)
30	19	abscl 4840	. . . . . . . . . 10 ⊢ (abs ‘(A ·_i B)) ∈ ℝ
31	30	recn 4098	. . . . . . . . 9 ⊢ (abs ‘(A ·_i B)) ∈ ℂ
32	19, 31	divclz 4222	. . . . . . . 8 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → ((A ·_i B) / (abs ‘(A ·_i B))) ∈ ℂ)
33	19, 31	divrecz 4237	. . . . . . . . . 10 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → ((A ·_i B) / (abs ‘(A ·_i B))) = ((A ·_i B) · (1 / (abs ‘(A ·_i B)))))
34	33	fveq2d 2836	. . . . . . . . 9 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → (abs ‘((A ·_i B) / (abs ‘(A ·_i B)))) = (abs ‘((A ·_i B) · (1 / (abs ‘(A ·_i B))))))
35		1cn 4101	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
36	35, 31	divclz 4222	. . . . . . . . . . . 12 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → (1 / (abs ‘(A ·_i B))) ∈ ℂ)
37	36, 19	jctil 240	. . . . . . . . . . 11 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → ((A ·_i B) ∈ ℂ ∧ (1 / (abs ‘(A ·_i B))) ∈ ℂ))
38		absmult 4849	. . . . . . . . . . 11 ⊢ (((A ·_i B) ∈ ℂ ∧ (1 / (abs ‘(A ·_i B))) ∈ ℂ) → (abs ‘((A ·_i B) · (1 / (abs ‘(A ·_i B))))) = ((abs ‘(A ·_i B)) · (abs ‘(1 / (abs ‘(A ·_i B))))))
39	37, 38	syl 12	. . . . . . . . . 10 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → (abs ‘((A ·_i B) · (1 / (abs ‘(A ·_i B))))) = ((abs ‘(A ·_i B)) · (abs ‘(1 / (abs ‘(A ·_i B))))))
40		absidt 4862	. . . . . . . . . . . 12 ⊢ ((1 / (abs ‘(A ·_i B))) ∈ ℝ → (0 ≤ (1 / (abs ‘(A ·_i B))) → (abs ‘(1 / (abs ‘(A ·_i B)))) = (1 / (abs ‘(A ·_i B)))))
41		ax1re 4064	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
42	41, 30	redivclz 4275	. . . . . . . . . . . 12 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → (1 / (abs ‘(A ·_i B))) ∈ ℝ)
43		ltlet 4286	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ (1 / (abs ‘(A ·_i B))) ∈ ℝ) → (0 < (1 / (abs ‘(A ·_i B))) → 0 ≤ (1 / (abs ‘(A ·_i B)))))
44		ax0re 4063	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
45	42, 44	jctil 240	. . . . . . . . . . . . 13 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → (0 ∈ ℝ ∧ (1 / (abs ‘(A ·_i B))) ∈ ℝ))
46	19	absgt0 4842	. . . . . . . . . . . . . . 15 ⊢ (¬ (A ·_i B) = 0 ↔ 0 < (abs ‘(A ·_i B)))
47	28, 27, 46	3bitr 155	. . . . . . . . . . . . . 14 ⊢ ((abs ‘(A ·_i B)) ≠ 0 ↔ 0 < (abs ‘(A ·_i B)))
48	30	recgt0 4386	. . . . . . . . . . . . . 14 ⊢ (0 < (abs ‘(A ·_i B)) → 0 < (1 / (abs ‘(A ·_i B))))
49	47, 48	sylbi 174	. . . . . . . . . . . . 13 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → 0 < (1 / (abs ‘(A ·_i B))))
50	43, 45, 49	sylc 62	. . . . . . . . . . . 12 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → 0 ≤ (1 / (abs ‘(A ·_i B))))
51	40, 42, 50	sylc 62	. . . . . . . . . . 11 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → (abs ‘(1 / (abs ‘(A ·_i B)))) = (1 / (abs ‘(A ·_i B))))
52	51	opreq2d 3013	. . . . . . . . . 10 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → ((abs ‘(A ·_i B)) · (abs ‘(1 / (abs ‘(A ·_i B))))) = ((abs ‘(A ·_i B)) · (1 / (abs ‘(A ·_i B)))))
53	39, 52	eqtrd 1128	. . . . . . . . 9 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → (abs ‘((A ·_i B) · (1 / (abs ‘(A ·_i B))))) = ((abs ‘(A ·_i B)) · (1 / (abs ‘(A ·_i B)))))
54	31	recidz 4234	. . . . . . . . 9 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → ((abs ‘(A ·_i B)) · (1 / (abs ‘(A ·_i B)))) = 1)
55	34, 53, 54	3eqtrd 1132	. . . . . . . 8 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → (abs ‘((A ·_i B) / (abs ‘(A ·_i B)))) = 1)
56	32, 55	jca 236	. . . . . . 7 ⊢ ((abs ‘(A ·_i B)) ≠ 0 → (((A ·_i B) / (abs ‘(A ·_i B))) ∈ ℂ ∧ (abs ‘((A ·_i B) / (abs ‘(A ·_i B)))) = 1))
57	29, 56	sylbir 176	. . . . . 6 ⊢ ((A ·_i B) ≠ 0 → (((A ·_i B) / (abs ‘(A ·_i B))) ∈ ℂ ∧ (abs ‘((A ·_i B) / (abs ‘(A ·_i B)))) = 1))
58	6, 9	normlem7t 5072	. . . . . 6 ⊢ ((((A ·_i B) / (abs ‘(A ·_i B))) ∈ ℂ ∧ (abs ‘((A ·_i B) / (abs ‘(A ·_i B)))) = 1) → (((∗ ‘((A ·_i B) / (abs ‘(A ·_i B)))) · (A ·_i B)) + (((A ·_i B) / (abs ‘(A ·_i B))) · (B ·_i A))) ≤ (2 · ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A)))))
59	57, 58	syl 12	. . . . 5 ⊢ ((A ·_i B) ≠ 0 → (((∗ ‘((A ·_i B) / (abs ‘(A ·_i B)))) · (A ·_i B)) + (((A ·_i B) / (abs ‘(A ·_i B))) · (B ·_i A))) ≤ (2 · ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A)))))
60	25, 59	eqbrtrd 2077	. . . 4 ⊢ ((A ·_i B) ≠ 0 → (2 · (abs ‘(A ·_i B))) ≤ (2 · ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A)))))
61	18, 60	sylbir 176	. . 3 ⊢ (¬ (A ·_i B) = 0 → (2 · (abs ‘(A ·_i B))) ≤ (2 · ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A)))))
62	12	recn 4098	. . . . . . 7 ⊢ (norm ‘A) ∈ ℂ
63	13	recn 4098	. . . . . . 7 ⊢ (norm ‘B) ∈ ℂ
64	62, 63	mulcom 4107	. . . . . 6 ⊢ ((norm ‘A) · (norm ‘B)) = ((norm ‘B) · (norm ‘A))
65		normvalt 5075	. . . . . . . 8 ⊢ (B ∈ ℋ → (norm ‘B) = (√ ‘(B ·_i B)))
66	9, 65	ax-mp 6	. . . . . . 7 ⊢ (norm ‘B) = (√ ‘(B ·_i B))
67		normvalt 5075	. . . . . . . 8 ⊢ (A ∈ ℋ → (norm ‘A) = (√ ‘(A ·_i A)))
68	6, 67	ax-mp 6	. . . . . . 7 ⊢ (norm ‘A) = (√ ‘(A ·_i A))
69	66, 68	opreq12i 3011	. . . . . 6 ⊢ ((norm ‘B) · (norm ‘A)) = ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A)))
70	64, 69	eqtr 1119	. . . . 5 ⊢ ((norm ‘A) · (norm ‘B)) = ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A)))
71	70	breq2i 2069	. . . 4 ⊢ ((abs ‘(A ·_i B)) ≤ ((norm ‘A) · (norm ‘B)) ↔ (abs ‘(A ·_i B)) ≤ ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A))))
72		2pos 4479	. . . . 5 ⊢ 0 < 2
73		hiidge0t 5056	. . . . . . . . 9 ⊢ (B ∈ ℋ → 0 ≤ (B ·_i B))
74	9, 73	ax-mp 6	. . . . . . . 8 ⊢ 0 ≤ (B ·_i B)
75		hiidrclt 5053	. . . . . . . . . 10 ⊢ (B ∈ ℋ → (B ·_i B) ∈ ℝ)
76	9, 75	ax-mp 6	. . . . . . . . 9 ⊢ (B ·_i B) ∈ ℝ
77	76	sqrcl 4758	. . . . . . . 8 ⊢ (0 ≤ (B ·_i B) → (√ ‘(B ·_i B)) ∈ ℝ)
78	74, 77	ax-mp 6	. . . . . . 7 ⊢ (√ ‘(B ·_i B)) ∈ ℝ
79		hiidge0t 5056	. . . . . . . . 9 ⊢ (A ∈ ℋ → 0 ≤ (A ·_i A))
80	6, 79	ax-mp 6	. . . . . . . 8 ⊢ 0 ≤ (A ·_i A)
81		hiidrclt 5053	. . . . . . . . . 10 ⊢ (A ∈ ℋ → (A ·_i A) ∈ ℝ)
82	6, 81	ax-mp 6	. . . . . . . . 9 ⊢ (A ·_i A) ∈ ℝ
83	82	sqrcl 4758	. . . . . . . 8 ⊢ (0 ≤ (A ·_i A) → (√ ‘(A ·_i A)) ∈ ℝ)
84	80, 83	ax-mp 6	. . . . . . 7 ⊢ (√ ‘(A ·_i A)) ∈ ℝ
85	78, 84	remulcl 4119	. . . . . 6 ⊢ ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A))) ∈ ℝ
86		2re 4470	. . . . . 6 ⊢ 2 ∈ ℝ
87	30, 85, 86	lemul2 4396	. . . . 5 ⊢ (0 < 2 → ((abs ‘(A ·_i B)) ≤ ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A))) ↔ (2 · (abs ‘(A ·_i B))) ≤ (2 · ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A))))))
88	72, 87	ax-mp 6	. . . 4 ⊢ ((abs ‘(A ·_i B)) ≤ ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A))) ↔ (2 · (abs ‘(A ·_i<ªI> B))) ≤ (2 · ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A)))))
89	71, 88	bitr 151	. . 3 ⊢ ((abs ‘(A ·_i B)) ≤ ((norm ‘A) · (norm ‘B)) ↔ (2 · (abs ‘(A ·_i B))) ≤ (2 · ((√ ‘(B ·_i B)) · (√ ‘(A ·_i A)))))
90	61, 89	sylibr 175	. 2 ⊢ (¬ (A ·_i B) = 0 → (abs ‘(A ·_i B)) ≤ ((norm ‘A) · (norm ‘B)))
91	17, 90	pm2.61i 110	1 ⊢ (abs ‘(A ·_i B)) ≤ ((norm ‘A) · (norm ‘B))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 ↔ wb 127 ∧ wa 196 = wceq 1091 ∈ wcel 1092 ≠ wne 1190 class class class wbr 2054 ‘cfv 2422 (class class class)co 3001 ℂcc 4026 ℝcr 4027 0cc0 4028 1c1 4029 + caddc 4031 · cmulc 4032 < clt 4033 / cdiv 4091 ≤ cle 4092 2c2 4454 √csqr 4727 ∗ccj 4788 abscabs 4789 ℋ chil 4958 ·_i csp 4963 normcno 4964

This theorem is referenced by: occllem1 5180

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