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 ⊢ S ∈ ℂ
normlem1.2 ⊢ F ∈ ℋ
normlem1.3 ⊢ G ∈ ℋ
normlem2.4 ⊢ B = − S ‾ ⁢ F ⋅ ih G + S ⁢ G ⋅ ih F
normlem3.5 ⊢ A = G ⋅ ih G
normlem3.6 ⊢ C = F ⋅ ih F
normlem4.7 ⊢ R ∈ ℝ
normlem4.8 ⊢ S = 1
Assertion normlem4 ⊢ F - ℎ S ⁢ R ⋅ ℎ G ⋅ ih F - ℎ S ⁢ R ⋅ ℎ G = A ⁢ R 2 + B ⁢ R + C

Proof

Step Hyp Ref Expression
1 normlem1.1 ⊢ S ∈ ℂ
2 normlem1.2 ⊢ F ∈ ℋ
3 normlem1.3 ⊢ G ∈ ℋ
4 normlem2.4 ⊢ B = − S ‾ ⁢ F ⋅ ih G + S ⁢ G ⋅ ih F
5 normlem3.5 ⊢ A = G ⋅ ih G
6 normlem3.6 ⊢ C = F ⋅ ih F
7 normlem4.7 ⊢ R ∈ ℝ
8 normlem4.8 ⊢ S = 1
9 1 2 3 7 8 normlem1 ⊢ F - ℎ S ⁢ R ⋅ ℎ G ⋅ ih F - ℎ S ⁢ R ⋅ ℎ G = F ⋅ ih F + S ‾ ⁢ − R ⁢ F ⋅ ih G + S ⁢ − R ⁢ G ⋅ ih F + R 2 ⁢ G ⋅ ih G
10 1 2 3 4 5 6 7 normlem3 ⊢ A ⁢ R 2 + B ⁢ R + C = F ⋅ ih F + S ‾ ⁢ − R ⁢ F ⋅ ih G + S ⁢ − R ⁢ G ⋅ ih F + R 2 ⁢ G ⋅ ih G
11 9 10 eqtr4i ⊢ F - ℎ S ⁢ R ⋅ ℎ G ⋅ ih F - ℎ S ⁢ R ⋅ ℎ G = A ⁢ R 2 + B ⁢ R + C