Theorem normlem4

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 29-Jul-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	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$$

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	1 2 3 7 8	normlem1	$$⊢\left(F{-}_{ℎ}\left(SR{\cdot }_{ℎ}G\right)\right){\cdot }_{\mathrm{ih}}\left(F{-}_{ℎ}\left(SR{\cdot }_{ℎ}G\right)\right)=\left(F{\cdot }_{\mathrm{ih}}F\right)+\bar{S}\left(-R\right)\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(-R\right)\left(G{\cdot }_{\mathrm{ih}}F\right)+R^2\left(G{\cdot }_{\mathrm{ih}}G\right)$$
10	1 2 3 4 5 6 7	normlem3	$$⊢A{R}^2+BR+C=\left(F{\cdot }_{\mathrm{ih}}F\right)+\bar{S}\left(-R\right)\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(-R\right)\left(G{\cdot }_{\mathrm{ih}}F\right)+R^2\left(G{\cdot }_{\mathrm{ih}}G\right)$$
11	9 10	eqtr4i	$$⊢\left(F{-}_{ℎ}\left(SR{\cdot }_{ℎ}G\right)\right){\cdot }_{\mathrm{ih}}\left(F{-}_{ℎ}\left(SR{\cdot }_{ℎ}G\right)\right)=A{R}^2+BR+C$$