Metamath Proof Explorer

Theorem nmparlem

Description: Lemma for nmpar . (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses nmpar.v 
|- V = ( Base ` W )
nmpar.p 
|- .+ = ( +g ` W )
nmpar.m 
|- .- = ( -g ` W )
nmpar.n 
|- N = ( norm ` W )
nmpar.h 
|- ., = ( .i ` W )
nmpar.f 
|- F = ( Scalar ` W )
nmpar.k 
|- K = ( Base ` F )
nmpar.1 
|- ( ph -> W e. CPreHil )
nmpar.2 
|- ( ph -> A e. V )
nmpar.3 
|- ( ph -> B e. V )
Assertion nmparlem 
|- ( ph -> ( ( ( N ` ( A .+ B ) ) ^ 2 ) + ( ( N ` ( A .- B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 nmpar.v 
 |-  V = ( Base ` W )
2 nmpar.p 
 |-  .+ = ( +g ` W )
3 nmpar.m 
 |-  .- = ( -g ` W )
4 nmpar.n 
 |-  N = ( norm ` W )
5 nmpar.h 
 |-  ., = ( .i ` W )
6 nmpar.f 
 |-  F = ( Scalar ` W )
7 nmpar.k 
 |-  K = ( Base ` F )
8 nmpar.1 
 |-  ( ph -> W e. CPreHil )
9 nmpar.2 
 |-  ( ph -> A e. V )
10 nmpar.3 
 |-  ( ph -> B e. V )
11 5 1 2 8 9 10 9 10 cph2di 
 |-  ( ph -> ( ( A .+ B ) ., ( A .+ B ) ) = ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., B ) + ( B ., A ) ) ) )
12 5 1 3 8 9 10 9 10 cph2subdi 
 |-  ( ph -> ( ( A .- B ) ., ( A .- B ) ) = ( ( ( A ., A ) + ( B ., B ) ) - ( ( A ., B ) + ( B ., A ) ) ) )
13 11 12 oveq12d 
 |-  ( ph -> ( ( ( A .+ B ) ., ( A .+ B ) ) + ( ( A .- B ) ., ( A .- B ) ) ) = ( ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., B ) + ( B ., A ) ) ) + ( ( ( A ., A ) + ( B ., B ) ) - ( ( A ., B ) + ( B ., A ) ) ) ) )
14 cphclm 
 |-  ( W e. CPreHil -> W e. CMod )
15 8 14 syl 
 |-  ( ph -> W e. CMod )
16 6 7 clmsscn 
 |-  ( W e. CMod -> K C_ CC )
17 15 16 syl 
 |-  ( ph -> K C_ CC )
18 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
19 8 18 syl 
 |-  ( ph -> W e. PreHil )
20 6 5 1 7 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ A e. V ) -> ( A ., A ) e. K )
21 19 9 9 20 syl3anc 
 |-  ( ph -> ( A ., A ) e. K )
22 6 5 1 7 ipcl 
 |-  ( ( W e. PreHil /\ B e. V /\ B e. V ) -> ( B ., B ) e. K )
23 19 10 10 22 syl3anc 
 |-  ( ph -> ( B ., B ) e. K )
24 6 7 clmacl 
 |-  ( ( W e. CMod /\ ( A ., A ) e. K /\ ( B ., B ) e. K ) -> ( ( A ., A ) + ( B ., B ) ) e. K )
25 15 21 23 24 syl3anc 
 |-  ( ph -> ( ( A ., A ) + ( B ., B ) ) e. K )
26 17 25 sseldd 
 |-  ( ph -> ( ( A ., A ) + ( B ., B ) ) e. CC )
27 6 5 1 7 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. K )
28 19 9 10 27 syl3anc 
 |-  ( ph -> ( A ., B ) e. K )
29 6 5 1 7 ipcl 
 |-  ( ( W e. PreHil /\ B e. V /\ A e. V ) -> ( B ., A ) e. K )
30 19 10 9 29 syl3anc 
 |-  ( ph -> ( B ., A ) e. K )
31 6 7 clmacl 
 |-  ( ( W e. CMod /\ ( A ., B ) e. K /\ ( B ., A ) e. K ) -> ( ( A ., B ) + ( B ., A ) ) e. K )
32 15 28 30 31 syl3anc 
 |-  ( ph -> ( ( A ., B ) + ( B ., A ) ) e. K )
33 17 32 sseldd 
 |-  ( ph -> ( ( A ., B ) + ( B ., A ) ) e. CC )
34 26 33 26 ppncand 
 |-  ( ph -> ( ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., B ) + ( B ., A ) ) ) + ( ( ( A ., A ) + ( B ., B ) ) - ( ( A ., B ) + ( B ., A ) ) ) ) = ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., A ) + ( B ., B ) ) ) )
35 13 34 eqtrd 
 |-  ( ph -> ( ( ( A .+ B ) ., ( A .+ B ) ) + ( ( A .- B ) ., ( A .- B ) ) ) = ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., A ) + ( B ., B ) ) ) )
36 cphlmod 
 |-  ( W e. CPreHil -> W e. LMod )
37 8 36 syl 
 |-  ( ph -> W e. LMod )
38 1 2 lmodvacl 
 |-  ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( A .+ B ) e. V )
39 37 9 10 38 syl3anc 
 |-  ( ph -> ( A .+ B ) e. V )
40 1 5 4 nmsq 
 |-  ( ( W e. CPreHil /\ ( A .+ B ) e. V ) -> ( ( N ` ( A .+ B ) ) ^ 2 ) = ( ( A .+ B ) ., ( A .+ B ) ) )
41 8 39 40 syl2anc 
 |-  ( ph -> ( ( N ` ( A .+ B ) ) ^ 2 ) = ( ( A .+ B ) ., ( A .+ B ) ) )
42 1 3 lmodvsubcl 
 |-  ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( A .- B ) e. V )
43 37 9 10 42 syl3anc 
 |-  ( ph -> ( A .- B ) e. V )
44 1 5 4 nmsq 
 |-  ( ( W e. CPreHil /\ ( A .- B ) e. V ) -> ( ( N ` ( A .- B ) ) ^ 2 ) = ( ( A .- B ) ., ( A .- B ) ) )
45 8 43 44 syl2anc 
 |-  ( ph -> ( ( N ` ( A .- B ) ) ^ 2 ) = ( ( A .- B ) ., ( A .- B ) ) )
46 41 45 oveq12d 
 |-  ( ph -> ( ( ( N ` ( A .+ B ) ) ^ 2 ) + ( ( N ` ( A .- B ) ) ^ 2 ) ) = ( ( ( A .+ B ) ., ( A .+ B ) ) + ( ( A .- B ) ., ( A .- B ) ) ) )
47 1 5 4 nmsq 
 |-  ( ( W e. CPreHil /\ A e. V ) -> ( ( N ` A ) ^ 2 ) = ( A ., A ) )
48 8 9 47 syl2anc 
 |-  ( ph -> ( ( N ` A ) ^ 2 ) = ( A ., A ) )
49 1 5 4 nmsq 
 |-  ( ( W e. CPreHil /\ B e. V ) -> ( ( N ` B ) ^ 2 ) = ( B ., B ) )
50 8 10 49 syl2anc 
 |-  ( ph -> ( ( N ` B ) ^ 2 ) = ( B ., B ) )
51 48 50 oveq12d 
 |-  ( ph -> ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) = ( ( A ., A ) + ( B ., B ) ) )
52 51 oveq2d 
 |-  ( ph -> ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) = ( 2 x. ( ( A ., A ) + ( B ., B ) ) ) )
53 26 2timesd 
 |-  ( ph -> ( 2 x. ( ( A ., A ) + ( B ., B ) ) ) = ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., A ) + ( B ., B ) ) ) )
54 52 53 eqtrd 
 |-  ( ph -> ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) = ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., A ) + ( B ., B ) ) ) )
55 35 46 54 3eqtr4d 
 |-  ( ph -> ( ( ( N ` ( A .+ B ) ) ^ 2 ) + ( ( N ` ( A .- B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )