cphipval2

Description: Value of the inner product expressed by the norm defined by it. (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)$
	cphipval2.m	$⊢ \underset{˙}{-} = -_{W}$
	cphipval2.f	$⊢ F = Scalar (W)$
	cphipval2.k	$⊢ K = {Base}_{F}$
Assertion	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 \underset{˙}{-} B)}^{2} + i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A \underset{˙}{-} (i \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		cphipval2.m	$⊢ \underset{˙}{-} = -_{W}$
7		cphipval2.f	$⊢ F = Scalar (W)$
8		cphipval2.k	$⊢ K = {Base}_{F}$
9		simpl	$⊢ (W \in CPreHil \land i \in K) \to W \in CPreHil$
10	9	3ad2ant1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to W \in CPreHil$
11		cphngp	$⊢ W \in CPreHil \to W \in NrmGrp$
12	11	adantr	$⊢ (W \in CPreHil \land i \in K) \to W \in NrmGrp$
13		ngpgrp	$⊢ W \in NrmGrp \to W \in Grp$
14	12 13	syl	$⊢ (W \in CPreHil \land i \in K) \to W \in Grp$
15	1 2	grpcl	$⊢ (W \in Grp \land A \in X \land B \in X) \to A \underset{˙}{+} B \in X$
16	14 15	syl3an1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{+} B \in X$
17	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)$
18	10 16 17	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)$
19		simp2	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \in X$
20		simp3	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to B \in X$
21	5 1 2 10 19 20 19 20	cph2di	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{+} B) \underset{˙}{,} (A \underset{˙}{+} B) = (A \underset{˙}{,} A) + (B \underset{˙}{,} B) + (A \underset{˙}{,} B) + (B \underset{˙}{,} A)$
22	18 21	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} = (A \underset{˙}{,} A) + (B \underset{˙}{,} B) + (A \underset{˙}{,} B) + (B \underset{˙}{,} A)$
23	1 6	grpsubcl	$⊢ (W \in Grp \land A \in X \land B \in X) \to A \underset{˙}{-} B \in X$
24	14 23	syl3an1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{-} B \in X$
25	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)$
26	10 24 25	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)$
27	5 1 6 10 19 20 19 20	cph2subdi	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{-} B) \underset{˙}{,} (A \underset{˙}{-} B) = (A \underset{˙}{,} A) + (B \underset{˙}{,} B) - ((A \underset{˙}{,} B) + (B \underset{˙}{,} A))$
28	26 27	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{-} B)}^{2} = (A \underset{˙}{,} A) + (B \underset{˙}{,} B) - ((A \underset{˙}{,} B) + (B \underset{˙}{,} A))$
29	22 28	oveq12d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} - {N (A \underset{˙}{-} B)}^{2} = ((A \underset{˙}{,} A) + (B \underset{˙}{,} B)) + ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) - ((A \underset{˙}{,} A) + (B \underset{˙}{,} B) - ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)))$
30	1 5	reipcl	$⊢ (W \in CPreHil \land A \in X) \to A \underset{˙}{,} A \in ℝ$
31	30	adantlr	$⊢ ((W \in CPreHil \land i \in K) \land A \in X) \to A \underset{˙}{,} A \in ℝ$
32	31	recnd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X) \to A \underset{˙}{,} A \in ℂ$
33	32	3adant3	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{,} A \in ℂ$
34	1 5	reipcl	$⊢ (W \in CPreHil \land B \in X) \to B \underset{˙}{,} B \in ℝ$
35	34	adantlr	$⊢ ((W \in CPreHil \land i \in K) \land B \in X) \to B \underset{˙}{,} B \in ℝ$
36	35	recnd	$⊢ ((W \in CPreHil \land i \in K) \land B \in X) \to B \underset{˙}{,} B \in ℂ$
37	36	3adant2	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to B \underset{˙}{,} B \in ℂ$
38	33 37	addcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{,} A) + (B \underset{˙}{,} B) \in ℂ$
39	1 5	cphipcl	$⊢ (W \in CPreHil \land A \in X \land B \in X) \to A \underset{˙}{,} B \in ℂ$
40	9 39	syl3an1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{,} B \in ℂ$
41	1 5	cphipcl	$⊢ (W \in CPreHil \land B \in X \land A \in X) \to B \underset{˙}{,} A \in ℂ$
42	9 41	syl3an1	$⊢ ((W \in CPreHil \land i \in K) \land B \in X \land A \in X) \to B \underset{˙}{,} A \in ℂ$
43	42	3com23	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to B \underset{˙}{,} A \in ℂ$
44	40 43	addcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{,} B) + (B \underset{˙}{,} A) \in ℂ$
45	38 44 44	pnncand	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to ((A \underset{˙}{,} A) + (B \underset{˙}{,} B)) + ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) - ((A \underset{˙}{,} A) + (B \underset{˙}{,} B) - ((A \underset{˙}{,} B) + (B \underset{˙}{,} A))) = (A \underset{˙}{,} B) + (B \underset{˙}{,} A) + (A \underset{˙}{,} B) + (B \underset{˙}{,} A)$
46	29 45	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} - {N (A \underset{˙}{-} B)}^{2} = (A \underset{˙}{,} B) + (B \underset{˙}{,} A) + (A \underset{˙}{,} B) + (B \underset{˙}{,} A)$
47	14	3ad2ant1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to W \in Grp$
48		cphlmod	$⊢ W \in CPreHil \to W \in LMod$
49	48	adantr	$⊢ (W \in CPreHil \land i \in K) \to W \in LMod$
50	49	adantr	$⊢ ((W \in CPreHil \land i \in K) \land B \in X) \to W \in LMod$
51		simplr	$⊢ ((W \in CPreHil \land i \in K) \land B \in X) \to i \in K$
52		simpr	$⊢ ((W \in CPreHil \land i \in K) \land B \in X) \to B \in X$
53	1 7 3 8	lmodvscl	$⊢ (W \in LMod \land i \in K \land B \in X) \to i \underset{˙}{\cdot} B \in X$
54	50 51 52 53	syl3anc	$⊢ ((W \in CPreHil \land i \in K) \land B \in X) \to i \underset{˙}{\cdot} B \in X$
55	54	3adant2	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i \underset{˙}{\cdot} B \in X$
56	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$
57	47 19 55 56	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$
58	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))$
59	10 57 58	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))$
60	5 1 2 10 19 55 19 55	cph2di	$⊢ ((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)) = (A \underset{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B)) + (A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A)$
61	59 60	eqtrd	$⊢ ((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{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B)) + (A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A)$
62	1 6	grpsubcl	$⊢ (W \in Grp \land A \in X \land i \underset{˙}{\cdot} B \in X) \to A \underset{˙}{-} (i \underset{˙}{\cdot} B) \in X$
63	47 19 55 62	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$
64	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))$
65	10 63 64	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))$
66	5 1 6 10 19 55 19 55	cph2subdi	$⊢ ((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)) = (A \underset{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B)) - ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A))$
67	65 66	eqtrd	$⊢ ((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{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B)) - ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A))$
68	61 67	oveq12d	$⊢ ((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 \underset{˙}{-} (i \underset{˙}{\cdot} B))}^{2} = ((A \underset{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B))) + ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A)) - ((A \underset{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B)) - ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A)))$
69	68	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{˙}{-} (i \underset{˙}{\cdot} B))}^{2}) = i (((A \underset{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B))) + ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A)) - ((A \underset{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B)) - ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A))))$
70	1 5	cphipcl	$⊢ (W \in CPreHil \land i \underset{˙}{\cdot} B \in X \land i \underset{˙}{\cdot} B \in X) \to (i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B) \in ℂ$
71	10 55 55 70	syl3anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B) \in ℂ$
72	33 71	addcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B)) \in ℂ$
73	1 5	cphipcl	$⊢ (W \in CPreHil \land A \in X \land i \underset{˙}{\cdot} B \in X) \to A \underset{˙}{,} (i \underset{˙}{\cdot} B) \in ℂ$
74	10 19 55 73	syl3anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{,} (i \underset{˙}{\cdot} B) \in ℂ$
75	1 5	cphipcl	$⊢ (W \in CPreHil \land i \underset{˙}{\cdot} B \in X \land A \in X) \to (i \underset{˙}{\cdot} B) \underset{˙}{,} A \in ℂ$
76	10 55 19 75	syl3anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (i \underset{˙}{\cdot} B) \underset{˙}{,} A \in ℂ$
77	74 76	addcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A) \in ℂ$
78	72 77 77	pnncand	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to ((A \underset{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B))) + ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A)) - ((A \underset{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B)) - ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A))) = (A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A) + (A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A)$
79	78	oveq2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i (((A \underset{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B))) + ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A)) - ((A \underset{˙}{,} A) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} (i \underset{˙}{\cdot} B)) - ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A)))) = i ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A) + (A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A))$
80	1 3 5 7 8	cphassir	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{,} (i \underset{˙}{\cdot} B) = (- i) (A \underset{˙}{,} B)$
81	1 3 5 7 8	cphassi	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (i \underset{˙}{\cdot} B) \underset{˙}{,} A = i (B \underset{˙}{,} A)$
82	80 81	oveq12d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A) = (- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A)$
83	82 82	oveq12d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A) + (A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A) = (- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A) + (- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A)$
84	83	oveq2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A) + (A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A)) = i ((- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A) + (- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A))$
85		ax-icn	$⊢ i \in ℂ$
86	85	a1i	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i \in ℂ$
87		negicn	$⊢ - i \in ℂ$
88	87	a1i	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to - i \in ℂ$
89	88 40	mulcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (- i) (A \underset{˙}{,} B) \in ℂ$
90	86 43	mulcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i (B \underset{˙}{,} A) \in ℂ$
91	89 90	addcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A) \in ℂ$
92	86 91 91	adddid	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ((- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A) + (- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A)) = i ((- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A)) + i ((- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A))$
93	86 89 90	adddid	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ((- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A)) = i (- i) (A \underset{˙}{,} B) + i i (B \underset{˙}{,} A)$
94	86 88 40	mulassd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i (- i) (A \underset{˙}{,} B) = i (- i) (A \underset{˙}{,} B)$
95	85 85	mulneg2i	$⊢ i (- i) = - i i$
96		ixi	$⊢ i i = - 1$
97	96	negeqi	$⊢ - i i = - -1$
98		negneg1e1	$⊢ - -1 = 1$
99	95 97 98	3eqtri	$⊢ i (- i) = 1$
100	99	oveq1i	$⊢ i (- i) (A \underset{˙}{,} B) = 1 (A \underset{˙}{,} B)$
101	94 100	eqtr3di	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i (- i) (A \underset{˙}{,} B) = 1 (A \underset{˙}{,} B)$
102	86 86 43	mulassd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i i (B \underset{˙}{,} A) = i i (B \underset{˙}{,} A)$
103	96	oveq1i	$⊢ i i (B \underset{˙}{,} A) = -1 (B \underset{˙}{,} A)$
104	102 103	eqtr3di	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i i (B \underset{˙}{,} A) = -1 (B \underset{˙}{,} A)$
105	101 104	oveq12d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i (- i) (A \underset{˙}{,} B) + i i (B \underset{˙}{,} A) = 1 (A \underset{˙}{,} B) + -1 (B \underset{˙}{,} A)$
106	93 105	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ((- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A)) = 1 (A \underset{˙}{,} B) + -1 (B \underset{˙}{,} A)$
107	106 106	oveq12d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ((- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A)) + i ((- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A)) = 1 (A \underset{˙}{,} B) + -1 (B \underset{˙}{,} A) + 1 (A \underset{˙}{,} B) + -1 (B \underset{˙}{,} A)$
108	40	mullidd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 1 (A \underset{˙}{,} B) = A \underset{˙}{,} B$
109	108	oveq1d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 1 (A \underset{˙}{,} B) + -1 (B \underset{˙}{,} A) = (A \underset{˙}{,} B) + -1 (B \underset{˙}{,} A)$
110		addneg1mul	$⊢ (A \underset{˙}{,} B \in ℂ \land B \underset{˙}{,} A \in ℂ) \to (A \underset{˙}{,} B) + -1 (B \underset{˙}{,} A) = (A \underset{˙}{,} B) - (B \underset{˙}{,} A)$
111	40 43 110	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{,} B) + -1 (B \underset{˙}{,} A) = (A \underset{˙}{,} B) - (B \underset{˙}{,} A)$
112	109 111	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 1 (A \underset{˙}{,} B) + -1 (B \underset{˙}{,} A) = (A \underset{˙}{,} B) - (B \underset{˙}{,} A)$
113	112 112	oveq12d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 1 (A \underset{˙}{,} B) + -1 (B \underset{˙}{,} A) + 1 (A \underset{˙}{,} B) + -1 (B \underset{˙}{,} A) = ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) + (A \underset{˙}{,} B) - (B \underset{˙}{,} A)$
114	107 113	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ((- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A)) + i ((- i) (A \underset{˙}{,} B) + i (B \underset{˙}{,} A)) = ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) + (A \underset{˙}{,} B) - (B \underset{˙}{,} A)$
115	84 92 114	3eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i ((A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A) + (A \underset{˙}{,} (i \underset{˙}{\cdot} B)) + ((i \underset{˙}{\cdot} B) \underset{˙}{,} A)) = ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) + (A \underset{˙}{,} B) - (B \underset{˙}{,} A)$
116	69 79 115	3eqtrd	$⊢ ((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{˙}{-} (i \underset{˙}{\cdot} B))}^{2}) = ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) + (A \underset{˙}{,} B) - (B \underset{˙}{,} A)$
117	46 116	oveq12d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} - {N (A \underset{˙}{-} B)}^{2} + i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A \underset{˙}{-} (i \underset{˙}{\cdot} B))}^{2}) = ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A))$
118	117	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 \underset{˙}{-} B)}^{2} + i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A \underset{˙}{-} (i \underset{˙}{\cdot} B))}^{2})}{4} = \frac{((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A))}{4}$
119	40 43	subcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{,} B) - (B \underset{˙}{,} A) \in ℂ$
120	44 44 119 119	add4d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) = ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A))$
121	40 43 40	ppncand	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{,} B) + (B \underset{˙}{,} A) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) = (A \underset{˙}{,} B) + (A \underset{˙}{,} B)$
122	121 121	oveq12d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) = (A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B)$
123	120 122	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) = (A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B)$
124	123	oveq1d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to \frac{((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) + (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A)) + ((A \underset{˙}{,} B) - (B \underset{˙}{,} A))}{4} = \frac{(A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B)}{4}$
125	40	2timesd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 2 (A \underset{˙}{,} B) = (A \underset{˙}{,} B) + (A \underset{˙}{,} B)$
126	125	eqcomd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{,} B) + (A \underset{˙}{,} B) = 2 (A \underset{˙}{,} B)$
127	126 126	oveq12d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B) = 2 (A \underset{˙}{,} B) + 2 (A \underset{˙}{,} B)$
128		2cnd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 2 \in ℂ$
129	128 128 40	adddird	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (2 + 2) (A \underset{˙}{,} B) = 2 (A \underset{˙}{,} B) + 2 (A \underset{˙}{,} B)$
130		2p2e4	$⊢ 2 + 2 = 4$
131	130	a1i	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 2 + 2 = 4$
132	131	oveq1d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (2 + 2) (A \underset{˙}{,} B) = 4 (A \underset{˙}{,} B)$
133	127 129 132	3eqtr2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to (A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B) = 4 (A \underset{˙}{,} B)$
134	133	oveq1d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to \frac{(A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B)}{4} = \frac{4 (A \underset{˙}{,} B)}{4}$
135		4cn	$⊢ 4 \in ℂ$
136	135	a1i	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 4 \in ℂ$
137		4ne0	$⊢ 4 \neq 0$
138	137	a1i	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 4 \neq 0$
139	40 136 138	divcan3d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to \frac{4 (A \underset{˙}{,} B)}{4} = A \underset{˙}{,} B$
140	134 139	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to \frac{(A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B) + (A \underset{˙}{,} B)}{4} = A \underset{˙}{,} B$
141	118 124 140	3eqtrrd	$⊢ ((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 \underset{˙}{-} B)}^{2} + i ({N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))}^{2} - {N (A \underset{˙}{-} (i \underset{˙}{\cdot} B))}^{2})}{4}$

Metamath Proof Explorer

Theorem cphipval2

Proof