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∈ℂ
normlem1.2 ⊢F∈ℋ
normlem1.3 ⊢G∈ℋ
normlem1.4 ⊢R∈ℝ
normlem1.5 ⊢S=1
Assertion normlem1 ⊢F-ℎS⁢R⋅ℎG⋅ihF-ℎS⁢R⋅ℎG=F⋅ihF+S‾⁢−R⁢F⋅ihG+S⁢−R⁢G⋅ihF+R2⁢G⋅ihG

Proof

Step Hyp Ref Expression
1 normlem1.1 ⊢S∈ℂ
2 normlem1.2 ⊢F∈ℋ
3 normlem1.3 ⊢G∈ℋ
4 normlem1.4 ⊢R∈ℝ
5 normlem1.5 ⊢S=1
6 4 recni ⊢R∈ℂ
7 1 6 mulcli ⊢S⁢R∈ℂ
8 7 2 3 normlem0 ⊢F-ℎS⁢R⋅ℎG⋅ihF-ℎS⁢R⋅ℎG=F⋅ihF+−S⁢R‾⁢F⋅ihG+−S⁢R⁢G⋅ihF+S⁢R⁢S⁢R‾⁢G⋅ihG
9 1 6 cjmuli ⊢S⁢R‾=S‾⁢R‾
10 6 cjrebi ⊢R∈ℝ↔R‾=R
11 4 10 mpbi ⊢R‾=R
12 11 oveq2i ⊢S‾⁢R‾=S‾⁢R
13 9 12 eqtri ⊢S⁢R‾=S‾⁢R
14 13 negeqi ⊢−S⁢R‾=−S‾⁢R
15 1 cjcli ⊢S‾∈ℂ
16 15 6 mulneg2i ⊢S‾⁢−R=−S‾⁢R
17 14 16 eqtr4i ⊢−S⁢R‾=S‾⁢−R
18 17 oveq1i ⊢−S⁢R‾⁢F⋅ihG=S‾⁢−R⁢F⋅ihG
19 18 oveq2i ⊢F⋅ihF+−S⁢R‾⁢F⋅ihG=F⋅ihF+S‾⁢−R⁢F⋅ihG
20 1 6 mulneg2i ⊢S⁢−R=−S⁢R
21 20 eqcomi ⊢−S⁢R=S⁢−R
22 21 oveq1i ⊢−S⁢R⁢G⋅ihF=S⁢−R⁢G⋅ihF
23 9 oveq2i ⊢S⁢R⁢S⁢R‾=S⁢R⁢S‾⁢R‾
24 6 cjcli ⊢R‾∈ℂ
25 1 6 15 24 mul4i ⊢S⁢R⁢S‾⁢R‾=S⁢S‾⁢R⁢R‾
26 5 oveq1i ⊢S2=12
27 1 absvalsqi ⊢S2=S⁢S‾
28 sq1 ⊢12=1
29 26 27 28 3eqtr3i ⊢S⁢S‾=1
30 11 oveq2i ⊢R⁢R‾=R⁢R
31 29 30 oveq12i ⊢S⁢S‾⁢R⁢R‾=1⁢R⁢R
32 6 6 mulcli ⊢R⁢R∈ℂ
33 32 mullidi ⊢1⁢R⁢R=R⁢R
34 31 33 eqtri ⊢S⁢S‾⁢R⁢R‾=R⁢R
35 25 34 eqtri ⊢S⁢R⁢S‾⁢R‾=R⁢R
36 23 35 eqtri ⊢S⁢R⁢S⁢R‾=R⁢R
37 6 sqvali ⊢R2=R⁢R
38 36 37 eqtr4i ⊢S⁢R⁢S⁢R‾=R2
39 38 oveq1i ⊢S⁢R⁢S⁢R‾⁢G⋅ihG=R2⁢G⋅ihG
40 22 39 oveq12i ⊢−S⁢R⁢G⋅ihF+S⁢R⁢S⁢R‾⁢G⋅ihG=S⁢−R⁢G⋅ihF+R2⁢G⋅ihG
41 19 40 oveq12i ⊢F⋅ihF+−S⁢R‾⁢F⋅ihG+−S⁢R⁢G⋅ihF+S⁢R⁢S⁢R‾⁢G⋅ihG=F⋅ihF+S‾⁢−R⁢F⋅ihG+S⁢−R⁢G⋅ihF+R2⁢G⋅ihG
42 8 41 eqtri ⊢F-ℎS⁢R⋅ℎG⋅ihF-ℎS⁢R⋅ℎG=F⋅ihF+S‾⁢−R⁢F⋅ihG+S⁢−R⁢G⋅ihF+R2⁢G⋅ihG