Theorem normlem2

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

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	1	cjcli	$$⊢\bar{S}\in ℂ$$
6	2 3	hicli	$$⊢F{\cdot }_{\mathrm{ih}}G\in ℂ$$
7	5 6	mulcli	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)\in ℂ$$
8	3 2	hicli	$$⊢G{\cdot }_{\mathrm{ih}}F\in ℂ$$
9	1 8	mulcli	$$⊢S\left(G{\cdot }_{\mathrm{ih}}F\right)\in ℂ$$
10	7 9	cjaddi	$$⊢\overline{\stackrel{‾}{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)}=\overline{\stackrel{‾}{S}\left(F{\cdot }_{\mathrm{ih}}G\right)}+\overline{S\left(G{\cdot }_{\mathrm{ih}}F\right)}$$
11	1	cjcji	$$⊢\overline{\stackrel{‾}{S}}=S$$
12	11	eqcomi	$$⊢S=\overline{\stackrel{‾}{S}}$$
13	3 2	his1i	$$⊢G{\cdot }_{\mathrm{ih}}F=\overline{F{\cdot }_{\mathrm{ih}}G}$$
14	12 13	oveq12i	$$⊢S\left(G{\cdot }_{\mathrm{ih}}F\right)=\overline{\stackrel{‾}{S}}\overline{F{\cdot }_{\mathrm{ih}}G}$$
15	5 6	cjmuli	$$⊢\overline{\stackrel{‾}{S}\left(F{\cdot }_{\mathrm{ih}}G\right)}=\overline{\stackrel{‾}{S}}\overline{F{\cdot }_{\mathrm{ih}}G}$$
16	14 15	eqtr4i	$$⊢S\left(G{\cdot }_{\mathrm{ih}}F\right)=\overline{\stackrel{‾}{S}\left(F{\cdot }_{\mathrm{ih}}G\right)}$$
17	2 3	his1i	$$⊢F{\cdot }_{\mathrm{ih}}G=\overline{G{\cdot }_{\mathrm{ih}}F}$$
18	17	oveq2i	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)=\bar{S}\overline{G{\cdot }_{\mathrm{ih}}F}$$
19	1 8	cjmuli	$$⊢\overline{S\left(G{\cdot }_{\mathrm{ih}}F\right)}=\bar{S}\overline{G{\cdot }_{\mathrm{ih}}F}$$
20	18 19	eqtr4i	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)=\overline{S\left(G{\cdot }_{\mathrm{ih}}F\right)}$$
21	16 20	oveq12i	$$⊢S\left(G{\cdot }_{\mathrm{ih}}F\right)+\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)=\overline{\stackrel{‾}{S}\left(F{\cdot }_{\mathrm{ih}}G\right)}+\overline{S\left(G{\cdot }_{\mathrm{ih}}F\right)}$$
22	10 21	eqtr4i	$$⊢\overline{\stackrel{‾}{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)}=S\left(G{\cdot }_{\mathrm{ih}}F\right)+\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)$$
23	7 9	addcomi	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)=S\left(G{\cdot }_{\mathrm{ih}}F\right)+\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)$$
24	22 23	eqtr4i	$$⊢\overline{\stackrel{‾}{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)}=\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)$$
25	7 9	addcli	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\in ℂ$$
26	25	cjrebi	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\in ℝ\leftrightarrow \overline{\stackrel{‾}{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)}=\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)$$
27	24 26	mpbir	$$⊢\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\in ℝ$$
28	27	renegcli	$$⊢-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)\in ℝ$$
29	4 28	eqeltri	$$⊢B\in ℝ$$