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 ⊢ 𝑆 ∈ ℂ
normlem1.2 ⊢ 𝐹 ∈ ℋ
normlem1.3 ⊢ 𝐺 ∈ ℋ
normlem1.4 ⊢ 𝑅 ∈ ℝ
normlem1.5 ⊢ ( abs ‘ 𝑆 ) = 1
Assertion normlem1 ( ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ·ih ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ) = ( ( ( 𝐹 ·ih 𝐹 ) + ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) ) + ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) )

Proof

Step Hyp Ref Expression
1 normlem1.1 ⊢ 𝑆 ∈ ℂ
2 normlem1.2 ⊢ 𝐹 ∈ ℋ
3 normlem1.3 ⊢ 𝐺 ∈ ℋ
4 normlem1.4 ⊢ 𝑅 ∈ ℝ
5 normlem1.5 ⊢ ( abs ‘ 𝑆 ) = 1
6 4 recni ⊢ 𝑅 ∈ ℂ
7 1 6 mulcli ⊢ ( 𝑆 · 𝑅 ) ∈ ℂ
8 7 2 3 normlem0 ⊢ ( ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ·ih ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ) = ( ( ( 𝐹 ·ih 𝐹 ) + ( - ( ∗ ‘ ( 𝑆 · 𝑅 ) ) · ( 𝐹 ·ih 𝐺 ) ) ) + ( ( - ( 𝑆 · 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( ( 𝑆 · 𝑅 ) · ( ∗ ‘ ( 𝑆 · 𝑅 ) ) ) · ( 𝐺 ·ih 𝐺 ) ) ) )
9 1 6 cjmuli ⊢ ( ∗ ‘ ( 𝑆 · 𝑅 ) ) = ( ( ∗ ‘ 𝑆 ) · ( ∗ ‘ 𝑅 ) )
10 6 cjrebi ⊢ ( 𝑅 ∈ ℝ ↔ ( ∗ ‘ 𝑅 ) = 𝑅 )
11 4 10 mpbi ⊢ ( ∗ ‘ 𝑅 ) = 𝑅
12 11 oveq2i ⊢ ( ( ∗ ‘ 𝑆 ) · ( ∗ ‘ 𝑅 ) ) = ( ( ∗ ‘ 𝑆 ) · 𝑅 )
13 9 12 eqtri ⊢ ( ∗ ‘ ( 𝑆 · 𝑅 ) ) = ( ( ∗ ‘ 𝑆 ) · 𝑅 )
14 13 negeqi ⊢ - ( ∗ ‘ ( 𝑆 · 𝑅 ) ) = - ( ( ∗ ‘ 𝑆 ) · 𝑅 )
15 1 cjcli ⊢ ( ∗ ‘ 𝑆 ) ∈ ℂ
16 15 6 mulneg2i ⊢ ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) = - ( ( ∗ ‘ 𝑆 ) · 𝑅 )
17 14 16 eqtr4i ⊢ - ( ∗ ‘ ( 𝑆 · 𝑅 ) ) = ( ( ∗ ‘ 𝑆 ) · - 𝑅 )
18 17 oveq1i ⊢ ( - ( ∗ ‘ ( 𝑆 · 𝑅 ) ) · ( 𝐹 ·ih 𝐺 ) ) = ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) )
19 18 oveq2i ⊢ ( ( 𝐹 ·ih 𝐹 ) + ( - ( ∗ ‘ ( 𝑆 · 𝑅 ) ) · ( 𝐹 ·ih 𝐺 ) ) ) = ( ( 𝐹 ·ih 𝐹 ) + ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) )
20 1 6 mulneg2i ⊢ ( 𝑆 · - 𝑅 ) = - ( 𝑆 · 𝑅 )
21 20 eqcomi ⊢ - ( 𝑆 · 𝑅 ) = ( 𝑆 · - 𝑅 )
22 21 oveq1i ⊢ ( - ( 𝑆 · 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) = ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) )
23 9 oveq2i ⊢ ( ( 𝑆 · 𝑅 ) · ( ∗ ‘ ( 𝑆 · 𝑅 ) ) ) = ( ( 𝑆 · 𝑅 ) · ( ( ∗ ‘ 𝑆 ) · ( ∗ ‘ 𝑅 ) ) )
24 6 cjcli ⊢ ( ∗ ‘ 𝑅 ) ∈ ℂ
25 1 6 15 24 mul4i ⊢ ( ( 𝑆 · 𝑅 ) · ( ( ∗ ‘ 𝑆 ) · ( ∗ ‘ 𝑅 ) ) ) = ( ( 𝑆 · ( ∗ ‘ 𝑆 ) ) · ( 𝑅 · ( ∗ ‘ 𝑅 ) ) )
26 5 oveq1i ⊢ ( ( abs ‘ 𝑆 ) ↑ 2 ) = ( 1 ↑ 2 )
27 1 absvalsqi ⊢ ( ( abs ‘ 𝑆 ) ↑ 2 ) = ( 𝑆 · ( ∗ ‘ 𝑆 ) )
28 sq1 ⊢ ( 1 ↑ 2 ) = 1
29 26 27 28 3eqtr3i ⊢ ( 𝑆 · ( ∗ ‘ 𝑆 ) ) = 1
30 11 oveq2i ⊢ ( 𝑅 · ( ∗ ‘ 𝑅 ) ) = ( 𝑅 · 𝑅 )
31 29 30 oveq12i ⊢ ( ( 𝑆 · ( ∗ ‘ 𝑆 ) ) · ( 𝑅 · ( ∗ ‘ 𝑅 ) ) ) = ( 1 · ( 𝑅 · 𝑅 ) )
32 6 6 mulcli ⊢ ( 𝑅 · 𝑅 ) ∈ ℂ
33 32 mulid2i ⊢ ( 1 · ( 𝑅 · 𝑅 ) ) = ( 𝑅 · 𝑅 )
34 31 33 eqtri ⊢ ( ( 𝑆 · ( ∗ ‘ 𝑆 ) ) · ( 𝑅 · ( ∗ ‘ 𝑅 ) ) ) = ( 𝑅 · 𝑅 )
35 25 34 eqtri ⊢ ( ( 𝑆 · 𝑅 ) · ( ( ∗ ‘ 𝑆 ) · ( ∗ ‘ 𝑅 ) ) ) = ( 𝑅 · 𝑅 )
36 23 35 eqtri ⊢ ( ( 𝑆 · 𝑅 ) · ( ∗ ‘ ( 𝑆 · 𝑅 ) ) ) = ( 𝑅 · 𝑅 )
37 6 sqvali ⊢ ( 𝑅 ↑ 2 ) = ( 𝑅 · 𝑅 )
38 36 37 eqtr4i ⊢ ( ( 𝑆 · 𝑅 ) · ( ∗ ‘ ( 𝑆 · 𝑅 ) ) ) = ( 𝑅 ↑ 2 )
39 38 oveq1i ⊢ ( ( ( 𝑆 · 𝑅 ) · ( ∗ ‘ ( 𝑆 · 𝑅 ) ) ) · ( 𝐺 ·ih 𝐺 ) ) = ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) )
40 22 39 oveq12i ⊢ ( ( - ( 𝑆 · 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( ( 𝑆 · 𝑅 ) · ( ∗ ‘ ( 𝑆 · 𝑅 ) ) ) · ( 𝐺 ·ih 𝐺 ) ) ) = ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) )
41 19 40 oveq12i ⊢ ( ( ( 𝐹 ·ih 𝐹 ) + ( - ( ∗ ‘ ( 𝑆 · 𝑅 ) ) · ( 𝐹 ·ih 𝐺 ) ) ) + ( ( - ( 𝑆 · 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( ( 𝑆 · 𝑅 ) · ( ∗ ‘ ( 𝑆 · 𝑅 ) ) ) · ( 𝐺 ·ih 𝐺 ) ) ) ) = ( ( ( 𝐹 ·ih 𝐹 ) + ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) ) + ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) )
42 8 41 eqtri ⊢ ( ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ·ih ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ) = ( ( ( 𝐹 ·ih 𝐹 ) + ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) ) + ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) )