Metamath Proof Explorer

Theorem cphpyth

Description: The pythagorean theorem for a subcomplex pre-Hilbert space. The square of the norm of the sum of two orthogonal vectors (i.e., whose inner product is 0) is the sum of the squares of their norms. Problem 2 in Kreyszig p. 135. This is Metamath 100 proof #4. (Contributed by NM, 17-Apr-2008) (Revised by SN, 22-Sep-2024)

Ref Expression
Hypotheses cphpyth.v 
|- V = ( Base ` W )
cphpyth.h 
|- ., = ( .i ` W )
cphpyth.p 
|- .+ = ( +g ` W )
cphpyth.n 
|- N = ( norm ` W )
cphpyth.w 
|- ( ph -> W e. CPreHil )
cphpyth.a 
|- ( ph -> A e. V )
cphpyth.b 
|- ( ph -> B e. V )
Assertion cphpyth 
|- ( ( ph /\ ( A ., B ) = 0 ) -> ( ( N ` ( A .+ B ) ) ^ 2 ) = ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 cphpyth.v 
 |-  V = ( Base ` W )
2 cphpyth.h 
 |-  ., = ( .i ` W )
3 cphpyth.p 
 |-  .+ = ( +g ` W )
4 cphpyth.n 
 |-  N = ( norm ` W )
5 cphpyth.w 
 |-  ( ph -> W e. CPreHil )
6 cphpyth.a 
 |-  ( ph -> A e. V )
7 cphpyth.b 
 |-  ( ph -> B e. V )
8 2 1 3 5 6 7 6 7 cph2di 
 |-  ( ph -> ( ( A .+ B ) ., ( A .+ B ) ) = ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., B ) + ( B ., A ) ) ) )
9 8 adantr 
 |-  ( ( ph /\ ( A ., B ) = 0 ) -> ( ( A .+ B ) ., ( A .+ B ) ) = ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., B ) + ( B ., A ) ) ) )
10 simpr 
 |-  ( ( ph /\ ( A ., B ) = 0 ) -> ( A ., B ) = 0 )
11 2 1 cphorthcom 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( A ., B ) = 0 <-> ( B ., A ) = 0 ) )
12 5 6 7 11 syl3anc 
 |-  ( ph -> ( ( A ., B ) = 0 <-> ( B ., A ) = 0 ) )
13 12 biimpa 
 |-  ( ( ph /\ ( A ., B ) = 0 ) -> ( B ., A ) = 0 )
14 10 13 oveq12d 
 |-  ( ( ph /\ ( A ., B ) = 0 ) -> ( ( A ., B ) + ( B ., A ) ) = ( 0 + 0 ) )
15 00id 
 |-  ( 0 + 0 ) = 0
16 14 15 eqtrdi 
 |-  ( ( ph /\ ( A ., B ) = 0 ) -> ( ( A ., B ) + ( B ., A ) ) = 0 )
17 16 oveq2d 
 |-  ( ( ph /\ ( A ., B ) = 0 ) -> ( ( ( A ., A ) + ( B ., B ) ) + ( ( A ., B ) + ( B ., A ) ) ) = ( ( ( A ., A ) + ( B ., B ) ) + 0 ) )
18 1 2 cphipcl 
 |-  ( ( W e. CPreHil /\ A e. V /\ A e. V ) -> ( A ., A ) e. CC )
19 5 6 6 18 syl3anc 
 |-  ( ph -> ( A ., A ) e. CC )
20 1 2 cphipcl 
 |-  ( ( W e. CPreHil /\ B e. V /\ B e. V ) -> ( B ., B ) e. CC )
21 5 7 7 20 syl3anc 
 |-  ( ph -> ( B ., B ) e. CC )
22 19 21 addcld 
 |-  ( ph -> ( ( A ., A ) + ( B ., B ) ) e. CC )
23 22 addid1d 
 |-  ( ph -> ( ( ( A ., A ) + ( B ., B ) ) + 0 ) = ( ( A ., A ) + ( B ., B ) ) )
24 23 adantr 
 |-  ( ( ph /\ ( A ., B ) = 0 ) -> ( ( ( A ., A ) + ( B ., B ) ) + 0 ) = ( ( A ., A ) + ( B ., B ) ) )
25 9 17 24 3eqtrd 
 |-  ( ( ph /\ ( A ., B ) = 0 ) -> ( ( A .+ B ) ., ( A .+ B ) ) = ( ( A ., A ) + ( B ., B ) ) )
26 cphngp 
 |-  ( W e. CPreHil -> W e. NrmGrp )
27 ngpgrp 
 |-  ( W e. NrmGrp -> W e. Grp )
28 5 26 27 3syl 
 |-  ( ph -> W e. Grp )
29 1 3 28 6 7 grpcld 
 |-  ( ph -> ( A .+ B ) e. V )
30 1 2 4 nmsq 
 |-  ( ( W e. CPreHil /\ ( A .+ B ) e. V ) -> ( ( N ` ( A .+ B ) ) ^ 2 ) = ( ( A .+ B ) ., ( A .+ B ) ) )
31 5 29 30 syl2anc 
 |-  ( ph -> ( ( N ` ( A .+ B ) ) ^ 2 ) = ( ( A .+ B ) ., ( A .+ B ) ) )
32 31 adantr 
 |-  ( ( ph /\ ( A ., B ) = 0 ) -> ( ( N ` ( A .+ B ) ) ^ 2 ) = ( ( A .+ B ) ., ( A .+ B ) ) )
33 1 2 4 nmsq 
 |-  ( ( W e. CPreHil /\ A e. V ) -> ( ( N ` A ) ^ 2 ) = ( A ., A ) )
34 5 6 33 syl2anc 
 |-  ( ph -> ( ( N ` A ) ^ 2 ) = ( A ., A ) )
35 1 2 4 nmsq 
 |-  ( ( W e. CPreHil /\ B e. V ) -> ( ( N ` B ) ^ 2 ) = ( B ., B ) )
36 5 7 35 syl2anc 
 |-  ( ph -> ( ( N ` B ) ^ 2 ) = ( B ., B ) )
37 34 36 oveq12d 
 |-  ( ph -> ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) = ( ( A ., A ) + ( B ., B ) ) )
38 37 adantr 
 |-  ( ( ph /\ ( A ., B ) = 0 ) -> ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) = ( ( A ., A ) + ( B ., B ) ) )
39 25 32 38 3eqtr4d 
 |-  ( ( ph /\ ( A ., B ) = 0 ) -> ( ( N ` ( A .+ B ) ) ^ 2 ) = ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) )