normlem1

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

	Ref	Expression
Hypotheses	normlem1.1	$⊢ S \in ℂ$
	normlem1.2	$⊢ F \in ℋ$
	normlem1.3	$⊢ G \in ℋ$
	normlem1.4	$⊢ R \in ℝ$
	normlem1.5	$⊢ \|S\| = 1$
Assertion	normlem1	$⊢ (F -_{ℎ} (S R \cdot_{ℎ} G)) \cdot_{ih} (F -_{ℎ} (S R \cdot_{ℎ} G)) = (F \cdot_{ih} F) + \overline{S} (- R) (F \cdot_{ih} G) + S (- R) (G \cdot_{ih} F) + R^{2} (G \cdot_{ih} G)$

Proof

Step	Hyp	Ref	Expression
1		normlem1.1	$⊢ S \in ℂ$
2		normlem1.2	$⊢ F \in ℋ$
3		normlem1.3	$⊢ G \in ℋ$
4		normlem1.4	$⊢ R \in ℝ$
5		normlem1.5	$⊢ \|S\| = 1$
6	4	recni	$⊢ R \in ℂ$
7	1 6	mulcli	$⊢ S R \in ℂ$
8	7 2 3	normlem0	$⊢ (F -_{ℎ} (S R \cdot_{ℎ} G)) \cdot_{ih} (F -_{ℎ} (S R \cdot_{ℎ} G)) = (F \cdot_{ih} F) + (- \overline{S R}) (F \cdot_{ih} G) + (- S R) (G \cdot_{ih} F) + S R \overline{S R} (G \cdot_{ih} G)$
9	1 6	cjmuli	$⊢ \overline{S R} = \overline{S} \overline{R}$
10	6	cjrebi	$⊢ R \in ℝ \leftrightarrow \overline{R} = R$
11	4 10	mpbi	$⊢ \overline{R} = R$
12	11	oveq2i	$⊢ \overline{S} \overline{R} = \overline{S} R$
13	9 12	eqtri	$⊢ \overline{S R} = \overline{S} R$
14	13	negeqi	$⊢ - \overline{S R} = - \overline{S} R$
15	1	cjcli	$⊢ \overline{S} \in ℂ$
16	15 6	mulneg2i	$⊢ \overline{S} (- R) = - \overline{S} R$
17	14 16	eqtr4i	$⊢ - \overline{S R} = \overline{S} (- R)$
18	17	oveq1i	$⊢ (- \overline{S R}) (F \cdot_{ih} G) = \overline{S} (- R) (F \cdot_{ih} G)$
19	18	oveq2i	$⊢ (F \cdot_{ih} F) + (- \overline{S R}) (F \cdot_{ih} G) = (F \cdot_{ih} F) + \overline{S} (- R) (F \cdot_{ih} G)$
20	1 6	mulneg2i	$⊢ S (- R) = - S R$
21	20	eqcomi	$⊢ - S R = S (- R)$
22	21	oveq1i	$⊢ (- S R) (G \cdot_{ih} F) = S (- R) (G \cdot_{ih} F)$
23	9	oveq2i	$⊢ S R \overline{S R} = S R \overline{S} \overline{R}$
24	6	cjcli	$⊢ \overline{R} \in ℂ$
25	1 6 15 24	mul4i	$⊢ S R \overline{S} \overline{R} = S \overline{S} R \overline{R}$
26	5	oveq1i	$⊢ {\|S\|}^{2} = 1^{2}$
27	1	absvalsqi	$⊢ {\|S\|}^{2} = S \overline{S}$
28		sq1	$⊢ 1^{2} = 1$
29	26 27 28	3eqtr3i	$⊢ S \overline{S} = 1$
30	11	oveq2i	$⊢ R \overline{R} = R R$
31	29 30	oveq12i	$⊢ S \overline{S} R \overline{R} = 1 R R$
32	6 6	mulcli	$⊢ R R \in ℂ$
33	32	mullidi	$⊢ 1 R R = R R$
34	31 33	eqtri	$⊢ S \overline{S} R \overline{R} = R R$
35	25 34	eqtri	$⊢ S R \overline{S} \overline{R} = R R$
36	23 35	eqtri	$⊢ S R \overline{S R} = R R$
37	6	sqvali	$⊢ R^{2} = R R$
38	36 37	eqtr4i	$⊢ S R \overline{S R} = R^{2}$
39	38	oveq1i	$⊢ S R \overline{S R} (G \cdot_{ih} G) = R^{2} (G \cdot_{ih} G)$
40	22 39	oveq12i	$⊢ (- S R) (G \cdot_{ih} F) + S R \overline{S R} (G \cdot_{ih} G) = S (- R) (G \cdot_{ih} F) + R^{2} (G \cdot_{ih} G)$
41	19 40	oveq12i	$⊢ (F \cdot_{ih} F) + (- \overline{S R}) (F \cdot_{ih} G) + (- S R) (G \cdot_{ih} F) + S R \overline{S R} (G \cdot_{ih} G) = (F \cdot_{ih} F) + \overline{S} (- R) (F \cdot_{ih} G) + S (- R) (G \cdot_{ih} F) + R^{2} (G \cdot_{ih} G)$
42	8 41	eqtri	$⊢ (F -_{ℎ} (S R \cdot_{ℎ} G)) \cdot_{ih} (F -_{ℎ} (S R \cdot_{ℎ} G)) = (F \cdot_{ih} F) + \overline{S} (- R) (F \cdot_{ih} G) + S (- R) (G \cdot_{ih} F) + R^{2} (G \cdot_{ih} G)$

Metamath Proof Explorer

Theorem normlem1

Proof