Metamath Proof Explorer

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

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 1 2 3 4 5 6 7 8 cphipval2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , 𝐵 ) = ( ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
10 9 oveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 4 · ( 𝐴 , 𝐵 ) ) = ( 4 · ( ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) )
11 7 8 cphsubrg ⊢ ( 𝑊 ∈ ℂPreHil → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
12 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
13 12 subrgss ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ⊆ ℂ )
14 11 13 syl ⊢ ( 𝑊 ∈ ℂPreHil → 𝐾 ⊆ ℂ )
15 14 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) → 𝐾 ⊆ ℂ )
16 15 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐾 ⊆ ℂ )
17 simp1l ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑊 ∈ ℂPreHil )
18 cphngp ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp )
19 ngpgrp ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ Grp )
20 18 19 syl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ Grp )
21 20 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) → 𝑊 ∈ Grp )
22 1 2 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + 𝐵 ) ∈ 𝑋 )
23 21 22 syl3an1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + 𝐵 ) ∈ 𝑋 )
24 1 5 4 7 8 cphnmcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ∈ 𝐾 )
25 17 23 24 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ∈ 𝐾 )
26 16 25 sseldd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ∈ ℂ )
27 26 sqcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ∈ ℂ )
28 1 6 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 − 𝐵 ) ∈ 𝑋 )
29 21 28 syl3an1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 − 𝐵 ) ∈ 𝑋 )
30 1 5 4 7 8 cphnmcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 − 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ∈ 𝐾 )
31 17 29 30 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ∈ 𝐾 )
32 16 31 sseldd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ∈ ℂ )
33 32 sqcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ∈ ℂ )
34 27 33 subcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) ∈ ℂ )
35 ax-icn ⊢ i ∈ ℂ
36 35 a1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → i ∈ ℂ )
37 17 20 syl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑊 ∈ Grp )
38 simp2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
39 cphlmod ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod )
40 39 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) → 𝑊 ∈ LMod )
41 40 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑊 ∈ LMod )
42 simp1r ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → i ∈ 𝐾 )
43 simp3 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
44 1 7 3 8 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ) → ( i · 𝐵 ) ∈ 𝑋 )
45 41 42 43 44 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · 𝐵 ) ∈ 𝑋 )
46 1 2 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( i · 𝐵 ) ∈ 𝑋 ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑋 )
47 37 38 45 46 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑋 )
48 1 5 4 7 8 cphnmcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ 𝐾 )
49 17 47 48 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ 𝐾 )
50 16 49 sseldd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℂ )
51 50 sqcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
52 1 6 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( i · 𝐵 ) ∈ 𝑋 ) → ( 𝐴 − ( i · 𝐵 ) ) ∈ 𝑋 )
53 37 38 45 52 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 − ( i · 𝐵 ) ) ∈ 𝑋 )
54 1 5 4 7 8 cphnmcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 − ( i · 𝐵 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ∈ 𝐾 )
55 17 53 54 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ∈ 𝐾 )
56 16 55 sseldd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ∈ ℂ )
57 56 sqcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
58 51 57 subcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
59 36 58 mulcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ∈ ℂ )
60 34 59 addcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) ∈ ℂ )
61 4cn ⊢ 4 ∈ ℂ
62 61 a1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 4 ∈ ℂ )
63 4ne0 ⊢ 4 ≠ 0
64 63 a1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 4 ≠ 0 )
65 60 62 64 divcan2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 4 · ( ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) = ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) )
66 10 65 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 4 · ( 𝐴 , 𝐵 ) ) = ( ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 − ( i · 𝐵 ) ) ) ↑ 2 ) ) ) ) )