Theorem normlem5

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 10-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}$$
	normlem2.4	$$⊢B=-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)$$
	normlem3.5	$$⊢A=G{\cdot }_{\mathrm{ih}}G$$
	normlem3.6	$$⊢C=F{\cdot }_{\mathrm{ih}}F$$
	normlem4.7	$$⊢R\in ℝ$$
	normlem4.8	$$⊢\left|S\right|=1$$
Assertion	normlem5	$$⊢0\le A{R}^2+BR+C$$

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		normlem2.4	$$⊢B=-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)$$
5		normlem3.5	$$⊢A=G{\cdot }_{\mathrm{ih}}G$$
6		normlem3.6	$$⊢C=F{\cdot }_{\mathrm{ih}}F$$
7		normlem4.7	$$⊢R\in ℝ$$
8		normlem4.8	$$⊢\left|S\right|=1$$
9	7	recni	$$⊢R\in ℂ$$
10	1 9	mulcli	$$⊢SR\in ℂ$$
11	10 3	hvmulcli	$$⊢SR{\cdot }_{ℎ}G\in \mathscr{H}$$
12	2 11	hvsubcli	$$⊢F{-}_{ℎ}\left(SR{\cdot }_{ℎ}G\right)\in \mathscr{H}$$
13		hiidge0	$$⊢F{-}_{ℎ}\left(SR{\cdot }_{ℎ}G\right)\in \mathscr{H}\to 0\le \left(F{-}_{ℎ}\left(SR{\cdot }_{ℎ}G\right)\right){\cdot }_{\mathrm{ih}}\left(F{-}_{ℎ}\left(SR{\cdot }_{ℎ}G\right)\right)$$
14	12 13	ax-mp	$$⊢0\le \left(F{-}_{ℎ}\left(SR{\cdot }_{ℎ}G\right)\right){\cdot }_{\mathrm{ih}}\left(F{-}_{ℎ}\left(SR{\cdot }_{ℎ}G\right)\right)$$
15	1 2 3 4 5 6 7 8	normlem4	$$⊢\left(F{-}_{ℎ}\left(SR{\cdot }_{ℎ}G\right)\right){\cdot }_{\mathrm{ih}}\left(F{-}_{ℎ}\left(SR{\cdot }_{ℎ}G\right)\right)=A{R}^2+BR+C$$
16	14 15	breqtri	$$⊢0\le A{R}^2+BR+C$$