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