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

Metamath Proof Explorer

Theorem normlem3

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

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

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 normlem3.7 ⊢ 𝑅 ∈ ℝ
8 3 3 hicli ⊢ ( 𝐺 ·ih 𝐺 ) ∈ ℂ
9 5 8 eqeltri ⊢ 𝐴 ∈ ℂ
10 7 recni ⊢ 𝑅 ∈ ℂ
11 10 sqcli ⊢ ( 𝑅 ↑ 2 ) ∈ ℂ
12 9 11 mulcli ⊢ ( 𝐴 · ( 𝑅 ↑ 2 ) ) ∈ ℂ
13 1 2 3 4 normlem2 ⊢ 𝐵 ∈ ℝ
14 13 recni ⊢ 𝐵 ∈ ℂ
15 14 10 mulcli ⊢ ( 𝐵 · 𝑅 ) ∈ ℂ
16 12 15 addcomi ⊢ ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) = ( ( 𝐵 · 𝑅 ) + ( 𝐴 · ( 𝑅 ↑ 2 ) ) )
17 1 cjcli ⊢ ( ∗ ‘ 𝑆 ) ∈ ℂ
18 2 3 hicli ⊢ ( 𝐹 ·ih 𝐺 ) ∈ ℂ
19 17 18 mulcli ⊢ ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) ∈ ℂ
20 3 2 hicli ⊢ ( 𝐺 ·ih 𝐹 ) ∈ ℂ
21 1 20 mulcli ⊢ ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ∈ ℂ
22 19 21 addcli ⊢ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ∈ ℂ
23 22 10 mulneg1i ⊢ ( - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) · 𝑅 ) = - ( ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) · 𝑅 )
24 4 oveq1i ⊢ ( 𝐵 · 𝑅 ) = ( - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) · 𝑅 )
25 22 10 mulneg2i ⊢ ( ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) · - 𝑅 ) = - ( ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) · 𝑅 )
26 23 24 25 3eqtr4i ⊢ ( 𝐵 · 𝑅 ) = ( ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) · - 𝑅 )
27 10 negcli ⊢ - 𝑅 ∈ ℂ
28 19 21 27 adddiri ⊢ ( ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) · - 𝑅 ) = ( ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) · - 𝑅 ) + ( ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) · - 𝑅 ) )
29 17 18 27 mul32i ⊢ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) · - 𝑅 ) = ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) )
30 1 20 27 mul32i ⊢ ( ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) · - 𝑅 ) = ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) )
31 29 30 oveq12i ⊢ ( ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) · - 𝑅 ) + ( ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) · - 𝑅 ) ) = ( ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) + ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) )
32 26 28 31 3eqtri ⊢ ( 𝐵 · 𝑅 ) = ( ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) + ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) )
33 5 oveq2i ⊢ ( ( 𝑅 ↑ 2 ) · 𝐴 ) = ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) )
34 11 9 33 mulcomli ⊢ ( 𝐴 · ( 𝑅 ↑ 2 ) ) = ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) )
35 32 34 oveq12i ⊢ ( ( 𝐵 · 𝑅 ) + ( 𝐴 · ( 𝑅 ↑ 2 ) ) ) = ( ( ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) + ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) )
36 17 27 mulcli ⊢ ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) ∈ ℂ
37 36 18 mulcli ⊢ ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) ∈ ℂ
38 1 27 mulcli ⊢ ( 𝑆 · - 𝑅 ) ∈ ℂ
39 38 20 mulcli ⊢ ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) ∈ ℂ
40 11 8 mulcli ⊢ ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ∈ ℂ
41 37 39 40 addassi ⊢ ( ( ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) + ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) = ( ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) + ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) )
42 16 35 41 3eqtri ⊢ ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) = ( ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) + ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) )
43 6 42 oveq12i ⊢ ( 𝐶 + ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) ) = ( ( 𝐹 ·ih 𝐹 ) + ( ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) + ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) ) )
44 12 15 addcli ⊢ ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) ∈ ℂ
45 2 2 hicli ⊢ ( 𝐹 ·ih 𝐹 ) ∈ ℂ
46 6 45 eqeltri ⊢ 𝐶 ∈ ℂ
47 44 46 addcomi ⊢ ( ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) + 𝐶 ) = ( 𝐶 + ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) )
48 39 40 addcli ⊢ ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) ∈ ℂ
49 45 37 48 addassi ⊢ ( ( ( 𝐹 ·ih 𝐹 ) + ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) ) + ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) ) = ( ( 𝐹 ·ih 𝐹 ) + ( ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) + ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) ) )
50 43 47 49 3eqtr4i ⊢ ( ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) + 𝐶 ) = ( ( ( 𝐹 ·ih 𝐹 ) + ( ( ( ∗ ‘ 𝑆 ) · - 𝑅 ) · ( 𝐹 ·ih 𝐺 ) ) ) + ( ( ( 𝑆 · - 𝑅 ) · ( 𝐺 ·ih 𝐹 ) ) + ( ( 𝑅 ↑ 2 ) · ( 𝐺 ·ih 𝐺 ) ) ) )