normlem7 - Hilbert Space Explorer

	Hilbert Space Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HSE Home > Th. List > normlem7		Structured version Visualization version GIF version

Theorem normlem7 30364

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
normlem1.1	⊢ 𝑆 ∈ ℂ
normlem1.2	⊢ 𝐹 ∈ ℋ
normlem1.3	⊢ 𝐺 ∈ ℋ
normlem7.4	⊢ (abs‘𝑆) = 1

**Assertion**
Ref	Expression
normlem7	⊢ (((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) ≤ (2 · ((√‘(𝐺 ·_ih 𝐺)) · (√‘(𝐹 ·_ih 𝐹))))

**Proof of Theorem normlem7**
Step	Hyp	Ref	Expression
1		normlem1.1	. . . . . 6 ⊢ 𝑆 ∈ ℂ
2		normlem1.2	. . . . . 6 ⊢ 𝐹 ∈ ℋ
3		normlem1.3	. . . . . 6 ⊢ 𝐺 ∈ ℋ
4		eqid 2732	. . . . . 6 ⊢ -(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) = -(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹)))
5	1, 2, 3, 4	normlem2 30359	. . . . 5 ⊢ -(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) ∈ ℝ
6	1	cjcli 15115	. . . . . . . 8 ⊢ (∗‘𝑆) ∈ ℂ
7	2, 3	hicli 30329	. . . . . . . 8 ⊢ (𝐹 ·_ih 𝐺) ∈ ℂ
8	6, 7	mulcli 11220	. . . . . . 7 ⊢ ((∗‘𝑆) · (𝐹 ·_ih 𝐺)) ∈ ℂ
9	3, 2	hicli 30329	. . . . . . . 8 ⊢ (𝐺 ·_ih 𝐹) ∈ ℂ
10	1, 9	mulcli 11220	. . . . . . 7 ⊢ (𝑆 · (𝐺 ·_ih 𝐹)) ∈ ℂ
11	8, 10	addcli 11219	. . . . . 6 ⊢ (((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) ∈ ℂ
12	11	negrebi 11533	. . . . 5 ⊢ (-(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) ∈ ℝ ↔ (((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) ∈ ℝ)
13	5, 12	mpbi 229	. . . 4 ⊢ (((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) ∈ ℝ
14	13	leabsi 15325	. . 3 ⊢ (((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) ≤ (abs‘(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))))
15	11	absnegi 15346	. . 3 ⊢ (abs‘-(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹)))) = (abs‘(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))))
16	14, 15	breqtrri 5175	. 2 ⊢ (((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) ≤ (abs‘-(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))))
17		eqid 2732	. . 3 ⊢ (𝐺 ·_ih 𝐺) = (𝐺 ·_ih 𝐺)
18		eqid 2732	. . 3 ⊢ (𝐹 ·_ih 𝐹) = (𝐹 ·_ih 𝐹)
19		normlem7.4	. . 3 ⊢ (abs‘𝑆) = 1
20	1, 2, 3, 4, 17, 18, 19	normlem6 30363	. 2 ⊢ (abs‘-(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹)))) ≤ (2 · ((√‘(𝐺 ·_ih 𝐺)) · (√‘(𝐹 ·_ih 𝐹))))
21	11	negcli 11527	. . . 4 ⊢ -(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) ∈ ℂ
22	21	abscli 15341	. . 3 ⊢ (abs‘-(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹)))) ∈ ℝ
23		2re 12285	. . . 4 ⊢ 2 ∈ ℝ
24		hiidge0 30346	. . . . . 6 ⊢ (𝐺 ∈ ℋ → 0 ≤ (𝐺 ·_ih 𝐺))
25		hiidrcl 30343	. . . . . . . 8 ⊢ (𝐺 ∈ ℋ → (𝐺 ·_ih 𝐺) ∈ ℝ)
26	3, 25	ax-mp 5	. . . . . . 7 ⊢ (𝐺 ·_ih 𝐺) ∈ ℝ
27	26	sqrtcli 15317	. . . . . 6 ⊢ (0 ≤ (𝐺 ·_ih 𝐺) → (√‘(𝐺 ·_ih 𝐺)) ∈ ℝ)
28	3, 24, 27	mp2b 10	. . . . 5 ⊢ (√‘(𝐺 ·_ih 𝐺)) ∈ ℝ
29		hiidge0 30346	. . . . . 6 ⊢ (𝐹 ∈ ℋ → 0 ≤ (𝐹 ·_ih 𝐹))
30		hiidrcl 30343	. . . . . . . 8 ⊢ (𝐹 ∈ ℋ → (𝐹 ·_ih 𝐹) ∈ ℝ)
31	2, 30	ax-mp 5	. . . . . . 7 ⊢ (𝐹 ·_ih 𝐹) ∈ ℝ
32	31	sqrtcli 15317	. . . . . 6 ⊢ (0 ≤ (𝐹 ·_ih 𝐹) → (√‘(𝐹 ·_ih 𝐹)) ∈ ℝ)
33	2, 29, 32	mp2b 10	. . . . 5 ⊢ (√‘(𝐹 ·_ih 𝐹)) ∈ ℝ
34	28, 33	remulcli 11229	. . . 4 ⊢ ((√‘(𝐺 ·_ih 𝐺)) · (√‘(𝐹 ·_ih 𝐹))) ∈ ℝ
35	23, 34	remulcli 11229	. . 3 ⊢ (2 · ((√‘(𝐺 ·_ih 𝐺)) · (√‘(𝐹 ·_ih 𝐹)))) ∈ ℝ
36	13, 22, 35	letri 11342	. 2 ⊢ (((((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) ≤ (abs‘-(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹)))) ∧ (abs‘-(((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹)))) ≤ (2 · ((√‘(𝐺 ·_ih 𝐺)) · (√‘(𝐹 ·_ih 𝐹))))) → (((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) ≤ (2 · ((√‘(𝐺 ·_ih 𝐺)) · (√‘(𝐹 ·_ih 𝐹)))))
37	16, 20, 36	mp2an 690	1 ⊢ (((∗‘𝑆) · (𝐹 ·_ih 𝐺)) + (𝑆 · (𝐺 ·_ih 𝐹))) ≤ (2 · ((√‘(𝐺 ·_ih 𝐺)) · (√‘(𝐹 ·_ih 𝐹))))

Colors of variables: wff setvar class

Syntax hints: = wceq 1541 ∈ wcel 2106 class class class wbr 5148 ‘cfv 6543 (class class class)co 7408 ℂcc 11107 ℝcr 11108 0cc0 11109 1c1 11110 + caddc 11112 · cmul 11114 ≤ cle 11248 -cneg 11444 2c2 12266 ∗ccj 15042 √csqrt 15179 abscabs 15180 ℋchba 30167 ·_ih csp 30170

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7724 ax-cnex 11165 ax-resscn 11166 ax-1cn 11167 ax-icn 11168 ax-addcl 11169 ax-addrcl 11170 ax-mulcl 11171 ax-mulrcl 11172 ax-mulcom 11173 ax-addass 11174 ax-mulass 11175 ax-distr 11176 ax-i2m1 11177 ax-1ne0 11178 ax-1rid 11179 ax-rnegex 11180 ax-rrecex 11181 ax-cnre 11182 ax-pre-lttri 11183 ax-pre-lttrn 11184 ax-pre-ltadd 11185 ax-pre-mulgt0 11186 ax-pre-sup 11187 ax-hfvadd 30248 ax-hv0cl 30251 ax-hfvmul 30253 ax-hvmulass 30255 ax-hvmul0 30258 ax-hfi 30327 ax-his1 30330 ax-his2 30331 ax-his3 30332 ax-his4 30333

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7364 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7855 df-2nd 7975 df-frecs 8265 df-wrecs 8296 df-recs 8370 df-rdg 8409 df-er 8702 df-en 8939 df-dom 8940 df-sdom 8941 df-sup 9436 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11445 df-neg 11446 df-div 11871 df-nn 12212 df-2 12274 df-3 12275 df-4 12276 df-n0 12472 df-z 12558 df-uz 12822 df-rp 12974 df-seq 13966 df-exp 14027 df-cj 15045 df-re 15046 df-im 15047 df-sqrt 15181 df-abs 15182 df-hvsub 30219

This theorem is referenced by: normlem7tALT 30367 norm-ii-i 30385

W3C validator