4cphipval2

Description: Four times the inner product value cphipval2 . (Contributed by NM, 1-Feb-2008) (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	4cphipval2	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 4 (A \underset{˙}{,} B) = {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})$

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	1 2 3 4 5 6 7 8	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}$
10	9	oveq2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 4 (A \underset{˙}{,} B) = 4 (\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})$
11	7 8	cphsubrg	$⊢ W \in CPreHil \to K \in SubRing (ℂ_{fld})$
12		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
13	12	subrgss	$⊢ K \in SubRing (ℂ_{fld}) \to K \subseteq ℂ$
14	11 13	syl	$⊢ W \in CPreHil \to K \subseteq ℂ$
15	14	adantr	$⊢ (W \in CPreHil \land i \in K) \to K \subseteq ℂ$
16	15	3ad2ant1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to K \subseteq ℂ$
17		simp1l	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to W \in CPreHil$
18		cphngp	$⊢ W \in CPreHil \to W \in NrmGrp$
19		ngpgrp	$⊢ W \in NrmGrp \to W \in Grp$
20	18 19	syl	$⊢ W \in CPreHil \to W \in Grp$
21	20	adantr	$⊢ (W \in CPreHil \land i \in K) \to W \in Grp$
22	1 2	grpcl	$⊢ (W \in Grp \land A \in X \land B \in X) \to A \underset{˙}{+} B \in X$
23	21 22	syl3an1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{+} B \in X$
24	1 5 4 7 8	cphnmcl	$⊢ (W \in CPreHil \land A \underset{˙}{+} B \in X) \to N (A \underset{˙}{+} B) \in K$
25	17 23 24	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to N (A \underset{˙}{+} B) \in K$
26	16 25	sseldd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to N (A \underset{˙}{+} B) \in ℂ$
27	26	sqcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{+} B)}^{2} \in ℂ$
28	1 6	grpsubcl	$⊢ (W \in Grp \land A \in X \land B \in X) \to A \underset{˙}{-} B \in X$
29	21 28	syl3an1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{-} B \in X$
30	1 5 4 7 8	cphnmcl	$⊢ (W \in CPreHil \land A \underset{˙}{-} B \in X) \to N (A \underset{˙}{-} B) \in K$
31	17 29 30	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to N (A \underset{˙}{-} B) \in K$
32	16 31	sseldd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to N (A \underset{˙}{-} B) \in ℂ$
33	32	sqcld	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to {N (A \underset{˙}{-} B)}^{2} \in ℂ$
34	27 33	subcld	$⊢ ((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} \in ℂ$
35		ax-icn	$⊢ i \in ℂ$
36	35	a1i	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i \in ℂ$
37	17 20	syl	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to W \in Grp$
38		simp2	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \in X$
39		cphlmod	$⊢ W \in CPreHil \to W \in LMod$
40	39	adantr	$⊢ (W \in CPreHil \land i \in K) \to W \in LMod$
41	40	3ad2ant1	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to W \in LMod$
42		simp1r	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i \in K$
43		simp3	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to B \in X$
44	1 7 3 8	lmodvscl	$⊢ (W \in LMod \land i \in K \land B \in X) \to i \underset{˙}{\cdot} B \in X$
45	41 42 43 44	syl3anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i \underset{˙}{\cdot} B \in X$
46	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$
47	37 38 45 46	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$
48	1 5 4 7 8	cphnmcl	$⊢ (W \in CPreHil \land A \underset{˙}{+} (i \underset{˙}{\cdot} B) \in X) \to N (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \in K$
49	17 47 48	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to N (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \in K$
50	16 49	sseldd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to N (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \in ℂ$
51	50	sqcld	$⊢ ((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 ℂ$
52	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$
53	37 38 45 52	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$
54	1 5 4 7 8	cphnmcl	$⊢ (W \in CPreHil \land A \underset{˙}{-} (i \underset{˙}{\cdot} B) \in X) \to N (A \underset{˙}{-} (i \underset{˙}{\cdot} B)) \in K$
55	17 53 54	syl2anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to N (A \underset{˙}{-} (i \underset{˙}{\cdot} B)) \in K$
56	16 55	sseldd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to N (A \underset{˙}{-} (i \underset{˙}{\cdot} B)) \in ℂ$
57	56	sqcld	$⊢ ((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 ℂ$
58	51 57	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 \underset{˙}{-} (i \underset{˙}{\cdot} B))}^{2} \in ℂ$
59	36 58	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 \underset{˙}{-} (i \underset{˙}{\cdot} B))}^{2}) \in ℂ$
60	34 59	addcld	$⊢ ((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}) \in ℂ$
61		4cn	$⊢ 4 \in ℂ$
62	61	a1i	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 4 \in ℂ$
63		4ne0	$⊢ 4 \neq 0$
64	63	a1i	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 4 \neq 0$
65	60 62 64	divcan2d	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 4 (\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}) = {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})$
66	10 65	eqtrd	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to 4 (A \underset{˙}{,} B) = {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})$

Metamath Proof Explorer

Theorem 4cphipval2

Proof