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

Metamath Proof Explorer

Theorem normlem2

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

Ref Expression
Hypotheses normlem1.1 ⊢ 𝑆 ∈ ℂ
normlem1.2 ⊢ 𝐹 ∈ ℋ
normlem1.3 ⊢ 𝐺 ∈ ℋ
normlem2.4 ⊢ 𝐵 = - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) )
Assertion normlem2 𝐵 ∈ ℝ

Proof

Step Hyp Ref Expression
1 normlem1.1 ⊢ 𝑆 ∈ ℂ
2 normlem1.2 ⊢ 𝐹 ∈ ℋ
3 normlem1.3 ⊢ 𝐺 ∈ ℋ
4 normlem2.4 ⊢ 𝐵 = - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) )
5 1 cjcli ⊢ ( ∗ ‘ 𝑆 ) ∈ ℂ
6 2 3 hicli ⊢ ( 𝐹 ·ih 𝐺 ) ∈ ℂ
7 5 6 mulcli ⊢ ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) ∈ ℂ
8 3 2 hicli ⊢ ( 𝐺 ·ih 𝐹 ) ∈ ℂ
9 1 8 mulcli ⊢ ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ∈ ℂ
10 7 9 cjaddi ⊢ ( ∗ ‘ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ) = ( ( ∗ ‘ ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) ) + ( ∗ ‘ ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) )
11 1 cjcji ⊢ ( ∗ ‘ ( ∗ ‘ 𝑆 ) ) = 𝑆
12 11 eqcomi ⊢ 𝑆 = ( ∗ ‘ ( ∗ ‘ 𝑆 ) )
13 3 2 his1i ⊢ ( 𝐺 ·ih 𝐹 ) = ( ∗ ‘ ( 𝐹 ·ih 𝐺 ) )
14 12 13 oveq12i ⊢ ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝑆 ) ) · ( ∗ ‘ ( 𝐹 ·ih 𝐺 ) ) )
15 5 6 cjmuli ⊢ ( ∗ ‘ ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝑆 ) ) · ( ∗ ‘ ( 𝐹 ·ih 𝐺 ) ) )
16 14 15 eqtr4i ⊢ ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) = ( ∗ ‘ ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) )
17 2 3 his1i ⊢ ( 𝐹 ·ih 𝐺 ) = ( ∗ ‘ ( 𝐺 ·ih 𝐹 ) )
18 17 oveq2i ⊢ ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) = ( ( ∗ ‘ 𝑆 ) · ( ∗ ‘ ( 𝐺 ·ih 𝐹 ) ) )
19 1 8 cjmuli ⊢ ( ∗ ‘ ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) = ( ( ∗ ‘ 𝑆 ) · ( ∗ ‘ ( 𝐺 ·ih 𝐹 ) ) )
20 18 19 eqtr4i ⊢ ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) = ( ∗ ‘ ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) )
21 16 20 oveq12i ⊢ ( ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) + ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) ) = ( ( ∗ ‘ ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) ) + ( ∗ ‘ ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) )
22 10 21 eqtr4i ⊢ ( ∗ ‘ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ) = ( ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) + ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) )
23 7 9 addcomi ⊢ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) = ( ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) + ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) )
24 22 23 eqtr4i ⊢ ( ∗ ‘ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ) = ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) )
25 7 9 addcli ⊢ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ∈ ℂ
26 25 cjrebi ⊢ ( ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ∈ ℝ ↔ ( ∗ ‘ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ) = ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) )
27 24 26 mpbir ⊢ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ∈ ℝ
28 27 renegcli ⊢ - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ∈ ℝ
29 4 28 eqeltri ⊢ 𝐵 ∈ ℝ