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 𝐺 ) ) ) )