Proof of Theorem cphipval2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) → 𝑊 ∈
ℂPreHil) | 
| 2 | 1 | 3ad2ant1 1133 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑊 ∈ ℂPreHil) | 
| 3 |  | cphngp 25208 | . . . . . . . . . . 11
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
NrmGrp) | 
| 4 | 3 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) → 𝑊 ∈ NrmGrp) | 
| 5 |  | ngpgrp 24613 | . . . . . . . . . 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 18960 | . . . . . . . . 9
⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 + 𝐵) ∈ 𝑋) | 
| 10 | 6, 9 | syl3an1 1163 | . . . . . . . 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 584 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 + 𝐵))↑2) = ((𝐴 + 𝐵) , (𝐴 + 𝐵))) | 
| 15 |  | simp2 1137 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ 𝑋) | 
| 16 |  | simp3 1138 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋) | 
| 17 | 11, 7, 8, 2, 15, 16, 15, 16 | cph2di 25242 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) , (𝐴 + 𝐵)) = (((𝐴 , 𝐴) + (𝐵 , 𝐵)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴)))) | 
| 18 | 14, 17 | eqtrd 2776 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 + 𝐵))↑2) = (((𝐴 , 𝐴) + (𝐵 , 𝐵)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴)))) | 
| 19 |  | cphipval2.m | . . . . . . . . . 10
⊢  − =
(-g‘𝑊) | 
| 20 | 7, 19 | grpsubcl 19039 | . . . . . . . . 9
⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 − 𝐵) ∈ 𝑋) | 
| 21 | 6, 20 | syl3an1 1163 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 − 𝐵) ∈ 𝑋) | 
| 22 | 7, 11, 12 | nmsq 25229 | . . . . . . . 8
⊢ ((𝑊 ∈ ℂPreHil ∧
(𝐴 − 𝐵) ∈ 𝑋) → ((𝑁‘(𝐴 − 𝐵))↑2) = ((𝐴 − 𝐵) , (𝐴 − 𝐵))) | 
| 23 | 2, 21, 22 | syl2anc 584 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 − 𝐵))↑2) = ((𝐴 − 𝐵) , (𝐴 − 𝐵))) | 
| 24 | 11, 7, 19, 2, 15, 16, 15, 16 | cph2subdi 25245 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 − 𝐵) , (𝐴 − 𝐵)) = (((𝐴 , 𝐴) + (𝐵 , 𝐵)) − ((𝐴 , 𝐵) + (𝐵 , 𝐴)))) | 
| 25 | 23, 24 | eqtrd 2776 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 − 𝐵))↑2) = (((𝐴 , 𝐴) + (𝐵 , 𝐵)) − ((𝐴 , 𝐵) + (𝐵 , 𝐴)))) | 
| 26 | 18, 25 | oveq12d 7450 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) = ((((𝐴 , 𝐴) + (𝐵 , 𝐵)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) − (((𝐴 , 𝐴) + (𝐵 , 𝐵)) − ((𝐴 , 𝐵) + (𝐵 , 𝐴))))) | 
| 27 | 7, 11 | reipcl 25232 | . . . . . . . . . 10
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝑋) → (𝐴 , 𝐴) ∈ ℝ) | 
| 28 | 27 | adantlr 715 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋) → (𝐴 , 𝐴) ∈ ℝ) | 
| 29 | 28 | recnd 11290 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋) → (𝐴 , 𝐴) ∈ ℂ) | 
| 30 | 29 | 3adant3 1132 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐴) ∈ ℂ) | 
| 31 | 7, 11 | reipcl 25232 | . . . . . . . . . 10
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐵 ∈ 𝑋) → (𝐵 , 𝐵) ∈ ℝ) | 
| 32 | 31 | adantlr 715 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐵) ∈ ℝ) | 
| 33 | 32 | recnd 11290 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐵) ∈ ℂ) | 
| 34 | 33 | 3adant2 1131 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐵) ∈ ℂ) | 
| 35 | 30, 34 | addcld 11281 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐴) + (𝐵 , 𝐵)) ∈ ℂ) | 
| 36 | 7, 11 | cphipcl 25226 | . . . . . . . 8
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) ∈ ℂ) | 
| 37 | 1, 36 | syl3an1 1163 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) ∈ ℂ) | 
| 38 | 7, 11 | cphipcl 25226 | . . . . . . . . 9
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐵 , 𝐴) ∈ ℂ) | 
| 39 | 1, 38 | syl3an1 1163 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐵 , 𝐴) ∈ ℂ) | 
| 40 | 39 | 3com23 1126 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐵 , 𝐴) ∈ ℂ) | 
| 41 | 37, 40 | addcld 11281 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐵) + (𝐵 , 𝐴)) ∈ ℂ) | 
| 42 | 35, 41, 41 | pnncand 11660 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐴) + (𝐵 , 𝐵)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) − (((𝐴 , 𝐴) + (𝐵 , 𝐵)) − ((𝐴 , 𝐵) + (𝐵 , 𝐴)))) = (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴)))) | 
| 43 | 26, 42 | eqtrd 2776 | . . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) = (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴)))) | 
| 44 | 6 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑊 ∈ Grp) | 
| 45 |  | cphlmod 25209 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
LMod) | 
| 46 | 45 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) → 𝑊 ∈ LMod) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → 𝑊 ∈ LMod) | 
| 48 |  | simplr 768 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → i ∈ 𝐾) | 
| 49 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋) | 
| 50 |  | cphipval2.f | . . . . . . . . . . . . 13
⊢ 𝐹 = (Scalar‘𝑊) | 
| 51 |  | cphipfval.s | . . . . . . . . . . . . 13
⊢  · = (
·𝑠 ‘𝑊) | 
| 52 |  | cphipval2.k | . . . . . . . . . . . . 13
⊢ 𝐾 = (Base‘𝐹) | 
| 53 | 7, 50, 51, 52 | lmodvscl 20877 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ i ∈
𝐾 ∧ 𝐵 ∈ 𝑋) → (i · 𝐵) ∈ 𝑋) | 
| 54 | 47, 48, 49, 53 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐵 ∈ 𝑋) → (i · 𝐵) ∈ 𝑋) | 
| 55 | 54 | 3adant2 1131 | . . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · 𝐵) ∈ 𝑋) | 
| 56 | 7, 8 | grpcl 18960 | . . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (i · 𝐵) ∈ 𝑋) → (𝐴 + (i · 𝐵)) ∈ 𝑋) | 
| 57 | 44, 15, 55, 56 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 + (i · 𝐵)) ∈ 𝑋) | 
| 58 | 7, 11, 12 | nmsq 25229 | . . . . . . . . 9
⊢ ((𝑊 ∈ ℂPreHil ∧
(𝐴 + (i · 𝐵)) ∈ 𝑋) → ((𝑁‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴 + (i · 𝐵)) , (𝐴 + (i · 𝐵)))) | 
| 59 | 2, 57, 58 | syl2anc 584 | . . . . . . . 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 2776 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 + (i · 𝐵)))↑2) = (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))) | 
| 62 | 7, 19 | grpsubcl 19039 | . . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (i · 𝐵) ∈ 𝑋) → (𝐴 − (i · 𝐵)) ∈ 𝑋) | 
| 63 | 44, 15, 55, 62 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 − (i · 𝐵)) ∈ 𝑋) | 
| 64 | 7, 11, 12 | nmsq 25229 | . . . . . . . . 9
⊢ ((𝑊 ∈ ℂPreHil ∧
(𝐴 − (i · 𝐵)) ∈ 𝑋) → ((𝑁‘(𝐴 − (i · 𝐵)))↑2) = ((𝐴 − (i · 𝐵)) , (𝐴 − (i · 𝐵)))) | 
| 65 | 2, 63, 64 | syl2anc 584 | . . . . . . . 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 2776 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴 − (i · 𝐵)))↑2) = (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))) | 
| 68 | 61, 67 | oveq12d 7450 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)) = ((((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) − (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))))) | 
| 69 | 68 | oveq2d 7448 | . . . . 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 1372 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · 𝐵) , (i · 𝐵)) ∈ ℂ) | 
| 72 | 30, 71 | addcld 11281 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) ∈ ℂ) | 
| 73 | 7, 11 | cphipcl 25226 | . . . . . . . . 9
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝑋 ∧ (i · 𝐵) ∈ 𝑋) → (𝐴 , (i · 𝐵)) ∈ ℂ) | 
| 74 | 2, 15, 55, 73 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , (i · 𝐵)) ∈ ℂ) | 
| 75 | 7, 11 | cphipcl 25226 | . . . . . . . . 9
⊢ ((𝑊 ∈ ℂPreHil ∧ (i
·
𝐵) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((i · 𝐵) , 𝐴) ∈ ℂ) | 
| 76 | 2, 55, 15, 75 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · 𝐵) , 𝐴) ∈ ℂ) | 
| 77 | 74, 76 | addcld 11281 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) ∈ ℂ) | 
| 78 | 72, 77, 77 | pnncand 11660 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) − (((𝐴 , 𝐴) + ((i · 𝐵) , (i · 𝐵))) − ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))) = (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))) | 
| 79 | 78 | oveq2d 7448 | . . . . 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 7450 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) = ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) | 
| 83 | 82, 82 | oveq12d 7450 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴))) = (((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))) + ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))) | 
| 84 | 83 | oveq2d 7448 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))) = (i · (((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))) + ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))))) | 
| 85 |  | ax-icn 11215 | . . . . . . . 8
⊢ i ∈
ℂ | 
| 86 | 85 | a1i 11 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → i ∈ ℂ) | 
| 87 |  | negicn 11510 | . . . . . . . . . 10
⊢ -i ∈
ℂ | 
| 88 | 87 | a1i 11 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → -i ∈ ℂ) | 
| 89 | 88, 37 | mulcld 11282 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (-i · (𝐴 , 𝐵)) ∈ ℂ) | 
| 90 | 86, 40 | mulcld 11282 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (𝐵 , 𝐴)) ∈ ℂ) | 
| 91 | 89, 90 | addcld 11281 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))) ∈ ℂ) | 
| 92 | 86, 91, 91 | adddid 11286 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))) + ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))) = ((i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) + (i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))))) | 
| 93 | 86, 89, 90 | adddid 11286 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) = ((i · (-i · (𝐴 , 𝐵))) + (i · (i · (𝐵 , 𝐴))))) | 
| 94 | 86, 88, 37 | mulassd 11285 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · -i) · (𝐴 , 𝐵)) = (i · (-i · (𝐴 , 𝐵)))) | 
| 95 | 85, 85 | mulneg2i 11711 | . . . . . . . . . . . . 13
⊢ (i
· -i) = -(i · i) | 
| 96 |  | ixi 11893 | . . . . . . . . . . . . . 14
⊢ (i
· i) = -1 | 
| 97 | 96 | negeqi 11502 | . . . . . . . . . . . . 13
⊢ -(i
· i) = --1 | 
| 98 |  | negneg1e1 12385 | . . . . . . . . . . . . 13
⊢ --1 =
1 | 
| 99 | 95, 97, 98 | 3eqtri 2768 | . . . . . . . . . . . 12
⊢ (i
· -i) = 1 | 
| 100 | 99 | oveq1i 7442 | . . . . . . . . . . 11
⊢ ((i
· -i) · (𝐴
, 𝐵)) = (1 · (𝐴 , 𝐵)) | 
| 101 | 94, 100 | eqtr3di 2791 | . . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (-i · (𝐴 , 𝐵))) = (1 · (𝐴 , 𝐵))) | 
| 102 | 86, 86, 40 | mulassd 11285 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · i) · (𝐵 , 𝐴)) = (i · (i · (𝐵 , 𝐴)))) | 
| 103 | 96 | oveq1i 7442 | . . . . . . . . . . 11
⊢ ((i
· i) · (𝐵
, 𝐴)) = (-1 · (𝐵 , 𝐴)) | 
| 104 | 102, 103 | eqtr3di 2791 | . . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (i · (𝐵 , 𝐴))) = (-1 · (𝐵 , 𝐴))) | 
| 105 | 101, 104 | oveq12d 7450 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · (-i · (𝐴 , 𝐵))) + (i · (i · (𝐵 , 𝐴)))) = ((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴)))) | 
| 106 | 93, 105 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) = ((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴)))) | 
| 107 | 106, 106 | oveq12d 7450 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) + (i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))) = (((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴))) + ((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴))))) | 
| 108 | 37 | mullidd 11280 | . . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (1 · (𝐴 , 𝐵)) = (𝐴 , 𝐵)) | 
| 109 | 108 | oveq1d 7447 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴))) = ((𝐴 , 𝐵) + (-1 · (𝐵 , 𝐴)))) | 
| 110 |  | addneg1mul 11706 | . . . . . . . . . 10
⊢ (((𝐴 , 𝐵) ∈ ℂ ∧ (𝐵 , 𝐴) ∈ ℂ) → ((𝐴 , 𝐵) + (-1 · (𝐵 , 𝐴))) = ((𝐴 , 𝐵) − (𝐵 , 𝐴))) | 
| 111 | 37, 40, 110 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐵) + (-1 · (𝐵 , 𝐴))) = ((𝐴 , 𝐵) − (𝐵 , 𝐴))) | 
| 112 | 109, 111 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴))) = ((𝐴 , 𝐵) − (𝐵 , 𝐴))) | 
| 113 | 112, 112 | oveq12d 7450 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴))) + ((1 · (𝐴 , 𝐵)) + (-1 · (𝐵 , 𝐴)))) = (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) | 
| 114 | 107, 113 | eqtrd 2776 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴)))) + (i · ((-i · (𝐴 , 𝐵)) + (i · (𝐵 , 𝐴))))) = (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) | 
| 115 | 84, 92, 114 | 3eqtrd 2780 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)) + ((𝐴 , (i · 𝐵)) + ((i · 𝐵) , 𝐴)))) = (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) | 
| 116 | 69, 79, 115 | 3eqtrd 2780 | . . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2))) = (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) | 
| 117 | 43, 116 | oveq12d 7450 | . . 3
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) = ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))))) | 
| 118 | 117 | oveq1d 7447 | . 2
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) / 4) = (((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) / 4)) | 
| 119 | 37, 40 | subcld 11621 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐵) − (𝐵 , 𝐴)) ∈ ℂ) | 
| 120 | 41, 41, 119, 119 | add4d 11491 | . . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) = ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))) + (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))))) | 
| 121 | 37, 40, 37 | ppncand 11661 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))) = ((𝐴 , 𝐵) + (𝐴 , 𝐵))) | 
| 122 | 121, 121 | oveq12d 7450 | . . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴))) + (((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) = (((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵)))) | 
| 123 | 120, 122 | eqtrd 2776 | . . 3
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) = (((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵)))) | 
| 124 | 123 | oveq1d 7447 | . 2
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((((𝐴 , 𝐵) + (𝐵 , 𝐴)) + ((𝐴 , 𝐵) + (𝐵 , 𝐴))) + (((𝐴 , 𝐵) − (𝐵 , 𝐴)) + ((𝐴 , 𝐵) − (𝐵 , 𝐴)))) / 4) = ((((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) / 4)) | 
| 125 | 37 | 2timesd 12511 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (2 · (𝐴 , 𝐵)) = ((𝐴 , 𝐵) + (𝐴 , 𝐵))) | 
| 126 | 125 | eqcomd 2742 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 , 𝐵) + (𝐴 , 𝐵)) = (2 · (𝐴 , 𝐵))) | 
| 127 | 126, 126 | oveq12d 7450 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) = ((2 · (𝐴 , 𝐵)) + (2 · (𝐴 , 𝐵)))) | 
| 128 |  | 2cnd 12345 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 2 ∈ ℂ) | 
| 129 | 128, 128,
37 | adddird 11287 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((2 + 2) · (𝐴 , 𝐵)) = ((2 · (𝐴 , 𝐵)) + (2 · (𝐴 , 𝐵)))) | 
| 130 |  | 2p2e4 12402 | . . . . . . 7
⊢ (2 + 2) =
4 | 
| 131 | 130 | a1i 11 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (2 + 2) = 4) | 
| 132 | 131 | oveq1d 7447 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((2 + 2) · (𝐴 , 𝐵)) = (4 · (𝐴 , 𝐵))) | 
| 133 | 127, 129,
132 | 3eqtr2d 2782 | . . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) = (4 · (𝐴 , 𝐵))) | 
| 134 | 133 | oveq1d 7447 | . . 3
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) / 4) = ((4 · (𝐴 , 𝐵)) / 4)) | 
| 135 |  | 4cn 12352 | . . . . 5
⊢ 4 ∈
ℂ | 
| 136 | 135 | a1i 11 | . . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 4 ∈ ℂ) | 
| 137 |  | 4ne0 12375 | . . . . 5
⊢ 4 ≠
0 | 
| 138 | 137 | a1i 11 | . . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 4 ≠ 0) | 
| 139 | 37, 136, 138 | divcan3d 12049 | . . 3
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((4 · (𝐴 , 𝐵)) / 4) = (𝐴 , 𝐵)) | 
| 140 | 134, 139 | eqtrd 2776 | . 2
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝐴 , 𝐵) + (𝐴 , 𝐵)) + ((𝐴 , 𝐵) + (𝐴 , 𝐵))) / 4) = (𝐴 , 𝐵)) | 
| 141 | 118, 124,
140 | 3eqtrrd 2781 | 1
⊢ (((𝑊 ∈ ℂPreHil ∧ i
∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) = (((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) /
4)) |