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 25563

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 488	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) → 𝑊 ∈ ℂPreHil)
2	1	3ad2ant1 1151	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑊 ∈ ℂPreHil)
3		cphngp 25495	. . . . . . . . . . 11 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp)
4	3	adantr 486	. . . . . . . . . 10 ⊢ ((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) → 𝑊 ∈ NrmGrp)
5		ngpgrp 24919	. . . . . . . . . 10 ⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ Grp)
6	4, 5	syl 18	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) → 𝑊 ∈ Grp)
7		cphipfval.x	. . . . . . . . . 10 ⊢ 𝑋 = (Base‘𝑊)
8		cphipfval.p	. . . . . . . . . 10 ⊢ + = (+_g‘𝑊)
9	7, 8	grpcl 19153	. . . . . . . . 9 ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 + 𝐵) ∈ 𝑋)
10	6, 9	syl3an1 1181	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 + 𝐵) ∈ 𝑋)
11		cphipfval.i	. . . . . . . . 9 ⊢ , = (·_𝑖‘𝑊)
12		cphipfval.n	. . . . . . . . 9 ⊢ 𝑁 = (norm‘𝑊)
13	7, 11, 12	nmsq 25516	. . . . . . . 8 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 + 𝐵) ∈ 𝑋) → ((𝑁‘(𝐴 + 𝐵))↑2) = ((𝐴 + 𝐵) , (𝐴 + 𝐵)))
14	2, 10, 13	syl2anc 596	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 + 𝐵))↑2) = ((𝐴 + 𝐵) , (𝐴 + 𝐵)))
15		simp2 1155	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ 𝑋)
16		simp3 1156	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋)
17	11, 7, 8, 2, 15, 16, 15, 16	cph2di 25529	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) , (𝐴 + 𝐵)) = (((𝐴 , 𝐴) + (𝐵 , 𝐵)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))))
18	14, 17	eqtrd 2795	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 + 𝐵))↑2) = (((𝐴 , 𝐴) + (𝐵 , 𝐵)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))))
19		cphipval2.m	. . . . . . . . . 10 ⊢ − = (-_g‘𝑊)
20	7, 19	grpsubcl 19231	. . . . . . . . 9 ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 − 𝐵) ∈ 𝑋)
21	6, 20	syl3an1 1181	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 − 𝐵) ∈ 𝑋)
22	7, 11, 12	nmsq 25516	. . . . . . . 8 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 − 𝐵) ∈ 𝑋) → ((𝑁‘(𝐴 − 𝐵))↑2) = ((𝐴 − 𝐵) , (𝐴 − 𝐵)))
23	2, 21, 22	syl2anc 596	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 − 𝐵))↑2) = ((𝐴 − 𝐵) , (𝐴 − 𝐵)))
24	11, 7, 19, 2, 15, 16, 15, 16	cph2subdi 25532	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 − 𝐵) , (𝐴 − 𝐵)) = (((𝐴 , 𝐴) + (𝐵 , 𝐵)) − ((𝐴 , 𝐵) + (𝐵 , 𝐴))))
25	23, 24	eqtrd 2795	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 − 𝐵))↑2) = (((𝐴 , 𝐴) + (𝐵 , 𝐵)) − ((𝐴 , 𝐵) + (𝐵 , 𝐴))))
26	18, 25	oveq12d 7438	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) = ((((𝐴 , 𝐴) + (𝐵 , 𝐵)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) − (((𝐴 , 𝐴) + (𝐵 , 𝐵)) − ((𝐴 , 𝐵) + (𝐵 , 𝐴)))))
27	7, 11	reipcl 25519	. . . . . . . . . 10 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑋) → (𝐴 , 𝐴) ∈ ℝ)
28	27	adantlr 728	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋) → (𝐴 , 𝐴) ∈ ℝ)
29	28	recnd 11338	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋) → (𝐴 , 𝐴) ∈ ℂ)
30	29	3adant3 1150	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐴) ∈ ℂ)
31	7, 11	reipcl 25519	. . . . . . . . . 10 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐵) ∈ ℝ)
32	31	adantlr 728	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐵) ∈ ℝ)
33	32	recnd 11338	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐵) ∈ ℂ)
34	33	3adant2 1149	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐵) ∈ ℂ)
35	30, 34	addcld 11329	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐴) + (𝐵 , 𝐵)) ∈ ℂ)
36	7, 11	cphipcl 25513	. . . . . . . 8 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) ∈ ℂ)
37	1, 36	syl3an1 1181	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) ∈ ℂ)
38	7, 11	cphipcl 25513	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐵 , 𝐴) ∈ ℂ)
39	1, 38	syl3an1 1181	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐵 , 𝐴) ∈ ℂ)
40	39	3com23 1144	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐴) ∈ ℂ)
41	37, 40	addcld 11329	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐵) + (𝐵 , 𝐴)) ∈ ℂ)
42	35, 41, 41	pnncand 11709	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐴) + (𝐵 , 𝐵)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) − (((𝐴 , 𝐴) + (𝐵 , 𝐵)) − ((𝐴 , 𝐵) + (𝐵 , 𝐴)))) = (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))))
43	26, 42	eqtrd 2795	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) = (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))))
44	6	3ad2ant1 1151	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑊 ∈ Grp)
45		cphlmod 25496	. . . . . . . . . . . . . 14 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod)
46	45	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) → 𝑊 ∈ LMod)
47	46	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → 𝑊 ∈ LMod)
48		simplr 781	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → i ∈ 𝐾)
49		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋)
50		cphipval2.f	. . . . . . . . . . . . 13 ⊢ 𝐹 = (Scalar‘𝑊)
51		cphipfval.s	. . . . . . . . . . . . 13 ⊢ · = ( ·_𝑠 ‘𝑊)
52		cphipval2.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = (Base‘𝐹)
53	7, 50, 51, 52	lmodvscl 21154	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋) → (i · 𝐵) ∈ 𝑋)
54	47, 48, 49, 53	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → (i · 𝐵) ∈ 𝑋)
55	54	3adant2 1149	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · 𝐵) ∈ 𝑋)
56	7, 8	grpcl 19153	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (i · 𝐵) ∈ 𝑋) → (𝐴 + (i · 𝐵)) ∈ 𝑋)
57	44, 15, 55, 56	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 + (i · 𝐵)) ∈ 𝑋)
58	7, 11, 12	nmsq 25516	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 + (i · 𝐵)) ∈ 𝑋) → ((𝑁‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴 + (i · 𝐵)) , (𝐴 + (i · 𝐵))))
59	2, 57, 58	syl2anc 596	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴 + (i · 𝐵)) , (𝐴 + (i · 𝐵))))
60	11, 7, 8, 2, 15, 55, 15, 55	cph2di 25529	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + (i · 𝐵)) , (𝐴 + (i · 𝐵))) = (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))
61	59, 60	eqtrd 2795	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 + (i · 𝐵)))↑2) = (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))
62	7, 19	grpsubcl 19231	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (i · 𝐵) ∈ 𝑋) → (𝐴 − (i · 𝐵)) ∈ 𝑋)
63	44, 15, 55, 62	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 − (i · 𝐵)) ∈ 𝑋)
64	7, 11, 12	nmsq 25516	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 − (i · 𝐵)) ∈ 𝑋) → ((𝑁‘(𝐴 − (i · 𝐵)))↑2) = ((𝐴 − (i · 𝐵)) , (𝐴 − (i · 𝐵))))
65	2, 63, 64	syl2anc 596	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 − (i · 𝐵)))↑2) = ((𝐴 − (i · 𝐵)) , (𝐴 − (i · 𝐵))))
66	11, 7, 19, 2, 15, 55, 15, 55	cph2subdi 25532	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 − (i · 𝐵)) , (𝐴 − (i · 𝐵))) = (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))
67	65, 66	eqtrd 2795	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 − (i · 𝐵)))↑2) = (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))
68	61, 67	oveq12d 7438	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)) = ((((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) − (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))))
69	68	oveq2d 7436	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2))) = (i · ((((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) − (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))))
70	7, 11	cphipcl 25513	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ (i · 𝐵) ∈ 𝑋 ∧ (i · 𝐵) ∈ 𝑋) → ((i · 𝐵) , (i · 𝐵)) ∈ ℂ)
71	2, 55, 55, 70	syl3anc 1398	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · 𝐵) , (i · 𝐵)) ∈ ℂ)
72	30, 71	addcld 11329	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) ∈ ℂ)
73	7, 11	cphipcl 25513	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑋 ∧ (i · 𝐵) ∈ 𝑋) → (𝐴 , (i · 𝐵)) ∈ ℂ)
74	2, 15, 55, 73	syl3anc 1398	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , (i · 𝐵)) ∈ ℂ)
75	7, 11	cphipcl 25513	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ (i · 𝐵) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((i · 𝐵) , 𝐴) ∈ ℂ)
76	2, 55, 15, 75	syl3anc 1398	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · 𝐵) , 𝐴) ∈ ℂ)
77	74, 76	addcld 11329	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) ∈ ℂ)
78	72, 77, 77	pnncand 11709	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) − (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))) = (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))
79	78	oveq2d 7436	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · ((((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) − (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))) = (i · (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))))
80	7, 51, 11, 50, 52	cphassir 25537	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , (i · 𝐵)) = ( -i · (𝐴 , 𝐵)))
81	7, 51, 11, 50, 52	cphassi 25536	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · 𝐵) , 𝐴) = (i · (𝐵 , 𝐴)))
82	80, 81	oveq12d 7438	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) = (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))
83	82, 82	oveq12d 7438	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) = ((( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))) + (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))))
84	83	oveq2d 7436	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))) = (i · ((( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))) + (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))))
85		ax-icn 11260	. . . . . . . 8 ⊢ i ∈ ℂ
86	85	a1i 11	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → i ∈ ℂ)
87		negicn 11559	. . . . . . . . . 10 ⊢ -i ∈ ℂ
88	87	a1i 11	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → -i ∈ ℂ)
89	88, 37	mulcld 11330	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ( -i · (𝐴 , 𝐵)) ∈ ℂ)
90	86, 40	mulcld 11330	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (𝐵 , 𝐴)) ∈ ℂ)
91	89, 90	addcld 11329	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))) ∈ ℂ)
92	86, 91, 91	adddid 11334	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · ((( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))) + (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))) = ((i · (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) + (i · (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))))
93	86, 89, 90	adddid 11334	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) = ((i · ( -i · (𝐴 , 𝐵))) + (i · (i · (𝐵 , 𝐴)))))
94	86, 88, 37	mulassd 11333	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · -i) · (𝐴 , 𝐵)) = (i · ( -i · (𝐴 , 𝐵))))
95	85, 85	mulneg2i 11764	. . . . . . . . . . . . 13 ⊢ (i · -i) = -(i · i)
96		ixi 11946	. . . . . . . . . . . . . 14 ⊢ (i · i) = -1
97	96	negeqi 11551	. . . . . . . . . . . . 13 ⊢ -(i · i) = - -1
98		negneg1e1 12310	. . . . . . . . . . . . 13 ⊢ - -1 = 1
99	95, 97, 98	3eqtri 2787	. . . . . . . . . . . 12 ⊢ (i · -i) = 1
100	99	oveq1i 7430	. . . . . . . . . . 11 ⊢ ((i · -i) · (𝐴 , 𝐵)) = (1 · (𝐴 , 𝐵))
101	94, 100	eqtr3di 2810	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · ( -i · (𝐴 , 𝐵))) = (1 · (𝐴 , 𝐵)))
102	86, 86, 40	mulassd 11333	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · i) · (𝐵 , 𝐴)) = (i · (i · (𝐵 , 𝐴))))
103	96	oveq1i 7430	. . . . . . . . . . 11 ⊢ ((i · i) · (𝐵 , 𝐴)) = ( -1 · (𝐵 , 𝐴))
104	102, 103	eqtr3di 2810	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (i · (𝐵 , 𝐴))) = ( -1 · (𝐵 , 𝐴)))
105	101, 104	oveq12d 7438	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · ( -i · (𝐴 , 𝐵))) + (i · (i · (𝐵 , 𝐴)))) = ((1 · (𝐴 , 𝐵)) + ( -1 · (𝐵 , 𝐴))))
106	93, 105	eqtrd 2795	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) = ((1 · (𝐴 , 𝐵)) + ( -1 · (𝐵 , 𝐴))))
107	106, 106	oveq12d 7438	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) + (i · (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))) = (((1 · (𝐴 , 𝐵)) + ( -1 · (𝐵 , 𝐴))) + ((1 · (𝐴 , 𝐵)) + ( -1 · (𝐵 , 𝐴)))))
108	37	mullidd 11328	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (1 · (𝐴 , 𝐵)) = (𝐴 , 𝐵))
109	108	oveq1d 7435	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((1 · (𝐴 , 𝐵)) + ( -1 · (𝐵 , 𝐴))) = ((𝐴 , 𝐵) + ( -1 · (𝐵 , 𝐴))))
110		addneg1mul 11759	. . . . . . . . . 10 ⊢ (((𝐴 , 𝐵) ∈ ℂ ∧ (𝐵 , 𝐴) ∈ ℂ) → ((𝐴 , 𝐵) + ( -1 · (𝐵 , 𝐴))) = ((𝐴 , 𝐵) − (𝐵 , 𝐴)))
111	37, 40, 110	syl2anc 596	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐵) + ( -1 · (𝐵 , 𝐴))) = ((𝐴 , 𝐵) − (𝐵 , 𝐴)))
112	109, 111	eqtrd 2795	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((1 · (𝐴 , 𝐵)) + ( -1 · (𝐵 , 𝐴))) = ((𝐴 , 𝐵) − (𝐵 , 𝐴)))
113	112, 112	oveq12d 7438	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((1 · (𝐴 , 𝐵)) + ( -1 · (𝐵 , 𝐴))) + ((1 · (𝐴 , 𝐵)) + ( -1 · (𝐵 , 𝐴)))) = (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))))
114	107, 113	eqtrd 2795	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) + (i · (( -i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))) = (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))))
115	84, 92, 114	3eqtrd 2799	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))) = (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))))
116	69, 79, 115	3eqtrd 2799	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2))) = (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))))
117	43, 116	oveq12d 7438	. . 3 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) = ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))))
118	117	oveq1d 7435	. 2 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) / 4) = (((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) / 4))
119	37, 40	subcld 11670	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐵) − (𝐵 , 𝐴)) ∈ ℂ)
120	41, 41, 119, 119	add4d 11540	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) = ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))) + (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))))
121	37, 40, 37	ppncand 11710	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))) = ((𝐴 , 𝐵) + (𝐴 , 𝐵)))
122	121, 121	oveq12d 7438	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))) + (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) = (((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))))
123	120, 122	eqtrd 2795	. . 3 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) = (((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))))
124	123	oveq1d 7435	. 2 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) / 4) = ((((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) / 4))
125	37	2timesd 12590	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (2 · (𝐴 , 𝐵)) = ((𝐴 , 𝐵) + (𝐴 , 𝐵)))
126	125	eqcomd 2766	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐵) + (𝐴 , 𝐵)) = (2 · (𝐴 , 𝐵)))
127	126, 126	oveq12d 7438	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) = ((2 · (𝐴 , 𝐵)) + (2 · (𝐴 , 𝐵))))
128		2cnd 12422	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 2 ∈ ℂ)
129	128, 128, 37	adddird 11335	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((2 + 2) · (𝐴 , 𝐵)) = ((2 · (𝐴 , 𝐵)) + (2 · (𝐴 , 𝐵))))
130		2p2e4 12478	. . . . . . 7 ⊢ (2 + 2) = 4
131	130	a1i 11	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (2 + 2) = 4)
132	131	oveq1d 7435	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((2 + 2) · (𝐴 , 𝐵)) = (4 · (𝐴 , 𝐵)))
133	127, 129, 132	3eqtr2d 2801	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) = (4 · (𝐴 , 𝐵)))
134	133	oveq1d 7435	. . 3 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) / 4) = ((4 · (𝐴 , 𝐵)) / 4))
135		4cn 12429	. . . . 5 ⊢ 4 ∈ ℂ
136	135	a1i 11	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 4 ∈ ℂ)
137		4ne0 12455	. . . . 5 ⊢ 4 ≠ 0
138	137	a1i 11	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 4 ≠ 0)
139	37, 136, 138	divcan3d 12099	. . 3 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((4 · (𝐴 , 𝐵)) / 4) = (𝐴 , 𝐵))
140	134, 139	eqtrd 2795	. 2 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) / 4) = (𝐴 , 𝐵))
141	118, 124, 140	3eqtrrd 2800	1 ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) = (((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) / 4))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ‘cfv 6538 (class class class)co 7420 ℂcc 11199 ℝcr 11200 0cc0 11201 1c1 11202 ici 11203 + caddc 11204 · cmul 11206 − cmin 11542 -cneg 11543 / cdiv 11974 2c2 12398 4c4 12400 ↑cexp 14205 Basecbs 17388 +_gcplusg 17429 Scalarcsca 17432 ·_𝑠 cvsca 17433 ·_𝑖cip 17434 Grpcgrp 19145 -_gcsg 19147 LModclmod 21136 normcnm 24896 NrmGrpcngp 24897 ℂPreHilccph 25488

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11257 ax-resscn 11258 ax-1cn 11259 ax-icn 11260 ax-addcl 11261 ax-addrcl 11262 ax-mulcl 11263 ax-mulrcl 11264 ax-mulcom 11265 ax-addass 11266 ax-mulass 11267 ax-distr 11268 ax-i2m1 11269 ax-1ne0 11270 ax-1rid 11271 ax-rnegex 11272 ax-rrecex 11273 ax-cnre 11274 ax-pre-lttri 11275 ax-pre-lttrn 11276 ax-pre-ltadd 11277 ax-pre-mulgt0 11278 ax-pre-sup 11279 ax-addf 11280 ax-mulf 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-tpos 8244 df-frecs 8300 df-wrecs 8331 df-recs 8380 df-rdg 8419 df-1o 8477 df-er 8718 df-map 8850 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-sup 9435 df-inf 9436 df-pnf 11346 df-mnf 11347 df-xr 11348 df-ltxr 11349 df-le 11350 df-sub 11544 df-neg 11545 df-div 11975 df-nn 12337 df-2 12406 df-3 12407 df-4 12408 df-5 12409 df-6 12410 df-7 12411 df-8 12412 df-9 12413 df-n0 12608 df-z 12695 df-dec 12816 df-uz 12967 df-q 13077 df-rp 13122 df-xneg 13242 df-xadd 13243 df-xmul 13244 df-fz 13641 df-seq 14146 df-exp 14206 df-cj 15267 df-re 15268 df-im 15269 df-sqrt 15403 df-abs 15404 df-struct 17326 df-sets 17343 df-slot 17361 df-ndx 17373 df-base 17389 df-ress 17410 df-plusg 17442 df-mulr 17443 df-starv 17444 df-sca 17445 df-vsca 17446 df-ip 17447 df-tset 17448 df-ple 17449 df-ds 17451 df-unif 17452 df-0g 17613 df-topgen 17615 df-mgm 18817 df-sgrp 18909 df-mnd 18925 df-mhm 18979 df-grp 19148 df-minusg 19149 df-sbg 19150 df-subg 19334 df-ghm 19429 df-cmn 19997 df-abl 19998 df-mgp 20362 df-rng 20376 df-ur 20409 df-ring 20462 df-cring 20463 df-oppr 20568 df-dvdsr 20588 df-unit 20589 df-rhm 20703 df-subrg 20823 df-drng 20983 df-staf 21097 df-srng 21098 df-lmod 21138 df-lmhm 21298 df-lvec 21379 df-sra 21449 df-rgmod 21450 df-psmet 21671 df-xmet 21672 df-met 21673 df-bl 21674 df-mopn 21675 df-cnfld 21680 df-phl 21933 df-top 23213 df-topon 23230 df-topsp 23252 df-bases 23265 df-xms 24640 df-ms 24641 df-nm 24902 df-ngp 24903 df-nlm 24906 df-clm 25385 df-cph 25490

This theorem is used by: 4cphipval2 25564 cphipval 25565

W3C validator