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 ) ) + ( 𝐵 · 𝑅 ) ) + 𝐶 )