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 ⊢ 𝑆 ∈ ℂ
normlem1.2 ⊢ 𝐹 ∈ ℋ
normlem1.3 ⊢ 𝐺 ∈ ℋ
Assertion normlem0 ( ( 𝐹 −ℎ ( 𝑆 ·ℎ 𝐺 ) ) ·ih ( 𝐹 −ℎ ( 𝑆 ·ℎ 𝐺 ) ) ) = ( ( ( 𝐹 ·ih 𝐹 ) + ( - ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) ) + ( ( - 𝑆 · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑆 · ( ∗ ‘ 𝑆 ) ) · ( 𝐺 ·ih 𝐺 ) ) ) )

Proof

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