cphipval

Description: Value of the inner product expressed by a sum of terms with the norm defined by the inner product. Equation 6.45 of Ponnusamy p. 361. (Contributed by NM, 31-Jan-2007) (Revised by AV, 18-Oct-2021)

	Ref	Expression
Hypotheses	cphipfval.x	$⊢ X = {Base}_{W}$
	cphipfval.p	$⊢ \underset{˙}{+} = +_{W}$
	cphipfval.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	cphipfval.n	$⊢ N = norm (W)$
	cphipfval.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	cphipval.f	$⊢ F = Scalar (W)$
	cphipval.k	$⊢ K = {Base}_{F}$
Assertion	cphipval	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{,} B = \frac{\sum_{k = 1}^{4} i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2}}{4}$

Proof

Step	Hyp	Ref	Expression
1		cphipfval.x	$⊢ X = {Base}_{W}$
2		cphipfval.p	$⊢ \underset{˙}{+} = +_{W}$
3		cphipfval.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		cphipfval.n	$⊢ N = norm (W)$
5		cphipfval.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
6		cphipval.f	$⊢ F = Scalar (W)$
7		cphipval.k	$⊢ K = {Base}_{F}$
8		eqid	$⊢ -_{W} = -_{W}$
9	1 2 3 4 5 8 6 7	cphipval2	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{,} B = \frac{{N (A \underset{˙}{+} B)}^{2} - {N (A -_{W} B)}^{2} + i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2})}{4}$
10		ax-icn	$⊢ i \in ℂ$
11	10	a1i	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i \in ℂ$
12		simp1l	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to W \in CPreHil$
13		cphngp	$⊢ W \in CPreHil \to W \in NrmGrp$
14		ngpgrp	$⊢ W \in NrmGrp \to W \in Grp$
15	13 14	syl	$⊢ W \in CPreHil \to W \in Grp$
16	15	adantr	$⊢ (W \in CPreHil \land i \in K) \to W \in Grp$
17	16	3ad2ant1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to W \in Grp$
18		simp2	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \in X$
19		cphlmod	$⊢ W \in CPreHil \to W \in LMod$
20	19	3anim1i	$⊢ (W \in CPreHil \land i \in K \land B \in X) \to (W \in LMod \land i \in K \land B \in X)$
21	20	3expa	$⊢ ((W \in CPreHil \land i \in K) \land B \in X) \to (W \in LMod \land i \in K \land B \in X)$
22	1 6 3 7	lmodvscl	$⊢ (W \in LMod \land i \in K \land B \in X) \to i \underset{˙}{\cdot} B \in X$
23	21 22	syl	$⊢ ((W \in CPreHil \land i \in K) \land B \in X) \to i \underset{˙}{\cdot} B \in X$
24	23	3adant2	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i \underset{˙}{\cdot} B \in X$
25	1 2	grpcl	$⊢ (W \in Grp \land A \in X \land i \underset{˙}{\cdot} B \in X) \to A \underset{˙}{+} (i \underset{˙}{\cdot} B) \in X$
26	17 18 24 25	syl3anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{+} (i \underset{˙}{\cdot} B) \in X$
27	1 5 4	nmsq	$⊢ (W \in CPreHil \land A \underset{˙}{+} (i \underset{˙}{\cdot} B) \in X) \to {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} = (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (i \underset{˙}{\cdot} B))$
28	12 26 27	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} = (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (i \underset{˙}{\cdot} B))$
29	1 5	reipcl	$⊢ (W \in CPreHil \land A \underset{˙}{+} (i \underset{˙}{\cdot} B) \in X) \to (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \in ℝ$
30	12 26 29	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \in ℝ$
31	30	recnd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \in ℂ$
32	28 31	eqeltrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} \in ℂ$
33	11 32	mulcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} \in ℂ$
34	19	adantr	$⊢ (W \in CPreHil \land i \in K) \to W \in LMod$
35	34	3ad2ant1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to W \in LMod$
36		cphclm	$⊢ W \in CPreHil \to W \in CMod$
37	6 7	clmneg1	$⊢ W \in CMod \to - 1 \in K$
38	36 37	syl	$⊢ W \in CPreHil \to - 1 \in K$
39	38	adantr	$⊢ (W \in CPreHil \land i \in K) \to - 1 \in K$
40	39	3ad2ant1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to - 1 \in K$
41		simp3	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to B \in X$
42	1 6 3 7	lmodvscl	$⊢ (W \in LMod \land - 1 \in K \land B \in X) \to -1 \underset{˙}{\cdot} B \in X$
43	35 40 41 42	syl3anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to -1 \underset{˙}{\cdot} B \in X$
44	1 2	grpcl	$⊢ (W \in Grp \land A \in X \land -1 \underset{˙}{\cdot} B \in X) \to A \underset{˙}{+} (-1 \underset{˙}{\cdot} B) \in X$
45	17 18 43 44	syl3anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{+} (-1 \underset{˙}{\cdot} B) \in X$
46	1 5 4	nmsq	$⊢ (W \in CPreHil \land A \underset{˙}{+} (-1 \underset{˙}{\cdot} B) \in X) \to {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} = (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))$
47	12 45 46	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} = (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))$
48	1 5	reipcl	$⊢ (W \in CPreHil \land A \underset{˙}{+} (-1 \underset{˙}{\cdot} B) \in X) \to (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) \in ℝ$
49	12 45 48	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) \in ℝ$
50	47 49	eqeltrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} \in ℝ$
51	50	recnd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} \in ℂ$
52		addneg1mul	$⊢ (i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} \in ℂ \land {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} \in ℂ) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2}$
53	33 51 52	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2}$
54	36	adantr	$⊢ (W \in CPreHil \land i \in K) \to W \in CMod$
55	1 2 8 6 3	clmvsubval	$⊢ (W \in CMod \land A \in X \land B \in X) \to A -_{W} B = A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)$
56	55	eqcomd	$⊢ (W \in CMod \land A \in X \land B \in X) \to A \underset{˙}{+} (-1 \underset{˙}{\cdot} B) = A -_{W} B$
57	54 56	syl3an1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{+} (-1 \underset{˙}{\cdot} B) = A -_{W} B$
58	57	fveq2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) = N (A -_{W} B)$
59	58	oveq1d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} = {N (A -_{W} B)}^{2}$
60	59	oveq2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2}$
61	53 60	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2}$
62		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
63	54	3ad2ant1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to W \in CMod$
64		simp1r	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i \in K$
65	1 6 3 62 7 63 41 64	clmvsneg	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {inv}_{g} (W) (i \underset{˙}{\cdot} B) = (- i) \underset{˙}{\cdot} B$
66	65	eqcomd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (- i) \underset{˙}{\cdot} B = {inv}_{g} (W) (i \underset{˙}{\cdot} B)$
67	66	oveq2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B) = A \underset{˙}{+} {inv}_{g} (W) (i \underset{˙}{\cdot} B)$
68	1 2 62 8	grpsubval	$⊢ (A \in X \land i \underset{˙}{\cdot} B \in X) \to A -_{W} (i \underset{˙}{\cdot} B) = A \underset{˙}{+} {inv}_{g} (W) (i \underset{˙}{\cdot} B)$
69	18 24 68	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A -_{W} (i \underset{˙}{\cdot} B) = A \underset{˙}{+} {inv}_{g} (W) (i \underset{˙}{\cdot} B)$
70	67 69	eqtr4d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B) = A -_{W} (i \underset{˙}{\cdot} B)$
71	70	fveq2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B)) = N (A -_{W} (i \underset{˙}{\cdot} B))$
72	71	oveq1d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2} = {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}$
73	72	oveq2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (- i) {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2} = (- i) {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}$
74	61 73	oveq12d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} + (- i) {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2} + (- i) {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}$
75	54	anim1i	$⊢ ((W \in CPreHil \land i \in K) \land B \in X) \to (W \in CMod \land B \in X)$
76	75	3adant2	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (W \in CMod \land B \in X)$
77	1 3	clmvs1	$⊢ (W \in CMod \land B \in X) \to 1 \underset{˙}{\cdot} B = B$
78	76 77	syl	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 1 \underset{˙}{\cdot} B = B$
79	78	oveq2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{+} (1 \underset{˙}{\cdot} B) = A \underset{˙}{+} B$
80	79	fveq2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to N (A \underset{˙}{+} (1 \underset{˙}{\cdot} B)) = N (A \underset{˙}{+} B)$
81	80	oveq1d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} (1 \underset{˙}{\cdot} B))}^{2} = {N (A \underset{˙}{+} B)}^{2}$
82	81	oveq2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 1 {N (A \underset{˙}{+} (1 \underset{˙}{\cdot} B))}^{2} = 1 {N (A \underset{˙}{+} B)}^{2}$
83	1 2	grpcl	$⊢ (W \in Grp \land A \in X \land B \in X) \to A \underset{˙}{+} B \in X$
84	16 83	syl3an1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{+} B \in X$
85	1 5 4	nmsq	$⊢ (W \in CPreHil \land A \underset{˙}{+} B \in X) \to {N (A \underset{˙}{+} B)}^{2} = (A \underset{˙}{+} B) \underset{˙}{,} (A \underset{˙}{+} B)$
86	12 84 85	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} = (A \underset{˙}{+} B) \underset{˙}{,} (A \underset{˙}{+} B)$
87	1 5	reipcl	$⊢ (W \in CPreHil \land A \underset{˙}{+} B \in X) \to (A \underset{˙}{+} B) \underset{˙}{,} (A \underset{˙}{+} B) \in ℝ$
88	12 84 87	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{+} B) \underset{˙}{,} (A \underset{˙}{+} B) \in ℝ$
89	86 88	eqeltrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} \in ℝ$
90	89	recnd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} \in ℂ$
91	90	mulid2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 1 {N (A \underset{˙}{+} B)}^{2} = {N (A \underset{˙}{+} B)}^{2}$
92	82 91	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 1 {N (A \underset{˙}{+} (1 \underset{˙}{\cdot} B))}^{2} = {N (A \underset{˙}{+} B)}^{2}$
93	74 92	oveq12d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2}) + (- i) {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2} + 1 {N (A \underset{˙}{+} (1 \underset{˙}{\cdot} B))}^{2} = (i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2}) + (- i) {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} + {N (A \underset{˙}{+} B)}^{2}$
94		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
95		df-4	$⊢ 4 = 3 + 1$
96		oveq2	$⊢ k = 4 \to i^{k} = i^{4}$
97		i4	$⊢ i^{4} = 1$
98	96 97	eqtrdi	$⊢ k = 4 \to i^{k} = 1$
99	98	oveq1d	$⊢ k = 4 \to i^{k} \underset{˙}{\cdot} B = 1 \underset{˙}{\cdot} B$
100	99	oveq2d	$⊢ k = 4 \to A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B) = A \underset{˙}{+} (1 \underset{˙}{\cdot} B)$
101	100	fveq2d	$⊢ k = 4 \to N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) = N (A \underset{˙}{+} (1 \underset{˙}{\cdot} B))$
102	101	oveq1d	$⊢ k = 4 \to {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = {N (A \underset{˙}{+} (1 \underset{˙}{\cdot} B))}^{2}$
103	98 102	oveq12d	$⊢ k = 4 \to i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = 1 {N (A \underset{˙}{+} (1 \underset{˙}{\cdot} B))}^{2}$
104	10	a1i	$⊢ k \in ℕ \to i \in ℂ$
105		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
106	104 105	expcld	$⊢ k \in ℕ \to i^{k} \in ℂ$
107	106	adantl	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to i^{k} \in ℂ$
108	12	adantr	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to W \in CPreHil$
109	17	adantr	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to W \in Grp$
110	18	adantr	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to A \in X$
111	35	adantr	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to W \in LMod$
112	36	anim1i	$⊢ (W \in CPreHil \land i \in K) \to (W \in CMod \land i \in K)$
113	112	3ad2ant1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (W \in CMod \land i \in K)$
114	6 7	cmodscexp	$⊢ ((W \in CMod \land i \in K) \land k \in ℕ) \to i^{k} \in K$
115	113 114	sylan	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to i^{k} \in K$
116	41	adantr	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to B \in X$
117	1 6 3 7	lmodvscl	$⊢ (W \in LMod \land i^{k} \in K \land B \in X) \to i^{k} \underset{˙}{\cdot} B \in X$
118	111 115 116 117	syl3anc	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to i^{k} \underset{˙}{\cdot} B \in X$
119	1 2	grpcl	$⊢ (W \in Grp \land A \in X \land i^{k} \underset{˙}{\cdot} B \in X) \to A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B) \in X$
120	109 110 118 119	syl3anc	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B) \in X$
121	1 5 4	nmsq	$⊢ (W \in CPreHil \land A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B) \in X) \to {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))$
122	108 120 121	syl2anc	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))$
123	1 5	reipcl	$⊢ (W \in CPreHil \land A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B) \in X) \to (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) \in ℝ$
124	108 120 123	syl2anc	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) \in ℝ$
125	124	recnd	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) \in ℂ$
126	122 125	eqeltrd	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} \in ℂ$
127	107 126	mulcld	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} \in ℂ$
128		df-3	$⊢ 3 = 2 + 1$
129		oveq2	$⊢ k = 3 \to i^{k} = i^{3}$
130		i3	$⊢ i^{3} = - i$
131	129 130	eqtrdi	$⊢ k = 3 \to i^{k} = - i$
132	131	oveq1d	$⊢ k = 3 \to i^{k} \underset{˙}{\cdot} B = (- i) \underset{˙}{\cdot} B$
133	132	oveq2d	$⊢ k = 3 \to A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B) = A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B)$
134	133	fveq2d	$⊢ k = 3 \to N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) = N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))$
135	134	oveq1d	$⊢ k = 3 \to {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2}$
136	131 135	oveq12d	$⊢ k = 3 \to i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = (- i) {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2}$
137	10	a1i	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to i \in ℂ$
138	105	adantl	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to k \in ℕ_{0}$
139	137 138	expcld	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to i^{k} \in ℂ$
140	123	recnd	$⊢ (W \in CPreHil \land A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B) \in X) \to (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) \in ℂ$
141	108 120 140	syl2anc	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) \underset{˙}{,} (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) \in ℂ$
142	122 141	eqeltrd	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} \in ℂ$
143	139 142	mulcld	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} \in ℂ$
144		df-2	$⊢ 2 = 1 + 1$
145		oveq2	$⊢ k = 2 \to i^{k} = i^{2}$
146		i2	$⊢ i^{2} = - 1$
147	145 146	eqtrdi	$⊢ k = 2 \to i^{k} = - 1$
148	147	oveq1d	$⊢ k = 2 \to i^{k} \underset{˙}{\cdot} B = -1 \underset{˙}{\cdot} B$
149	148	oveq2d	$⊢ k = 2 \to A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B) = A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)$
150	149	fveq2d	$⊢ k = 2 \to N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) = N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))$
151	150	oveq1d	$⊢ k = 2 \to {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2}$
152	147 151	oveq12d	$⊢ k = 2 \to i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2}$
153	139 126	mulcld	$⊢ (((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \land k \in ℕ) \to i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} \in ℂ$
154		1z	$⊢ 1 \in ℤ$
155		oveq2	$⊢ k = 1 \to i^{k} = i^{1}$
156		exp1	$⊢ i \in ℂ \to i^{1} = i$
157	10 156	ax-mp	$⊢ i^{1} = i$
158	155 157	eqtrdi	$⊢ k = 1 \to i^{k} = i$
159	158	oveq1d	$⊢ k = 1 \to i^{k} \underset{˙}{\cdot} B = i \underset{˙}{\cdot} B$
160	159	oveq2d	$⊢ k = 1 \to A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B) = A \underset{˙}{+} (i \underset{˙}{\cdot} B)$
161	160	fveq2d	$⊢ k = 1 \to N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B)) = N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))$
162	161	oveq1d	$⊢ k = 1 \to {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2}$
163	158 162	oveq12d	$⊢ k = 1 \to i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2}$
164	163	fsum1	$⊢ (1 \in ℤ \land i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} \in ℂ) \to \sum_{k = 1}^{1} i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2}$
165	154 33 164	sylancr	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to \sum_{k = 1}^{1} i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2}$
166		1nn	$⊢ 1 \in ℕ$
167	165 166	jctil	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (1 \in ℕ \land \sum_{k = 1}^{1} i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2})$
168		eqidd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2}$
169	94 144 152 153 167 168	fsump1i	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (2 \in ℕ \land \sum_{k = 1}^{2} i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2})$
170		eqidd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} + (- i) {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} + (- i) {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2}$
171	94 128 136 143 169 170	fsump1i	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (3 \in ℕ \land \sum_{k = 1}^{3} i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2} + (- i) {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2})$
172		eqidd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2}) + (- i) {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2} + 1 {N (A \underset{˙}{+} (1 \underset{˙}{\cdot} B))}^{2} = (i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2}) + (- i) {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2} + 1 {N (A \underset{˙}{+} (1 \underset{˙}{\cdot} B))}^{2}$
173	94 95 103 127 171 172	fsump1i	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (4 \in ℕ \land \sum_{k = 1}^{4} i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = (i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2}) + (- i) {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2} + 1 {N (A \underset{˙}{+} (1 \underset{˙}{\cdot} B))}^{2})$
174	173	simprd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to \sum_{k = 1}^{4} i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2} = (i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} + -1 {N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))}^{2}) + (- i) {N (A \underset{˙}{+} ((- i) \underset{˙}{\cdot} B))}^{2} + 1 {N (A \underset{˙}{+} (1 \underset{˙}{\cdot} B))}^{2}$
175	1 8	grpsubcl	$⊢ (W \in Grp \land A \in X \land B \in X) \to A -_{W} B \in X$
176	16 175	syl3an1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A -_{W} B \in X$
177	1 5 4	nmsq	$⊢ (W \in CPreHil \land A -_{W} B \in X) \to {N (A -_{W} B)}^{2} = (A -_{W} B) \underset{˙}{,} (A -_{W} B)$
178	12 176 177	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A -_{W} B)}^{2} = (A -_{W} B) \underset{˙}{,} (A -_{W} B)$
179	1 5	reipcl	$⊢ (W \in CPreHil \land A -_{W} B \in X) \to (A -_{W} B) \underset{˙}{,} (A -_{W} B) \in ℝ$
180	12 176 179	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A -_{W} B) \underset{˙}{,} (A -_{W} B) \in ℝ$
181	178 180	eqeltrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A -_{W} B)}^{2} \in ℝ$
182	181	recnd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A -_{W} B)}^{2} \in ℂ$
183	90 182	subcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} - {N (A -_{W} B)}^{2} \in ℂ$
184	1 8	grpsubcl	$⊢ (W \in Grp \land A \in X \land i \underset{˙}{\cdot} B \in X) \to A -_{W} (i \underset{˙}{\cdot} B) \in X$
185	17 18 24 184	syl3anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A -_{W} (i \underset{˙}{\cdot} B) \in X$
186	1 5 4	nmsq	$⊢ (W \in CPreHil \land A -_{W} (i \underset{˙}{\cdot} B) \in X) \to {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} = (A -_{W} (i \underset{˙}{\cdot} B)) \underset{˙}{,} (A -_{W} (i \underset{˙}{\cdot} B))$
187	12 185 186	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} = (A -_{W} (i \underset{˙}{\cdot} B)) \underset{˙}{,} (A -_{W} (i \underset{˙}{\cdot} B))$
188	1 5	reipcl	$⊢ (W \in CPreHil \land A -_{W} (i \underset{˙}{\cdot} B) \in X) \to (A -_{W} (i \underset{˙}{\cdot} B)) \underset{˙}{,} (A -_{W} (i \underset{˙}{\cdot} B)) \in ℝ$
189	12 185 188	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A -_{W} (i \underset{˙}{\cdot} B)) \underset{˙}{,} (A -_{W} (i \underset{˙}{\cdot} B)) \in ℝ$
190	187 189	eqeltrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} \in ℝ$
191	190	recnd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} \in ℂ$
192	32 191	subcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} \in ℂ$
193	11 192	mulcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) \in ℂ$
194	183 193	addcomd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} - {N (A -_{W} B)}^{2} + i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) = i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) + {N (A \underset{˙}{+} B)}^{2} - {N (A -_{W} B)}^{2}$
195	193 182 90	subadd23d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) - {N (A -_{W} B)}^{2} + {N (A \underset{˙}{+} B)}^{2} = i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) + {N (A \underset{˙}{+} B)}^{2} - {N (A -_{W} B)}^{2}$
196	11 32 191	subdid	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}$
197	196	oveq1d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) - {N (A -_{W} B)}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2}$
198	11 191	mulcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} \in ℂ$
199	33 198 182	sub32d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2} - i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}$
200	197 199	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) - {N (A -_{W} B)}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2} - i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}$
201	200	oveq1d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) - {N (A -_{W} B)}^{2} + {N (A \underset{˙}{+} B)}^{2} = (i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2}) - i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} + {N (A \underset{˙}{+} B)}^{2}$
202	194 195 201	3eqtr2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} - {N (A -_{W} B)}^{2} + i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) = (i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2}) - i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} + {N (A \underset{˙}{+} B)}^{2}$
203	33 182	subcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2} \in ℂ$
204	203 198	negsubd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2} + (- i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2} - i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}$
205	11 191	mulneg1d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (- i) {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} = - i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}$
206	205	eqcomd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to - i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} = (- i) {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}$
207	206	oveq2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2} + (- i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2} + (- i) {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}$
208	204 207	eqtr3d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2} - i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} = i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2} + (- i) {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}$
209	208	oveq1d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2}) - i {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} + {N (A \underset{˙}{+} B)}^{2} = (i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2}) + (- i) {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} + {N (A \underset{˙}{+} B)}^{2}$
210	202 209	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} - {N (A -_{W} B)}^{2} + i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) = (i {N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} B)}^{2}) + (- i) {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2} + {N (A \underset{˙}{+} B)}^{2}$
211	93 174 210	3eqtr4rd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} - {N (A -_{W} B)}^{2} + i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2}) = \sum_{k = 1}^{4} i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2}$
212	211	oveq1d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to \frac{{N (A \underset{˙}{+} B)}^{2} - {N (A -_{W} B)}^{2} + i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A -_{W} (i \underset{˙}{\cdot} B))}^{2})}{4} = \frac{\sum_{k = 1}^{4} i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2}}{4}$
213	9 212	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{,} B = \frac{\sum_{k = 1}^{4} i^{k} {N (A \underset{˙}{+} (i^{k} \underset{˙}{\cdot} B))}^{2}}{4}$

Metamath Proof Explorer

Theorem cphipval

Proof