This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝑋 = ( Base ‘ 𝑊 )
cphipfval.p ⊢ + = ( +g ‘ 𝑊 )
cphipfval.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
cphipfval.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
cphipfval.i ⊢ , = ( ·𝑖 ‘ 𝑊 )
cphipval2.m ⊢ − = ( -g ‘ 𝑊 )
cphipval2.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cphipval2.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion cphipval2 ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , 𝐵 ) = ( ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) )

Proof

Step Hyp Ref Expression
1 cphipfval.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
2 cphipfval.p ⊢ + = ( +g ‘ 𝑊 )
3 cphipfval.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 cphipfval.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
5 cphipfval.i ⊢ , = ( ·𝑖 ‘ 𝑊 )
6 cphipval2.m ⊢ − = ( -g ‘ 𝑊 )
7 cphipval2.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
8 cphipval2.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
9 simpl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) → 𝑊 ∈ ℂPreHil )
10 9 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑊 ∈ ℂPreHil )
11 cphngp ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp )
12 11 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) → 𝑊 ∈ NrmGrp )
13 ngpgrp ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ Grp )
14 12 13 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) → 𝑊 ∈ Grp )
15 1 2 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + 𝐵 ) ∈ 𝑋 )
16 14 15 syl3an1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + 𝐵 ) ∈ 𝑋 )
17 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + 𝐵 ) ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) )
18 10 16 17 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) )
19 simp2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
20 simp3 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
21 5 1 2 10 19 20 19 20 cph2di ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) )
22 18 21 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) )
23 1 6 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 − 𝐵 ) ∈ 𝑋 )
24 14 23 syl3an1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 − 𝐵 ) ∈ 𝑋 )
25 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 − 𝐵 ) ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 − 𝐵 ) , ( 𝐴 − 𝐵 ) ) )
26 10 24 25 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 − 𝐵 ) , ( 𝐴 − 𝐵 ) ) )
27 5 1 6 10 19 20 19 20 cph2subdi ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 − 𝐵 ) , ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) − ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) )
28 26 27 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) − ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) )
29 22 28 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) − ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) − ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) ) )
30 1 5 reipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 , 𝐴 ) ∈ ℝ )
31 30 adantlr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 , 𝐴 ) ∈ ℝ )
32 31 recnd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 , 𝐴 ) ∈ ℂ )
33 32 3adant3 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , 𝐴 ) ∈ ℂ )
34 1 5 reipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 , 𝐵 ) ∈ ℝ )
35 34 adantlr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 , 𝐵 ) ∈ ℝ )
36 35 recnd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 , 𝐵 ) ∈ ℂ )
37 36 3adant2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 , 𝐵 ) ∈ ℂ )
38 33 37 addcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) ∈ ℂ )
39 1 5 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , 𝐵 ) ∈ ℂ )
40 9 39 syl3an1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , 𝐵 ) ∈ ℂ )
41 1 5 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 , 𝐴 ) ∈ ℂ )
42 9 41 syl3an1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 , 𝐴 ) ∈ ℂ )
43 42 3com23 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 , 𝐴 ) ∈ ℂ )
44 40 43 addcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ∈ ℂ )
45 38 44 44 pnncand ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) − ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) − ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) ) = ( ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) )
46 29 45 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) )
47 14 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑊 ∈ Grp )
48 cphlmod ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod )
49 48 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) → 𝑊 ∈ LMod )
50 49 adantr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐵 ∈ 𝑋 ) → 𝑊 ∈ LMod )
51 simplr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐵 ∈ 𝑋 ) → i ∈ 𝐾 )
52 simpr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
53 1 7 3 8 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ) → ( i · 𝐵 ) ∈ 𝑋 )
54 50 51 52 53 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐵 ∈ 𝑋 ) → ( i · 𝐵 ) ∈ 𝑋 )
55 54 3adant2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · 𝐵 ) ∈ 𝑋 )
56 1 2 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( i · 𝐵 ) ∈ 𝑋 ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑋 )
57 47 19 55 56 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑋 )
58 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 + ( i · 𝐵 ) ) , ( 𝐴 + ( i · 𝐵 ) ) ) )
59 10 57 58 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 + ( i · 𝐵 ) ) , ( 𝐴 + ( i · 𝐵 ) ) ) )
60 5 1 2 10 19 55 19 55 cph2di ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 + ( i · 𝐵 ) ) , ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) + ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) )
61 59 60 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) + ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) )
62 1 6 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( i · 𝐵 ) ∈ 𝑋 ) → ( 𝐴 − ( i · 𝐵 ) ) ∈ 𝑋 )
63 47 19 55 62 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 − ( i · 𝐵 ) ) ∈ 𝑋 )
64 1 5 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 − ( i · 𝐵 ) ) ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 − ( i · 𝐵 ) ) , ( 𝐴 − ( i · 𝐵 ) ) ) )
65 10 63 64 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 − ( i · 𝐵 ) ) , ( 𝐴 − ( i · 𝐵 ) ) ) )
66 5 1 6 10 19 55 19 55 cph2subdi ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 − ( i · 𝐵 ) ) , ( 𝐴 − ( i · 𝐵 ) ) ) = ( ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) − ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) )
67 65 66 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) − ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) )
68 61 67 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) + ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) − ( ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) − ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) ) )
69 68 oveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) = ( i · ( ( ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) + ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) − ( ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) − ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) ) ) )
70 1 5 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( i · 𝐵 ) ∈ 𝑋 ∧ ( i · 𝐵 ) ∈ 𝑋 ) → ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ∈ ℂ )
71 10 55 55 70 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ∈ ℂ )
72 33 71 addcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) ∈ ℂ )
73 1 5 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑋 ∧ ( i · 𝐵 ) ∈ 𝑋 ) → ( 𝐴 , ( i · 𝐵 ) ) ∈ ℂ )
74 10 19 55 73 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , ( i · 𝐵 ) ) ∈ ℂ )
75 1 5 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( i · 𝐵 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( i · 𝐵 ) , 𝐴 ) ∈ ℂ )
76 10 55 19 75 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · 𝐵 ) , 𝐴 ) ∈ ℂ )
77 74 76 addcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ∈ ℂ )
78 72 77 77 pnncand ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) + ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) − ( ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) − ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) ) = ( ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) + ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) )
79 78 oveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) + ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) − ( ( ( 𝐴 , 𝐴 ) + ( ( i · 𝐵 ) , ( i · 𝐵 ) ) ) − ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) ) ) = ( i · ( ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) + ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) ) )
80 1 3 5 7 8 cphassir ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , ( i · 𝐵 ) ) = ( - i · ( 𝐴 , 𝐵 ) ) )
81 1 3 5 7 8 cphassi ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · 𝐵 ) , 𝐴 ) = ( i · ( 𝐵 , 𝐴 ) ) )
82 80 81 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) = ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) )
83 82 82 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) + ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) = ( ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) + ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) ) )
84 83 oveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) + ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) ) = ( i · ( ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) + ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) ) ) )
85 ax-icn ⊢ i ∈ ℂ
86 85 a1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → i ∈ ℂ )
87 negicn ⊢ - i ∈ ℂ
88 87 a1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → - i ∈ ℂ )
89 88 40 mulcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - i · ( 𝐴 , 𝐵 ) ) ∈ ℂ )
90 86 43 mulcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( 𝐵 , 𝐴 ) ) ∈ ℂ )
91 89 90 addcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) ∈ ℂ )
92 86 91 91 adddid ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) + ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) ) ) = ( ( i · ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) ) + ( i · ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) ) ) )
93 86 89 90 adddid ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) ) = ( ( i · ( - i · ( 𝐴 , 𝐵 ) ) ) + ( i · ( i · ( 𝐵 , 𝐴 ) ) ) ) )
94 86 88 40 mulassd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · - i ) · ( 𝐴 , 𝐵 ) ) = ( i · ( - i · ( 𝐴 , 𝐵 ) ) ) )
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 ) · ( 𝐴 , 𝐵 ) ) = ( 1 · ( 𝐴 , 𝐵 ) )
101 94 100 eqtr3di ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( - i · ( 𝐴 , 𝐵 ) ) ) = ( 1 · ( 𝐴 , 𝐵 ) ) )
102 86 86 43 mulassd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · i ) · ( 𝐵 , 𝐴 ) ) = ( i · ( i · ( 𝐵 , 𝐴 ) ) ) )
103 96 oveq1i ⊢ ( ( i · i ) · ( 𝐵 , 𝐴 ) ) = ( - 1 · ( 𝐵 , 𝐴 ) )
104 102 103 eqtr3di ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( i · ( 𝐵 , 𝐴 ) ) ) = ( - 1 · ( 𝐵 , 𝐴 ) ) )
105 101 104 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( - i · ( 𝐴 , 𝐵 ) ) ) + ( i · ( i · ( 𝐵 , 𝐴 ) ) ) ) = ( ( 1 · ( 𝐴 , 𝐵 ) ) + ( - 1 · ( 𝐵 , 𝐴 ) ) ) )
106 93 105 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) ) = ( ( 1 · ( 𝐴 , 𝐵 ) ) + ( - 1 · ( 𝐵 , 𝐴 ) ) ) )
107 106 106 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) ) + ( i · ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) ) ) = ( ( ( 1 · ( 𝐴 , 𝐵 ) ) + ( - 1 · ( 𝐵 , 𝐴 ) ) ) + ( ( 1 · ( 𝐴 , 𝐵 ) ) + ( - 1 · ( 𝐵 , 𝐴 ) ) ) ) )
108 40 mullidd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 · ( 𝐴 , 𝐵 ) ) = ( 𝐴 , 𝐵 ) )
109 108 oveq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 1 · ( 𝐴 , 𝐵 ) ) + ( - 1 · ( 𝐵 , 𝐴 ) ) ) = ( ( 𝐴 , 𝐵 ) + ( - 1 · ( 𝐵 , 𝐴 ) ) ) )
110 addneg1mul ⊢ ( ( ( 𝐴 , 𝐵 ) ∈ ℂ ∧ ( 𝐵 , 𝐴 ) ∈ ℂ ) → ( ( 𝐴 , 𝐵 ) + ( - 1 · ( 𝐵 , 𝐴 ) ) ) = ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) )
111 40 43 110 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 , 𝐵 ) + ( - 1 · ( 𝐵 , 𝐴 ) ) ) = ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) )
112 109 111 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 1 · ( 𝐴 , 𝐵 ) ) + ( - 1 · ( 𝐵 , 𝐴 ) ) ) = ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) )
113 112 112 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 1 · ( 𝐴 , 𝐵 ) ) + ( - 1 · ( 𝐵 , 𝐴 ) ) ) + ( ( 1 · ( 𝐴 , 𝐵 ) ) + ( - 1 · ( 𝐵 , 𝐴 ) ) ) ) = ( ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) )
114 107 113 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) ) + ( i · ( ( - i · ( 𝐴 , 𝐵 ) ) + ( i · ( 𝐵 , 𝐴 ) ) ) ) ) = ( ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) )
115 84 92 114 3eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) + ( ( 𝐴 , ( i · 𝐵 ) ) + ( ( i · 𝐵 ) , 𝐴 ) ) ) ) = ( ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) )
116 69 79 115 3eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) = ( ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) )
117 46 116 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) ) )
118 117 oveq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) = ( ( ( ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) ) / 4 ) )
119 40 43 subcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ∈ ℂ )
120 44 44 119 119 add4d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) ) = ( ( ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) ) )
121 40 43 40 ppncand ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) = ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) )
122 121 121 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) ) = ( ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) ) )
123 120 122 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) ) = ( ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) ) )
124 123 oveq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) + ( ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) + ( ( 𝐴 , 𝐵 ) − ( 𝐵 , 𝐴 ) ) ) ) / 4 ) = ( ( ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) ) / 4 ) )
125 40 2timesd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 2 · ( 𝐴 , 𝐵 ) ) = ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) )
126 125 eqcomd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) = ( 2 · ( 𝐴 , 𝐵 ) ) )
127 126 126 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) ) = ( ( 2 · ( 𝐴 , 𝐵 ) ) + ( 2 · ( 𝐴 , 𝐵 ) ) ) )
128 2cnd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 2 ∈ ℂ )
129 128 128 40 adddird ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 2 + 2 ) · ( 𝐴 , 𝐵 ) ) = ( ( 2 · ( 𝐴 , 𝐵 ) ) + ( 2 · ( 𝐴 , 𝐵 ) ) ) )
130 2p2e4 ⊢ ( 2 + 2 ) = 4
131 130 a1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 2 + 2 ) = 4 )
132 131 oveq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 2 + 2 ) · ( 𝐴 , 𝐵 ) ) = ( 4 · ( 𝐴 , 𝐵 ) ) )
133 127 129 132 3eqtr2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) ) = ( 4 · ( 𝐴 , 𝐵 ) ) )
134 133 oveq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) ) / 4 ) = ( ( 4 · ( 𝐴 , 𝐵 ) ) / 4 ) )
135 4cn ⊢ 4 ∈ ℂ
136 135 a1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 4 ∈ ℂ )
137 4ne0 ⊢ 4 ≠ 0
138 137 a1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 4 ≠ 0 )
139 40 136 138 divcan3d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 4 · ( 𝐴 , 𝐵 ) ) / 4 ) = ( 𝐴 , 𝐵 ) )
140 134 139 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐴 , 𝐵 ) ) ) / 4 ) = ( 𝐴 , 𝐵 ) )
141 118 124 140 3eqtrrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , 𝐵 ) = ( ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) )