cphipval2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cphipval2		Structured version Visualization version GIF version

Theorem cphipval2 25276

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

**Hypotheses**
Ref	Expression
cphipfval.x	⊢ 𝑋 = (Base‘𝑊)
cphipfval.p	⊢ + = (+_g‘𝑊)
cphipfval.s	⊢ · = ( ·_𝑠 ‘𝑊)
cphipfval.n	⊢ 𝑁 = (norm‘𝑊)
cphipfval.i	⊢ , = (·_𝑖‘𝑊)
cphipval2.m	⊢ − = (-_g‘𝑊)
cphipval2.f	⊢ 𝐹 = (Scalar‘𝑊)
cphipval2.k	⊢ 𝐾 = (Base‘𝐹)

**Assertion**
Ref	Expression
cphipval2	⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) = (((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) / 4))

**Proof of Theorem cphipval2**
Step	Hyp	Ref	Expression
1		simpl 485	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) → 𝑊 ∈ ℂPreHil)
2	1	3ad2ant1 1142	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑊 ∈ ℂPreHil)
3		cphngp 25208	. . . . . . . . . . 11 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp)
4	3	adantr 483	. . . . . . . . . 10 ⊢ ((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) → 𝑊 ∈ NrmGrp)
5		ngpgrp 24632	. . . . . . . . . 10 ⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ Grp)
6	4, 5	syl 17	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) → 𝑊 ∈ Grp)
7		cphipfval.x	. . . . . . . . . 10 ⊢ 𝑋 = (Base‘𝑊)
8		cphipfval.p	. . . . . . . . . 10 ⊢ + = (+_g‘𝑊)
9	7, 8	grpcl 18959	. . . . . . . . 9 ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 + 𝐵) ∈ 𝑋)
10	6, 9	syl3an1 1172	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 + 𝐵) ∈ 𝑋)
11		cphipfval.i	. . . . . . . . 9 ⊢ , = (·_𝑖‘𝑊)
12		cphipfval.n	. . . . . . . . 9 ⊢ 𝑁 = (norm‘𝑊)
13	7, 11, 12	nmsq 25229	. . . . . . . 8 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 + 𝐵) ∈ 𝑋) → ((𝑁‘(𝐴 + 𝐵))↑2) = ((𝐴 + 𝐵) , (𝐴 + 𝐵)))
14	2, 10, 13	syl2anc 592	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 + 𝐵))↑2) = ((𝐴 + 𝐵) , (𝐴 + 𝐵)))
15		simp2 1146	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ 𝑋)
16		simp3 1147	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋)
17	11, 7, 8, 2, 15, 16, 15, 16	cph2di 25242	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) , (𝐴 + 𝐵)) = (((𝐴 , 𝐴) + (𝐵 , 𝐵)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))))
18	14, 17	eqtrd 2791	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 + 𝐵))↑2) = (((𝐴 , 𝐴) + (𝐵 , 𝐵)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))))
19		cphipval2.m	. . . . . . . . . 10 ⊢ − = (-_g‘𝑊)
20	7, 19	grpsubcl 19038	. . . . . . . . 9 ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 − 𝐵) ∈ 𝑋)
21	6, 20	syl3an1 1172	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 − 𝐵) ∈ 𝑋)
22	7, 11, 12	nmsq 25229	. . . . . . . 8 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 − 𝐵) ∈ 𝑋) → ((𝑁‘(𝐴 − 𝐵))↑2) = ((𝐴 − 𝐵) , (𝐴 − 𝐵)))
23	2, 21, 22	syl2anc 592	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 − 𝐵))↑2) = ((𝐴 − 𝐵) , (𝐴 − 𝐵)))
24	11, 7, 19, 2, 15, 16, 15, 16	cph2subdi 25245	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 − 𝐵) , (𝐴 − 𝐵)) = (((𝐴 , 𝐴) + (𝐵 , 𝐵)) − ((𝐴 , 𝐵) + (𝐵 , 𝐴))))
25	23, 24	eqtrd 2791	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 − 𝐵))↑2) = (((𝐴 , 𝐴) + (𝐵 , 𝐵)) − ((𝐴 , 𝐵) + (𝐵 , 𝐴))))
26	18, 25	oveq12d 7403	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) = ((((𝐴 , 𝐴) + (𝐵 , 𝐵)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) − (((𝐴 , 𝐴) + (𝐵 , 𝐵)) − ((𝐴 , 𝐵) + (𝐵 , 𝐴)))))
27	7, 11	reipcl 25232	. . . . . . . . . 10 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑋) → (𝐴 , 𝐴) ∈ ℝ)
28	27	adantlr 723	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋) → (𝐴 , 𝐴) ∈ ℝ)
29	28	recnd 11200	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋) → (𝐴 , 𝐴) ∈ ℂ)
30	29	3adant3 1141	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐴) ∈ ℂ)
31	7, 11	reipcl 25232	. . . . . . . . . 10 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐵) ∈ ℝ)
32	31	adantlr 723	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐵) ∈ ℝ)
33	32	recnd 11200	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐵) ∈ ℂ)
34	33	3adant2 1140	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐵) ∈ ℂ)
35	30, 34	addcld 11191	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐴) + (𝐵 , 𝐵)) ∈ ℂ)
36	7, 11	cphipcl 25226	. . . . . . . 8 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) ∈ ℂ)
37	1, 36	syl3an1 1172	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) ∈ ℂ)
38	7, 11	cphipcl 25226	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐵 , 𝐴) ∈ ℂ)
39	1, 38	syl3an1 1172	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐵 , 𝐴) ∈ ℂ)
40	39	3com23 1135	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐴) ∈ ℂ)
41	37, 40	addcld 11191	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐵) + (𝐵 , 𝐴)) ∈ ℂ)
42	35, 41, 41	pnncand 11571	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐴) + (𝐵 , 𝐵)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) − (((𝐴 , 𝐴) + (𝐵 , 𝐵)) − ((𝐴 , 𝐵) + (𝐵 , 𝐴)))) = (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))))
43	26, 42	eqtrd 2791	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) = (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))))
44	6	3ad2ant1 1142	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑊 ∈ Grp)
45		cphlmod 25209	. . . . . . . . . . . . . 14 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod)
46	45	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) → 𝑊 ∈ LMod)
47	46	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → 𝑊 ∈ LMod)
48		simplr 776	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → i ∈ 𝐾)
49		simpr 487	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋)
50		cphipval2.f	. . . . . . . . . . . . 13 ⊢ 𝐹 = (Scalar‘𝑊)
51		cphipfval.s	. . . . . . . . . . . . 13 ⊢ · = ( ·_𝑠 ‘𝑊)
52		cphipval2.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = (Base‘𝐹)
53	7, 50, 51, 52	lmodvscl 20918	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋) → (i · 𝐵) ∈ 𝑋)
54	47, 48, 49, 53	syl3anc 1386	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → (i · 𝐵) ∈ 𝑋)
55	54	3adant2 1140	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · 𝐵) ∈ 𝑋)
56	7, 8	grpcl 18959	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (i · 𝐵) ∈ 𝑋) → (𝐴 + (i · 𝐵)) ∈ 𝑋)
57	44, 15, 55, 56	syl3anc 1386	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 + (i · 𝐵)) ∈ 𝑋)
58	7, 11, 12	nmsq 25229	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 + (i · 𝐵)) ∈ 𝑋) → ((𝑁‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴 + (i · 𝐵)) , (𝐴 + (i · 𝐵))))
59	2, 57, 58	syl2anc 592	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴 + (i · 𝐵)) , (𝐴 + (i · 𝐵))))
60	11, 7, 8, 2, 15, 55, 15, 55	cph2di 25242	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + (i · 𝐵)) , (𝐴 + (i · 𝐵))) = (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))
61	59, 60	eqtrd 2791	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 + (i · 𝐵)))↑2) = (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))
62	7, 19	grpsubcl 19038	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (i · 𝐵) ∈ 𝑋) → (𝐴 − (i · 𝐵)) ∈ 𝑋)
63	44, 15, 55, 62	syl3anc 1386	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 − (i · 𝐵)) ∈ 𝑋)
64	7, 11, 12	nmsq 25229	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 − (i · 𝐵)) ∈ 𝑋) → ((𝑁‘(𝐴 − (i · 𝐵)))↑2) = ((𝐴 − (i · 𝐵)) , (𝐴 − (i · 𝐵))))
65	2, 63, 64	syl2anc 592	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 − (i · 𝐵)))↑2) = ((𝐴 − (i · 𝐵)) , (𝐴 − (i · 𝐵))))
66	11, 7, 19, 2, 15, 55, 15, 55	cph2subdi 25245	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 − (i · 𝐵)) , (𝐴 − (i · 𝐵))) = (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))
67	65, 66	eqtrd 2791	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 − (i · 𝐵)))↑2) = (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))
68	61, 67	oveq12d 7403	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)) = ((((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) − (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))))
69	68	oveq2d 7401	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2))) = (i · ((((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) − (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))))
70	7, 11	cphipcl 25226	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ (i · 𝐵) ∈ 𝑋 ∧ (i · 𝐵) ∈ 𝑋) → ((i · 𝐵) , (i · 𝐵)) ∈ ℂ)
71	2, 55, 55, 70	syl3anc 1386	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · 𝐵) , (i · 𝐵)) ∈ ℂ)
72	30, 71	addcld 11191	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) ∈ ℂ)
73	7, 11	cphipcl 25226	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑋 ∧ (i · 𝐵) ∈ 𝑋) → (𝐴 , (i · 𝐵)) ∈ ℂ)
74	2, 15, 55, 73	syl3anc 1386	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , (i · 𝐵)) ∈ ℂ)
75	7, 11	cphipcl 25226	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ (i · 𝐵) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((i · 𝐵) , 𝐴) ∈ ℂ)
76	2, 55, 15, 75	syl3anc 1386	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · 𝐵) , 𝐴) ∈ ℂ)
77	74, 76	addcld 11191	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) ∈ ℂ)
78	72, 77, 77	pnncand 11571	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) − (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))) = (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))
79	78	oveq2d 7401	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · ((((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) − (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))) = (i · (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))))
80	7, 51, 11, 50, 52	cphassir 25250	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , (i · 𝐵)) = (-i · (𝐴 , 𝐵)))
81	7, 51, 11, 50, 52	cphassi 25249	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · 𝐵) , 𝐴) = (i · (𝐵 , 𝐴)))
82	80, 81	oveq12d 7403	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) = ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))
83	82, 82	oveq12d 7403	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) = (((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))) + ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))))
84	83	oveq2d 7401	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))) = (i · (((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))) + ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))))
85		ax-icn 11122	. . . . . . . 8 ⊢ i ∈ ℂ
86	85	a1i 11	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → i ∈ ℂ)
87		negicn 11421	. . . . . . . . . 10 ⊢ -i ∈ ℂ
88	87	a1i 11	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → -i ∈ ℂ)
89	88, 37	mulcld 11192	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (-i · (𝐴 , 𝐵)) ∈ ℂ)
90	86, 40	mulcld 11192	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (𝐵 , 𝐴)) ∈ ℂ)
91	89, 90	addcld 11191	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))) ∈ ℂ)
92	86, 91, 91	adddid 11196	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))) + ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))) = ((i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) + (i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))))
93	86, 89, 90	adddid 11196	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) = ((i · (-i · (𝐴 , 𝐵))) + (i · (i · (𝐵 , 𝐴)))))
94	86, 88, 37	mulassd 11195	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · -i) · (𝐴 , 𝐵)) = (i · (-i · (𝐴 , 𝐵))))
95	85, 85	mulneg2i 11624	. . . . . . . . . . . . 13 ⊢ (i · -i) = -(i · i)
96		ixi 11806	. . . . . . . . . . . . . 14 ⊢ (i · i) = -1
97	96	negeqi 11413	. . . . . . . . . . . . 13 ⊢ -(i · i) = --1
98		negneg1e1 12174	. . . . . . . . . . . . 13 ⊢ --1 = 1
99	95, 97, 98	3eqtri 2783	. . . . . . . . . . . 12 ⊢ (i · -i) = 1
100	99	oveq1i 7395	. . . . . . . . . . 11 ⊢ ((i · -i) · (𝐴 , 𝐵)) = (1 · (𝐴 , 𝐵))
101	94, 100	eqtr3di 2806	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (-i · (𝐴 , 𝐵))) = (1 · (𝐴 , 𝐵)))
102	86, 86, 40	mulassd 11195	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · i) · (𝐵 , 𝐴)) = (i · (i · (𝐵 , 𝐴))))
103	96	oveq1i 7395	. . . . . . . . . . 11 ⊢ ((i · i) · (𝐵 , 𝐴)) = (-1 · (𝐵 , 𝐴))
104	102, 103	eqtr3di 2806	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (i · (𝐵 , 𝐴))) = (-1 · (𝐵 , 𝐴)))
105	101, 104	oveq12d 7403	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · (-i · (𝐴 , 𝐵))) + (i · (i · (𝐵 , 𝐴)))) = ((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴))))
106	93, 105	eqtrd 2791	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) = ((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴))))
107	106, 106	oveq12d 7403	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) + (i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))) = (((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴))) + ((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴)))))
108	37	mullidd 11190	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (1 · (𝐴 , 𝐵)) = (𝐴 , 𝐵))
109	108	oveq1d 7400	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴))) = ((𝐴 , 𝐵) + (-1 · (𝐵 , 𝐴))))
110		addneg1mul 11619	. . . . . . . . . 10 ⊢ (((𝐴 , 𝐵) ∈ ℂ ∧ (𝐵 , 𝐴) ∈ ℂ) → ((𝐴 , 𝐵) + (-1 · (𝐵 , 𝐴))) = ((𝐴 , 𝐵) − (𝐵 , 𝐴)))
111	37, 40, 110	syl2anc 592	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐵) + (-1 · (𝐵 , 𝐴))) = ((𝐴 , 𝐵) − (𝐵 , 𝐴)))
112	109, 111	eqtrd 2791	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴))) = ((𝐴 , 𝐵) − (𝐵 , 𝐴)))
113	112, 112	oveq12d 7403	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴))) + ((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴)))) = (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))))
114	107, 113	eqtrd 2791	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) + (i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))) = (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))))
115	84, 92, 114	3eqtrd 2795	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))) = (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))))
116	69, 79, 115	3eqtrd 2795	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2))) = (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))))
117	43, 116	oveq12d 7403	. . 3 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) = ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))))
118	117	oveq1d 7400	. 2 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) / 4) = (((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) / 4))
119	37, 40	subcld 11532	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐵) − (𝐵 , 𝐴)) ∈ ℂ)
120	41, 41, 119, 119	add4d 11402	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) = ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))) + (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))))
121	37, 40, 37	ppncand 11572	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))) = ((𝐴 , 𝐵) + (𝐴 , 𝐵)))
122	121, 121	oveq12d 7403	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))) + (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) = (((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))))
123	120, 122	eqtrd 2791	. . 3 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) = (((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))))
124	123	oveq1d 7400	. 2 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) / 4) = ((((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) / 4))
125	37	2timesd 12454	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (2 · (𝐴 , 𝐵)) = ((𝐴 , 𝐵) + (𝐴 , 𝐵)))
126	125	eqcomd 2762	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐵) + (𝐴 , 𝐵)) = (2 · (𝐴 , 𝐵)))
127	126, 126	oveq12d 7403	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) = ((2 · (𝐴 , 𝐵)) + (2 · (𝐴 , 𝐵))))
128		2cnd 12286	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 2 ∈ ℂ)
129	128, 128, 37	adddird 11197	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((2 + 2) · (𝐴 , 𝐵)) = ((2 · (𝐴 , 𝐵)) + (2 · (𝐴 , 𝐵))))
130		2p2e4 12342	. . . . . . 7 ⊢ (2 + 2) = 4
131	130	a1i 11	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (2 + 2) = 4)
132	131	oveq1d 7400	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((2 + 2) · (𝐴 , 𝐵)) = (4 · (𝐴 , 𝐵)))
133	127, 129, 132	3eqtr2d 2797	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) = (4 · (𝐴 , 𝐵)))
134	133	oveq1d 7400	. . 3 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) / 4) = ((4 · (𝐴 , 𝐵)) / 4))
135		4cn 12293	. . . . 5 ⊢ 4 ∈ ℂ
136	135	a1i 11	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 4 ∈ ℂ)
137		4ne0 12319	. . . . 5 ⊢ 4 ≠ 0
138	137	a1i 11	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 4 ≠ 0)
139	37, 136, 138	divcan3d 11962	. . 3 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((4 · (𝐴 , 𝐵)) / 4) = (𝐴 , 𝐵))
140	134, 139	eqtrd 2791	. 2 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) / 4) = (𝐴 , 𝐵))
141	118, 124, 140	3eqtrrd 2796	1 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) = (((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) / 4))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1095 = wceq 1554 ∈ wcel 2136 ≠ wne 2951 ‘cfv 6510 (class class class)co 7385 ℂcc 11061 ℝcr 11062 0cc0 11063 1c1 11064 ici 11065 + caddc 11066 · cmul 11068 − cmin 11404 -cneg 11405 / cdiv 11834 2c2 12262 4c4 12264 ↑cexp 14064 Basecbs 17221 +_gcplusg 17262 Scalarcsca 17265 ·_𝑠 cvsca 17266 ·_𝑖cip 17267 Grpcgrp 18951 -_gcsg 18953 LModclmod 20900 normcnm 24609 NrmGrpcngp 24610 ℂPreHilccph 25201

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1809 ax-4 1823 ax-5 1924 ax-6 1981 ax-7 2022 ax-8 2138 ax-9 2146 ax-10 2169 ax-11 2185 ax-12 2206 ax-ext 2728 ax-rep 5221 ax-sep 5240 ax-nul 5250 ax-pow 5316 ax-pr 5384 ax-un 7707 ax-cnex 11119 ax-resscn 11120 ax-1cn 11121 ax-icn 11122 ax-addcl 11123 ax-addrcl 11124 ax-mulcl 11125 ax-mulrcl 11126 ax-mulcom 11127 ax-addass 11128 ax-mulass 11129 ax-distr 11130 ax-i2m1 11131 ax-1ne0 11132 ax-1rid 11133 ax-rnegex 11134 ax-rrecex 11135 ax-cnre 11136 ax-pre-lttri 11137 ax-pre-lttrn 11138 ax-pre-ltadd 11139 ax-pre-mulgt0 11140 ax-pre-sup 11141 ax-addf 11142 ax-mulf 11143

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3or 1096 df-3an 1097 df-tru 1557 df-fal 1567 df-ex 1794 df-nf 1798 df-sb 2085 df-mo 2560 df-eu 2590 df-clab 2735 df-cleq 2748 df-clel 2831 df-nfc 2905 df-ne 2952 df-nel 3056 df-ral 3071 df-rex 3081 df-rmo 3361 df-reu 3362 df-rab 3409 df-v 3450 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4281 df-if 4475 df-pw 4551 df-sn 4577 df-pr 4579 df-tp 4581 df-op 4583 df-uni 4860 df-iun 4945 df-br 5095 df-opab 5157 df-mpt 5176 df-tr 5202 df-id 5535 df-eprel 5540 df-po 5548 df-so 5549 df-fr 5593 df-we 5595 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-rn 5651 df-res 5652 df-ima 5653 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6466 df-fun 6512 df-fn 6513 df-f 6514 df-f1 6515 df-fo 6516 df-f1o 6517 df-fv 6518 df-riota 7342 df-ov 7388 df-oprab 7389 df-mpo 7390 df-om 7836 df-1st 7959 df-2nd 7960 df-tpos 8194 df-frecs 8250 df-wrecs 8281 df-recs 8330 df-rdg 8369 df-1o 8425 df-er 8666 df-map 8798 df-en 8917 df-dom 8918 df-sdom 8919 df-fin 8920 df-sup 9378 df-inf 9379 df-pnf 11208 df-mnf 11209 df-xr 11210 df-ltxr 11211 df-le 11212 df-sub 11406 df-neg 11407 df-div 11835 df-nn 12201 df-2 12270 df-3 12271 df-4 12272 df-5 12273 df-6 12274 df-7 12275 df-8 12276 df-9 12277 df-n0 12472 df-z 12559 df-dec 12679 df-uz 12830 df-q 12940 df-rp 12984 df-xneg 13104 df-xadd 13105 df-xmul 13106 df-fz 13503 df-seq 14005 df-exp 14065 df-cj 15102 df-re 15103 df-im 15104 df-sqrt 15238 df-abs 15239 df-struct 17159 df-sets 17176 df-slot 17194 df-ndx 17206 df-base 17222 df-ress 17243 df-plusg 17275 df-mulr 17276 df-starv 17277 df-sca 17278 df-vsca 17279 df-ip 17280 df-tset 17281 df-ple 17282 df-ds 17284 df-unif 17285 df-0g 17446 df-topgen 17448 df-mgm 18650 df-sgrp 18729 df-mnd 18745 df-mhm 18793 df-grp 18954 df-minusg 18955 df-sbg 18956 df-subg 19141 df-ghm 19230 df-cmn 19798 df-abl 19799 df-mgp 20163 df-rng 20175 df-ur 20204 df-ring 20257 df-cring 20258 df-oppr 20358 df-dvdsr 20378 df-unit 20379 df-rhm 20493 df-subrg 20592 df-drng 20753 df-staf 20861 df-srng 20862 df-lmod 20902 df-lmhm 21062 df-lvec 21143 df-sra 21213 df-rgmod 21214 df-psmet 21389 df-xmet 21390 df-met 21391 df-bl 21392 df-mopn 21393 df-cnfld 21398 df-phl 21651 df-top 22927 df-topon 22944 df-topsp 22966 df-bases 22979 df-xms 24353 df-ms 24354 df-nm 24615 df-ngp 24616 df-nlm 24619 df-clm 25098 df-cph 25203

This theorem is referenced by: 4cphipval2 25277 cphipval 25278

W3C validator