Theorem normlem3

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 21-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$$
	normlem3.7	$$⊢R\in ℝ$$
Assertion	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)$$

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		normlem3.7	$$⊢R\in ℝ$$
8	3 3	hicli	$$⊢G{\cdot }_{\mathrm{ih}}G\in ℂ$$
9	5 8	eqeltri	$$⊢A\in ℂ$$
10	7	recni	$$⊢R\in ℂ$$
11	10	sqcli	$$⊢R^2\in ℂ$$
12	9 11	mulcli	$$⊢A{R}^2\in ℂ$$
13	1 2 3 4	normlem2	$$⊢B\in ℝ$$
14	13	recni	$$⊢B\in ℂ$$
15	14 10	mulcli	$$⊢BR\in ℂ$$
16	12 15	addcomi	$$⊢A{R}^2+BR=BR+A{R}^2$$
17	1	cjcli	$$⊢\bar{S}\in ℂ$$
18	2 3	hicli	$$⊢F{\cdot }_{\mathrm{ih}}G\in ℂ$$
19	17 18	mulcli	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)\in ℂ$$
20	3 2	hicli	$$⊢G{\cdot }_{\mathrm{ih}}F\in ℂ$$
21	1 20	mulcli	$$⊢S\left(G{\cdot }_{\mathrm{ih}}F\right)\in ℂ$$
22	19 21	addcli	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\in ℂ$$
23	22 10	mulneg1i	$$⊢\left(-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\right)R=-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)R$$
24	4	oveq1i	$$⊢BR=\left(-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\right)R$$
25	22 10	mulneg2i	$$⊢\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\left(-R\right)=-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)R$$
26	23 24 25	3eqtr4i	$$⊢BR=\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\left(-R\right)$$
27	10	negcli	$$⊢-R\in ℂ$$
28	19 21 27	adddiri	$$⊢\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\left(-R\right)=\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)\left(-R\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\left(-R\right)$$
29	17 18 27	mul32i	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)\left(-R\right)=\bar{S}\left(-R\right)\left(F{\cdot }_{\mathrm{ih}}G\right)$$
30	1 20 27	mul32i	$$⊢S\left(G{\cdot }_{\mathrm{ih}}F\right)\left(-R\right)=S\left(-R\right)\left(G{\cdot }_{\mathrm{ih}}F\right)$$
31	29 30	oveq12i	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)\left(-R\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\left(-R\right)=\bar{S}\left(-R\right)\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(-R\right)\left(G{\cdot }_{\mathrm{ih}}F\right)$$
32	26 28 31	3eqtri	$$⊢BR=\bar{S}\left(-R\right)\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(-R\right)\left(G{\cdot }_{\mathrm{ih}}F\right)$$
33	5	oveq2i	$$⊢R^{2}A=R^2\left(G{\cdot }_{\mathrm{ih}}G\right)$$
34	11 9 33	mulcomli	$$⊢A{R}^2=R^2\left(G{\cdot }_{\mathrm{ih}}G\right)$$
35	32 34	oveq12i	$$⊢BR+A{R}^2=\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)$$
36	17 27	mulcli	$$⊢\bar{S}\left(-R\right)\in ℂ$$
37	36 18	mulcli	$$⊢\bar{S}\left(-R\right)\left(F{\cdot }_{\mathrm{ih}}G\right)\in ℂ$$
38	1 27	mulcli	$$⊢S\left(-R\right)\in ℂ$$
39	38 20	mulcli	$$⊢S\left(-R\right)\left(G{\cdot }_{\mathrm{ih}}F\right)\in ℂ$$
40	11 8	mulcli	$$⊢R^2\left(G{\cdot }_{\mathrm{ih}}G\right)\in ℂ$$
41	37 39 40	addassi	$$⊢\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)=\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)$$
42	16 35 41	3eqtri	$$⊢A{R}^2+BR=\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)$$
43	6 42	oveq12i	$$⊢C+A{R}^2+BR=\left(F{\cdot }_{\mathrm{ih}}F\right)+\bar{S}\left(-R\right)\left(F{\cdot }_{\mathrm{ih}}G\right)+\left(S\left(-R\right)\left(G{\cdot }_{\mathrm{ih}}F\right)+R^2\left(G{\cdot }_{\mathrm{ih}}G\right)\right)$$
44	12 15	addcli	$$⊢A{R}^2+BR\in ℂ$$
45	2 2	hicli	$$⊢F{\cdot }_{\mathrm{ih}}F\in ℂ$$
46	6 45	eqeltri	$$⊢C\in ℂ$$
47	44 46	addcomi	$$⊢A{R}^2+BR+C=C+A{R}^2+BR$$
48	39 40	addcli	$$⊢S\left(-R\right)\left(G{\cdot }_{\mathrm{ih}}F\right)+R^2\left(G{\cdot }_{\mathrm{ih}}G\right)\in ℂ$$
49	45 37 48	addassi	$$⊢\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)=\left(F{\cdot }_{\mathrm{ih}}F\right)+\bar{S}\left(-R\right)\left(F{\cdot }_{\mathrm{ih}}G\right)+\left(S\left(-R\right)\left(G{\cdot }_{\mathrm{ih}}F\right)+R^2\left(G{\cdot }_{\mathrm{ih}}G\right)\right)$$
50	43 47 49	3eqtr4i	$$⊢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)$$