Metamath Proof Explorer


Theorem normlem4

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

Ref Expression
Hypotheses normlem1.1 𝑆 ∈ ℂ
normlem1.2 𝐹 ∈ ℋ
normlem1.3 𝐺 ∈ ℋ
normlem2.4 𝐵 = - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) )
normlem3.5 𝐴 = ( 𝐺 ·ih 𝐺 )
normlem3.6 𝐶 = ( 𝐹 ·ih 𝐹 )
normlem4.7 𝑅 ∈ ℝ
normlem4.8 ( abs ‘ 𝑆 ) = 1
Assertion normlem4 ( ( 𝐹 ( ( 𝑆 · 𝑅 ) · 𝐺 ) ) ·ih ( 𝐹 ( ( 𝑆 · 𝑅 ) · 𝐺 ) ) ) = ( ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) + 𝐶 )

Proof

Step Hyp Ref Expression
1 normlem1.1 𝑆 ∈ ℂ
2 normlem1.2 𝐹 ∈ ℋ
3 normlem1.3 𝐺 ∈ ℋ
4 normlem2.4 𝐵 = - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) )
5 normlem3.5 𝐴 = ( 𝐺 ·ih 𝐺 )
6 normlem3.6 𝐶 = ( 𝐹 ·ih 𝐹 )
7 normlem4.7 𝑅 ∈ ℝ
8 normlem4.8 ( abs ‘ 𝑆 ) = 1
9 1 2 3 7 8 normlem1 ( ( 𝐹 ( ( 𝑆 · 𝑅 ) · 𝐺 ) ) ·ih ( 𝐹 ( ( 𝑆 · 𝑅 ) · 𝐺 ) ) ) = ( ( ( 𝐹 ·ih 𝐹 ) + ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) ) + ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) )
10 1 2 3 4 5 6 7 normlem3 ( ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) + 𝐶 ) = ( ( ( 𝐹 ·ih 𝐹 ) + ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) ) + ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) )
11 9 10 eqtr4i ( ( 𝐹 ( ( 𝑆 · 𝑅 ) · 𝐺 ) ) ·ih ( 𝐹 ( ( 𝑆 · 𝑅 ) · 𝐺 ) ) ) = ( ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) + 𝐶 )