Metamath Proof Explorer

Theorem normlem1

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 22-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses normlem1.1 ${⊢}{S}\in ℂ$
normlem1.2 ${⊢}{F}\in ℋ$
normlem1.3 ${⊢}{G}\in ℋ$
normlem1.4 ${⊢}{R}\in ℝ$
normlem1.5 ${⊢}\left|{S}\right|=1$
Assertion normlem1 ${⊢}\left({F}{-}_{ℎ}\left({S}{R}{\cdot }_{ℎ}{G}\right)\right){\cdot }_{\mathrm{ih}}\left({F}{-}_{ℎ}\left({S}{R}{\cdot }_{ℎ}{G}\right)\right)=\left({F}{\cdot }_{\mathrm{ih}}{F}\right)+\stackrel{‾}{{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 ℋ$
3 normlem1.3 ${⊢}{G}\in ℋ$
4 normlem1.4 ${⊢}{R}\in ℝ$
5 normlem1.5 ${⊢}\left|{S}\right|=1$
6 4 recni ${⊢}{R}\in ℂ$
7 1 6 mulcli ${⊢}{S}{R}\in ℂ$
8 7 2 3 normlem0 ${⊢}\left({F}{-}_{ℎ}\left({S}{R}{\cdot }_{ℎ}{G}\right)\right){\cdot }_{\mathrm{ih}}\left({F}{-}_{ℎ}\left({S}{R}{\cdot }_{ℎ}{G}\right)\right)=\left({F}{\cdot }_{\mathrm{ih}}{F}\right)+\left(-\stackrel{‾}{{S}{R}}\right)\left({F}{\cdot }_{\mathrm{ih}}{G}\right)+\left(-{S}{R}\right)\left({G}{\cdot }_{\mathrm{ih}}{F}\right)+{S}{R}\stackrel{‾}{{S}{R}}\left({G}{\cdot }_{\mathrm{ih}}{G}\right)$
9 1 6 cjmuli ${⊢}\stackrel{‾}{{S}{R}}=\stackrel{‾}{{S}}\stackrel{‾}{{R}}$
10 6 cjrebi ${⊢}{R}\in ℝ↔\stackrel{‾}{{R}}={R}$
11 4 10 mpbi ${⊢}\stackrel{‾}{{R}}={R}$
12 11 oveq2i ${⊢}\stackrel{‾}{{S}}\stackrel{‾}{{R}}=\stackrel{‾}{{S}}{R}$
13 9 12 eqtri ${⊢}\stackrel{‾}{{S}{R}}=\stackrel{‾}{{S}}{R}$
14 13 negeqi ${⊢}-\stackrel{‾}{{S}{R}}=-\stackrel{‾}{{S}}{R}$
15 1 cjcli ${⊢}\stackrel{‾}{{S}}\in ℂ$
16 15 6 mulneg2i ${⊢}\stackrel{‾}{{S}}\left(-{R}\right)=-\stackrel{‾}{{S}}{R}$
17 14 16 eqtr4i ${⊢}-\stackrel{‾}{{S}{R}}=\stackrel{‾}{{S}}\left(-{R}\right)$
18 17 oveq1i ${⊢}\left(-\stackrel{‾}{{S}{R}}\right)\left({F}{\cdot }_{\mathrm{ih}}{G}\right)=\stackrel{‾}{{S}}\left(-{R}\right)\left({F}{\cdot }_{\mathrm{ih}}{G}\right)$
19 18 oveq2i ${⊢}\left({F}{\cdot }_{\mathrm{ih}}{F}\right)+\left(-\stackrel{‾}{{S}{R}}\right)\left({F}{\cdot }_{\mathrm{ih}}{G}\right)=\left({F}{\cdot }_{\mathrm{ih}}{F}\right)+\stackrel{‾}{{S}}\left(-{R}\right)\left({F}{\cdot }_{\mathrm{ih}}{G}\right)$
20 1 6 mulneg2i ${⊢}{S}\left(-{R}\right)=-{S}{R}$
21 20 eqcomi ${⊢}-{S}{R}={S}\left(-{R}\right)$
22 21 oveq1i ${⊢}\left(-{S}{R}\right)\left({G}{\cdot }_{\mathrm{ih}}{F}\right)={S}\left(-{R}\right)\left({G}{\cdot }_{\mathrm{ih}}{F}\right)$
23 9 oveq2i ${⊢}{S}{R}\stackrel{‾}{{S}{R}}={S}{R}\stackrel{‾}{{S}}\stackrel{‾}{{R}}$
24 6 cjcli ${⊢}\stackrel{‾}{{R}}\in ℂ$
25 1 6 15 24 mul4i ${⊢}{S}{R}\stackrel{‾}{{S}}\stackrel{‾}{{R}}={S}\stackrel{‾}{{S}}{R}\stackrel{‾}{{R}}$
26 5 oveq1i ${⊢}{\left|{S}\right|}^{2}={1}^{2}$
27 1 absvalsqi ${⊢}{\left|{S}\right|}^{2}={S}\stackrel{‾}{{S}}$
28 sq1 ${⊢}{1}^{2}=1$
29 26 27 28 3eqtr3i ${⊢}{S}\stackrel{‾}{{S}}=1$
30 11 oveq2i ${⊢}{R}\stackrel{‾}{{R}}={R}{R}$
31 29 30 oveq12i ${⊢}{S}\stackrel{‾}{{S}}{R}\stackrel{‾}{{R}}=1{R}{R}$
32 6 6 mulcli ${⊢}{R}{R}\in ℂ$
33 32 mulid2i ${⊢}1{R}{R}={R}{R}$
34 31 33 eqtri ${⊢}{S}\stackrel{‾}{{S}}{R}\stackrel{‾}{{R}}={R}{R}$
35 25 34 eqtri ${⊢}{S}{R}\stackrel{‾}{{S}}\stackrel{‾}{{R}}={R}{R}$
36 23 35 eqtri ${⊢}{S}{R}\stackrel{‾}{{S}{R}}={R}{R}$
37 6 sqvali ${⊢}{{R}}^{2}={R}{R}$
38 36 37 eqtr4i ${⊢}{S}{R}\stackrel{‾}{{S}{R}}={{R}}^{2}$
39 38 oveq1i ${⊢}{S}{R}\stackrel{‾}{{S}{R}}\left({G}{\cdot }_{\mathrm{ih}}{G}\right)={{R}}^{2}\left({G}{\cdot }_{\mathrm{ih}}{G}\right)$
40 22 39 oveq12i ${⊢}\left(-{S}{R}\right)\left({G}{\cdot }_{\mathrm{ih}}{F}\right)+{S}{R}\stackrel{‾}{{S}{R}}\left({G}{\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)$
41 19 40 oveq12i ${⊢}\left({F}{\cdot }_{\mathrm{ih}}{F}\right)+\left(-\stackrel{‾}{{S}{R}}\right)\left({F}{\cdot }_{\mathrm{ih}}{G}\right)+\left(-{S}{R}\right)\left({G}{\cdot }_{\mathrm{ih}}{F}\right)+{S}{R}\stackrel{‾}{{S}{R}}\left({G}{\cdot }_{\mathrm{ih}}{G}\right)=\left({F}{\cdot }_{\mathrm{ih}}{F}\right)+\stackrel{‾}{{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 8 41 eqtri ${⊢}\left({F}{-}_{ℎ}\left({S}{R}{\cdot }_{ℎ}{G}\right)\right){\cdot }_{\mathrm{ih}}\left({F}{-}_{ℎ}\left({S}{R}{\cdot }_{ℎ}{G}\right)\right)=\left({F}{\cdot }_{\mathrm{ih}}{F}\right)+\stackrel{‾}{{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)$