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 ⋅ ih F - ℎ S ⋅ ℎ G = F ⋅ ih F + − S ‾ ⁢ F ⋅ ih G + − S ⁢ G ⋅ ih F + S ⁢ S ‾ ⁢ G ⋅ ih G

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 ⋅ ih F - ℎ S ⋅ ℎ G = F + ℎ − S ⋅ ℎ G ⋅ ih F + ℎ − 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 ⋅ ih F + ℎ − S ⋅ ℎ G = F ⋅ ih F + ℎ − S ⋅ ℎ G + − S ⋅ ℎ G ⋅ ih F + ℎ − S ⋅ ℎ G
18 2 15 16 17 mp3an ⊢ F + ℎ − S ⋅ ℎ G ⋅ ih F + ℎ − S ⋅ ℎ G = F ⋅ ih F + ℎ − S ⋅ ℎ G + − S ⋅ ℎ G ⋅ ih F + ℎ − S ⋅ ℎ G
19 his7 ⊢ F ∈ ℋ ∧ F ∈ ℋ ∧ − S ⋅ ℎ G ∈ ℋ → F ⋅ ih F + ℎ − S ⋅ ℎ G = F ⋅ ih F + F ⋅ ih − S ⋅ ℎ G
20 2 2 15 19 mp3an ⊢ F ⋅ ih F + ℎ − S ⋅ ℎ G = F ⋅ ih F + F ⋅ ih − S ⋅ ℎ G
21 his5 ⊢ − S ∈ ℂ ∧ F ∈ ℋ ∧ G ∈ ℋ → F ⋅ ih − S ⋅ ℎ G = − S ‾ ⁢ F ⋅ ih G
22 14 2 3 21 mp3an ⊢ F ⋅ ih − S ⋅ ℎ G = − S ‾ ⁢ F ⋅ ih G
23 1 cjnegi ⊢ − S ‾ = − S ‾
24 23 oveq1i ⊢ − S ‾ ⁢ F ⋅ ih G = − S ‾ ⁢ F ⋅ ih G
25 22 24 eqtri ⊢ F ⋅ ih − S ⋅ ℎ G = − S ‾ ⁢ F ⋅ ih G
26 25 oveq2i ⊢ F ⋅ ih F + F ⋅ ih − S ⋅ ℎ G = F ⋅ ih F + − S ‾ ⁢ F ⋅ ih G
27 20 26 eqtri ⊢ F ⋅ ih F + ℎ − S ⋅ ℎ G = F ⋅ ih F + − S ‾ ⁢ F ⋅ ih G
28 ax-his3 ⊢ − S ∈ ℂ ∧ G ∈ ℋ ∧ F + ℎ − S ⋅ ℎ G ∈ ℋ → − S ⋅ ℎ G ⋅ ih F + ℎ − S ⋅ ℎ G = − S ⁢ G ⋅ ih F + ℎ − S ⋅ ℎ G
29 14 3 16 28 mp3an ⊢ − S ⋅ ℎ G ⋅ ih F + ℎ − S ⋅ ℎ G = − S ⁢ G ⋅ ih F + ℎ − S ⋅ ℎ G
30 his7 ⊢ G ∈ ℋ ∧ F ∈ ℋ ∧ − S ⋅ ℎ G ∈ ℋ → G ⋅ ih F + ℎ − S ⋅ ℎ G = G ⋅ ih F + G ⋅ ih − S ⋅ ℎ G
31 3 2 15 30 mp3an ⊢ G ⋅ ih F + ℎ − S ⋅ ℎ G = G ⋅ ih F + G ⋅ ih − S ⋅ ℎ G
32 his5 ⊢ − S ∈ ℂ ∧ G ∈ ℋ ∧ G ∈ ℋ → G ⋅ ih − S ⋅ ℎ G = − S ‾ ⁢ G ⋅ ih G
33 14 3 3 32 mp3an ⊢ G ⋅ ih − S ⋅ ℎ G = − S ‾ ⁢ G ⋅ ih G
34 33 oveq2i ⊢ G ⋅ ih F + G ⋅ ih − S ⋅ ℎ G = G ⋅ ih F + − S ‾ ⁢ G ⋅ ih G
35 31 34 eqtri ⊢ G ⋅ ih F + ℎ − S ⋅ ℎ G = G ⋅ ih F + − S ‾ ⁢ G ⋅ ih G
36 35 oveq2i ⊢ − S ⁢ G ⋅ ih F + ℎ − S ⋅ ℎ G = − S ⁢ G ⋅ ih F + − S ‾ ⁢ G ⋅ ih G
37 3 2 hicli ⊢ G ⋅ ih F ∈ ℂ
38 14 cjcli ⊢ − S ‾ ∈ ℂ
39 3 3 hicli ⊢ G ⋅ ih G ∈ ℂ
40 38 39 mulcli ⊢ − S ‾ ⁢ G ⋅ ih G ∈ ℂ
41 14 37 40 adddii ⊢ − S ⁢ G ⋅ ih F + − S ‾ ⁢ G ⋅ ih G = − S ⁢ G ⋅ ih F + − S ⁢ − S ‾ ⁢ G ⋅ ih G
42 14 38 39 mulassi ⊢ − S ⁢ − S ‾ ⁢ G ⋅ ih G = − S ⁢ − S ‾ ⁢ G ⋅ ih G
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 ⋅ ih G = S ⁢ S ‾ ⁢ G ⋅ ih G
48 42 47 eqtr3i ⊢ − S ⁢ − S ‾ ⁢ G ⋅ ih G = S ⁢ S ‾ ⁢ G ⋅ ih G
49 48 oveq2i ⊢ − S ⁢ G ⋅ ih F + − S ⁢ − S ‾ ⁢ G ⋅ ih G = − S ⁢ G ⋅ ih F + S ⁢ S ‾ ⁢ G ⋅ ih G
50 41 49 eqtri ⊢ − S ⁢ G ⋅ ih F + − S ‾ ⁢ G ⋅ ih G = − S ⁢ G ⋅ ih F + S ⁢ S ‾ ⁢ G ⋅ ih G
51 29 36 50 3eqtri ⊢ − S ⋅ ℎ G ⋅ ih F + ℎ − S ⋅ ℎ G = − S ⁢ G ⋅ ih F + S ⁢ S ‾ ⁢ G ⋅ ih G
52 27 51 oveq12i ⊢ F ⋅ ih F + ℎ − S ⋅ ℎ G + − S ⋅ ℎ G ⋅ ih F + ℎ − S ⋅ ℎ G = F ⋅ ih F + − S ‾ ⁢ F ⋅ ih G + − S ⁢ G ⋅ ih F + S ⁢ S ‾ ⁢ G ⋅ ih G
53 13 18 52 3eqtri ⊢ F - ℎ S ⋅ ℎ G ⋅ ih F - ℎ S ⋅ ℎ G = F ⋅ ih F + − S ‾ ⁢ F ⋅ ih G + − S ⁢ G ⋅ ih F + S ⁢ S ‾ ⁢ G ⋅ ih G