Theorem normlem7

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.)

	Ref	Expression
Hypotheses	normlem1.1	$$⊢S\in ℂ$$
	normlem1.2	$$⊢F\in \mathscr{H}$$
	normlem1.3	$$⊢G\in \mathscr{H}$$
	normlem7.4	$$⊢\left|S\right|=1$$
Assertion	normlem7	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\le 2\sqrt{G{\cdot }_{\mathrm{ih}}G}\sqrt{F{\cdot }_{\mathrm{ih}}F}$$

Proof

Step	Hyp	Ref	Expression
1		normlem1.1	$$⊢S\in ℂ$$
2		normlem1.2	$$⊢F\in \mathscr{H}$$
3		normlem1.3	$$⊢G\in \mathscr{H}$$
4		normlem7.4	$$⊢\left|S\right|=1$$
5		eqid	$$⊢-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)=-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)$$
6	1 2 3 5	normlem2	$$⊢-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\in ℝ$$
7	1	cjcli	$$⊢\bar{S}\in ℂ$$
8	2 3	hicli	$$⊢F{\cdot }_{\mathrm{ih}}G\in ℂ$$
9	7 8	mulcli	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)\in ℂ$$
10	3 2	hicli	$$⊢G{\cdot }_{\mathrm{ih}}F\in ℂ$$
11	1 10	mulcli	$$⊢S\left(G{\cdot }_{\mathrm{ih}}F\right)\in ℂ$$
12	9 11	addcli	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\in ℂ$$
13	12	negrebi	$$⊢-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\in ℝ\leftrightarrow \bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\in ℝ$$
14	6 13	mpbi	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\in ℝ$$
15	14	leabsi	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\le \left|\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right|$$
16	12	absnegi	$$⊢\left|-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\right|=\left|\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right|$$
17	15 16	breqtrri	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\le \left|-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\right|$$
18		eqid	$$⊢G{\cdot }_{\mathrm{ih}}G=G{\cdot }_{\mathrm{ih}}G$$
19		eqid	$$⊢F{\cdot }_{\mathrm{ih}}F=F{\cdot }_{\mathrm{ih}}F$$
20	1 2 3 5 18 19 4	normlem6	$$⊢\left|-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\right|\le 2\sqrt{G{\cdot }_{\mathrm{ih}}G}\sqrt{F{\cdot }_{\mathrm{ih}}F}$$
21	12	negcli	$$⊢-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\in ℂ$$
22	21	abscli	$$⊢\left|-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\right|\in ℝ$$
23		2re	$$⊢2\in ℝ$$
24		hiidge0	$$⊢G\in \mathscr{H}\to 0\le G{\cdot }_{\mathrm{ih}}G$$
25		hiidrcl	$$⊢G\in \mathscr{H}\to G{\cdot }_{\mathrm{ih}}G\in ℝ$$
26	3 25	ax-mp	$$⊢G{\cdot }_{\mathrm{ih}}G\in ℝ$$
27	26	sqrtcli	$$⊢0\le G{\cdot }_{\mathrm{ih}}G\to \sqrt{G{\cdot }_{\mathrm{ih}}G}\in ℝ$$
28	3 24 27	mp2b	$$⊢\sqrt{G{\cdot }_{\mathrm{ih}}G}\in ℝ$$
29		hiidge0	$$⊢F\in \mathscr{H}\to 0\le F{\cdot }_{\mathrm{ih}}F$$
30		hiidrcl	$$⊢F\in \mathscr{H}\to F{\cdot }_{\mathrm{ih}}F\in ℝ$$
31	2 30	ax-mp	$$⊢F{\cdot }_{\mathrm{ih}}F\in ℝ$$
32	31	sqrtcli	$$⊢0\le F{\cdot }_{\mathrm{ih}}F\to \sqrt{F{\cdot }_{\mathrm{ih}}F}\in ℝ$$
33	2 29 32	mp2b	$$⊢\sqrt{F{\cdot }_{\mathrm{ih}}F}\in ℝ$$
34	28 33	remulcli	$$⊢\sqrt{G{\cdot }_{\mathrm{ih}}G}\sqrt{F{\cdot }_{\mathrm{ih}}F}\in ℝ$$
35	23 34	remulcli	$$⊢2\sqrt{G{\cdot }_{\mathrm{ih}}G}\sqrt{F{\cdot }_{\mathrm{ih}}F}\in ℝ$$
36	14 22 35	letri	$$⊢\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\le \left|-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\right|\wedge \left|-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\right|\le 2\sqrt{G{\cdot }_{\mathrm{ih}}G}\sqrt{F{\cdot }_{\mathrm{ih}}F}\right)\to \bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\le 2\sqrt{G{\cdot }_{\mathrm{ih}}G}\sqrt{F{\cdot }_{\mathrm{ih}}F}$$
37	17 20 36	mp2an	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\le 2\sqrt{G{\cdot }_{\mathrm{ih}}G}\sqrt{F{\cdot }_{\mathrm{ih}}F}$$