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 
|- X = ( Base ` W )
cphipfval.p 
|- .+ = ( +g ` W )
cphipfval.s 
|- .x. = ( .s ` W )
cphipfval.n 
|- N = ( norm ` W )
cphipfval.i 
|- ., = ( .i ` W )
cphipval2.m 
|- .- = ( -g ` W )
cphipval2.f 
|- F = ( Scalar ` W )
cphipval2.k 
|- K = ( Base ` F )
Assertion 4cphipval2 
|- ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( 4 x. ( A ., B ) ) = ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cphipfval.x 
 |-  X = ( Base ` W )
2 cphipfval.p 
 |-  .+ = ( +g ` W )
3 cphipfval.s 
 |-  .x. = ( .s ` W )
4 cphipfval.n 
 |-  N = ( norm ` W )
5 cphipfval.i 
 |-  ., = ( .i ` W )
6 cphipval2.m 
 |-  .- = ( -g ` W )
7 cphipval2.f 
 |-  F = ( Scalar ` W )
8 cphipval2.k 
 |-  K = ( Base ` F )
9 1 2 3 4 5 6 7 8 cphipval2 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., B ) = ( ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) / 4 ) )
10 9 oveq2d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( 4 x. ( A ., B ) ) = ( 4 x. ( ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) / 4 ) ) )
11 7 8 cphsubrg 
 |-  ( W e. CPreHil -> K e. ( SubRing ` CCfld ) )
12 cnfldbas 
 |-  CC = ( Base ` CCfld )
13 12 subrgss 
 |-  ( K e. ( SubRing ` CCfld ) -> K C_ CC )
14 11 13 syl 
 |-  ( W e. CPreHil -> K C_ CC )
15 14 adantr 
 |-  ( ( W e. CPreHil /\ _i e. K ) -> K C_ CC )
16 15 3ad2ant1 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> K C_ CC )
17 simp1l 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> W e. CPreHil )
18 cphngp 
 |-  ( W e. CPreHil -> W e. NrmGrp )
19 ngpgrp 
 |-  ( W e. NrmGrp -> W e. Grp )
20 18 19 syl 
 |-  ( W e. CPreHil -> W e. Grp )
21 20 adantr 
 |-  ( ( W e. CPreHil /\ _i e. K ) -> W e. Grp )
22 1 2 grpcl 
 |-  ( ( W e. Grp /\ A e. X /\ B e. X ) -> ( A .+ B ) e. X )
23 21 22 syl3an1 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A .+ B ) e. X )
24 1 5 4 7 8 cphnmcl 
 |-  ( ( W e. CPreHil /\ ( A .+ B ) e. X ) -> ( N ` ( A .+ B ) ) e. K )
25 17 23 24 syl2anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( N ` ( A .+ B ) ) e. K )
26 16 25 sseldd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( N ` ( A .+ B ) ) e. CC )
27 26 sqcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( N ` ( A .+ B ) ) ^ 2 ) e. CC )
28 1 6 grpsubcl 
 |-  ( ( W e. Grp /\ A e. X /\ B e. X ) -> ( A .- B ) e. X )
29 21 28 syl3an1 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A .- B ) e. X )
30 1 5 4 7 8 cphnmcl 
 |-  ( ( W e. CPreHil /\ ( A .- B ) e. X ) -> ( N ` ( A .- B ) ) e. K )
31 17 29 30 syl2anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( N ` ( A .- B ) ) e. K )
32 16 31 sseldd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( N ` ( A .- B ) ) e. CC )
33 32 sqcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( N ` ( A .- B ) ) ^ 2 ) e. CC )
34 27 33 subcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) e. CC )
35 ax-icn 
 |-  _i e. CC
36 35 a1i 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> _i e. CC )
37 17 20 syl 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> W e. Grp )
38 simp2 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> A e. X )
39 cphlmod 
 |-  ( W e. CPreHil -> W e. LMod )
40 39 adantr 
 |-  ( ( W e. CPreHil /\ _i e. K ) -> W e. LMod )
41 40 3ad2ant1 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> W e. LMod )
42 simp1r 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> _i e. K )
43 simp3 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> B e. X )
44 1 7 3 8 lmodvscl 
 |-  ( ( W e. LMod /\ _i e. K /\ B e. X ) -> ( _i .x. B ) e. X )
45 41 42 43 44 syl3anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i .x. B ) e. X )
46 1 2 grpcl 
 |-  ( ( W e. Grp /\ A e. X /\ ( _i .x. B ) e. X ) -> ( A .+ ( _i .x. B ) ) e. X )
47 37 38 45 46 syl3anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A .+ ( _i .x. B ) ) e. X )
48 1 5 4 7 8 cphnmcl 
 |-  ( ( W e. CPreHil /\ ( A .+ ( _i .x. B ) ) e. X ) -> ( N ` ( A .+ ( _i .x. B ) ) ) e. K )
49 17 47 48 syl2anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( N ` ( A .+ ( _i .x. B ) ) ) e. K )
50 16 49 sseldd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( N ` ( A .+ ( _i .x. B ) ) ) e. CC )
51 50 sqcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) e. CC )
52 1 6 grpsubcl 
 |-  ( ( W e. Grp /\ A e. X /\ ( _i .x. B ) e. X ) -> ( A .- ( _i .x. B ) ) e. X )
53 37 38 45 52 syl3anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A .- ( _i .x. B ) ) e. X )
54 1 5 4 7 8 cphnmcl 
 |-  ( ( W e. CPreHil /\ ( A .- ( _i .x. B ) ) e. X ) -> ( N ` ( A .- ( _i .x. B ) ) ) e. K )
55 17 53 54 syl2anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( N ` ( A .- ( _i .x. B ) ) ) e. K )
56 16 55 sseldd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( N ` ( A .- ( _i .x. B ) ) ) e. CC )
57 56 sqcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) e. CC )
58 51 57 subcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) e. CC )
59 36 58 mulcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) e. CC )
60 34 59 addcld 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) e. CC )
61 4cn 
 |-  4 e. CC
62 61 a1i 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> 4 e. CC )
63 4ne0 
 |-  4 =/= 0
64 63 a1i 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> 4 =/= 0 )
65 60 62 64 divcan2d 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( 4 x. ( ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) / 4 ) ) = ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) )
66 10 65 eqtrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( 4 x. ( A ., B ) ) = ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) )