This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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