Metamath Proof Explorer

Theorem normlem0

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

Ref Expression
Hypotheses normlem1.1 ⊢S∈ℂ
normlem1.2 ⊢F∈ℋ
normlem1.3 ⊢G∈ℋ
Assertion normlem0 ⊢F-ℎS⋅ℎG⋅ihF-ℎS⋅ℎG=F⋅ihF+−S‾⁢F⋅ihG+−S⁢G⋅ihF+S⁢S‾⁢G⋅ihG

Proof

Step Hyp Ref Expression
1 normlem1.1 ⊢S∈ℂ
2 normlem1.2 ⊢F∈ℋ
3 normlem1.3 ⊢G∈ℋ
4 1 3 hvmulcli ⊢S⋅ℎG∈ℋ
5 2 4 hvsubvali ⊢F-ℎS⋅ℎG=F+ℎ-1⋅ℎS⋅ℎG
6 1 mulm1i ⊢-1⁢S=−S
7 6 oveq1i ⊢-1⁢S⋅ℎG=−S⋅ℎG
8 neg1cn ⊢−1∈ℂ
9 8 1 3 hvmulassi ⊢-1⁢S⋅ℎG=-1⋅ℎS⋅ℎG
10 7 9 eqtr3i ⊢−S⋅ℎG=-1⋅ℎS⋅ℎG
11 10 oveq2i ⊢F+ℎ−S⋅ℎG=F+ℎ-1⋅ℎS⋅ℎG
12 5 11 eqtr4i ⊢F-ℎS⋅ℎG=F+ℎ−S⋅ℎG
13 12 12 oveq12i ⊢F-ℎS⋅ℎG⋅ihF-ℎS⋅ℎG=F+ℎ−S⋅ℎG⋅ihF+ℎ−S⋅ℎG
14 1 negcli ⊢−S∈ℂ
15 14 3 hvmulcli ⊢−S⋅ℎG∈ℋ
16 2 15 hvaddcli ⊢F+ℎ−S⋅ℎG∈ℋ
17 ax-his2 ⊢F∈ℋ∧−S⋅ℎG∈ℋ∧F+ℎ−S⋅ℎG∈ℋ→F+ℎ−S⋅ℎG⋅ihF+ℎ−S⋅ℎG=F⋅ihF+ℎ−S⋅ℎG+−S⋅ℎG⋅ihF+ℎ−S⋅ℎG
18 2 15 16 17 mp3an ⊢F+ℎ−S⋅ℎG⋅ihF+ℎ−S⋅ℎG=F⋅ihF+ℎ−S⋅ℎG+−S⋅ℎG⋅ihF+ℎ−S⋅ℎG
19 his7 ⊢F∈ℋ∧F∈ℋ∧−S⋅ℎG∈ℋ→F⋅ihF+ℎ−S⋅ℎG=F⋅ihF+F⋅ih−S⋅ℎG
20 2 2 15 19 mp3an ⊢F⋅ihF+ℎ−S⋅ℎG=F⋅ihF+F⋅ih−S⋅ℎG
21 his5 ⊢−S∈ℂ∧F∈ℋ∧G∈ℋ→F⋅ih−S⋅ℎG=−S‾⁢F⋅ihG
22 14 2 3 21 mp3an ⊢F⋅ih−S⋅ℎG=−S‾⁢F⋅ihG
23 1 cjnegi ⊢−S‾=−S‾
24 23 oveq1i ⊢−S‾⁢F⋅ihG=−S‾⁢F⋅ihG
25 22 24 eqtri ⊢F⋅ih−S⋅ℎG=−S‾⁢F⋅ihG
26 25 oveq2i ⊢F⋅ihF+F⋅ih−S⋅ℎG=F⋅ihF+−S‾⁢F⋅ihG
27 20 26 eqtri ⊢F⋅ihF+ℎ−S⋅ℎG=F⋅ihF+−S‾⁢F⋅ihG
28 ax-his3 ⊢−S∈ℂ∧G∈ℋ∧F+ℎ−S⋅ℎG∈ℋ→−S⋅ℎG⋅ihF+ℎ−S⋅ℎG=−S⁢G⋅ihF+ℎ−S⋅ℎG
29 14 3 16 28 mp3an ⊢−S⋅ℎG⋅ihF+ℎ−S⋅ℎG=−S⁢G⋅ihF+ℎ−S⋅ℎG
30 his7 ⊢G∈ℋ∧F∈ℋ∧−S⋅ℎG∈ℋ→G⋅ihF+ℎ−S⋅ℎG=G⋅ihF+G⋅ih−S⋅ℎG
31 3 2 15 30 mp3an ⊢G⋅ihF+ℎ−S⋅ℎG=G⋅ihF+G⋅ih−S⋅ℎG
32 his5 ⊢−S∈ℂ∧G∈ℋ∧G∈ℋ→G⋅ih−S⋅ℎG=−S‾⁢G⋅ihG
33 14 3 3 32 mp3an ⊢G⋅ih−S⋅ℎG=−S‾⁢G⋅ihG
34 33 oveq2i ⊢G⋅ihF+G⋅ih−S⋅ℎG=G⋅ihF+−S‾⁢G⋅ihG
35 31 34 eqtri ⊢G⋅ihF+ℎ−S⋅ℎG=G⋅ihF+−S‾⁢G⋅ihG
36 35 oveq2i ⊢−S⁢G⋅ihF+ℎ−S⋅ℎG=−S⁢G⋅ihF+−S‾⁢G⋅ihG
37 3 2 hicli ⊢G⋅ihF∈ℂ
38 14 cjcli ⊢−S‾∈ℂ
39 3 3 hicli ⊢G⋅ihG∈ℂ
40 38 39 mulcli ⊢−S‾⁢G⋅ihG∈ℂ
41 14 37 40 adddii ⊢−S⁢G⋅ihF+−S‾⁢G⋅ihG=−S⁢G⋅ihF+−S⁢−S‾⁢G⋅ihG
42 14 38 39 mulassi ⊢−S⁢−S‾⁢G⋅ihG=−S⁢−S‾⁢G⋅ihG
43 23 oveq2i ⊢−S⁢−S‾=−S⁢−S‾
44 1 cjcli ⊢S‾∈ℂ
45 1 44 mul2negi ⊢−S⁢−S‾=S⁢S‾
46 43 45 eqtri ⊢−S⁢−S‾=S⁢S‾
47 46 oveq1i ⊢−S⁢−S‾⁢G⋅ihG=S⁢S‾⁢G⋅ihG
48 42 47 eqtr3i ⊢−S⁢−S‾⁢G⋅ihG=S⁢S‾⁢G⋅ihG
49 48 oveq2i ⊢−S⁢G⋅ihF+−S⁢−S‾⁢G⋅ihG=−S⁢G⋅ihF+S⁢S‾⁢G⋅ihG
50 41 49 eqtri ⊢−S⁢G⋅ihF+−S‾⁢G⋅ihG=−S⁢G⋅ihF+S⁢S‾⁢G⋅ihG
51 29 36 50 3eqtri ⊢−S⋅ℎG⋅ihF+ℎ−S⋅ℎG=−S⁢G⋅ihF+S⁢S‾⁢G⋅ihG
52 27 51 oveq12i ⊢F⋅ihF+ℎ−S⋅ℎG+−S⋅ℎG⋅ihF+ℎ−S⋅ℎG=F⋅ihF+−S‾⁢F⋅ihG+−S⁢G⋅ihF+S⁢S‾⁢G⋅ihG
53 13 18 52 3eqtri ⊢F-ℎS⋅ℎG⋅ihF-ℎS⋅ℎG=F⋅ihF+−S‾⁢F⋅ihG+−S⁢G⋅ihF+S⁢S‾⁢G⋅ihG