Metamath Proof Explorer

Theorem pythi

Description: The Pythagorean theorem for an arbitrary complex inner product (pre-Hilbert) space U . 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. (Contributed by NM, 17-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses pyth.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
pyth.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
pyth.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
pyth.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
pythi.u ⊢ 𝑈 ∈ CPreHilOLD
pythi.a ⊢ 𝐴 ∈ 𝑋
pythi.b ⊢ 𝐵 ∈ 𝑋
Assertion pythi ( ( 𝐴 𝑃 𝐵 ) = 0 → ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) = ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 pyth.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 pyth.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 pyth.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
4 pyth.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
5 pythi.u ⊢ 𝑈 ∈ CPreHilOLD
6 pythi.a ⊢ 𝐴 ∈ 𝑋
7 pythi.b ⊢ 𝐵 ∈ 𝑋
8 1 2 4 5 6 7 6 7 ip2dii ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝑃 ( 𝐴 𝐺 𝐵 ) ) = ( ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) ) + ( ( 𝐴 𝑃 𝐵 ) + ( 𝐵 𝑃 𝐴 ) ) )
9 id ⊢ ( ( 𝐴 𝑃 𝐵 ) = 0 → ( 𝐴 𝑃 𝐵 ) = 0 )
10 5 phnvi ⊢ 𝑈 ∈ NrmCVec
11 1 4 diporthcom ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑃 𝐵 ) = 0 ↔ ( 𝐵 𝑃 𝐴 ) = 0 ) )
12 10 6 7 11 mp3an ⊢ ( ( 𝐴 𝑃 𝐵 ) = 0 ↔ ( 𝐵 𝑃 𝐴 ) = 0 )
13 12 biimpi ⊢ ( ( 𝐴 𝑃 𝐵 ) = 0 → ( 𝐵 𝑃 𝐴 ) = 0 )
14 9 13 oveq12d ⊢ ( ( 𝐴 𝑃 𝐵 ) = 0 → ( ( 𝐴 𝑃 𝐵 ) + ( 𝐵 𝑃 𝐴 ) ) = ( 0 + 0 ) )
15 00id ⊢ ( 0 + 0 ) = 0
16 14 15 eqtrdi ⊢ ( ( 𝐴 𝑃 𝐵 ) = 0 → ( ( 𝐴 𝑃 𝐵 ) + ( 𝐵 𝑃 𝐴 ) ) = 0 )
17 16 oveq2d ⊢ ( ( 𝐴 𝑃 𝐵 ) = 0 → ( ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) ) + ( ( 𝐴 𝑃 𝐵 ) + ( 𝐵 𝑃 𝐴 ) ) ) = ( ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) ) + 0 ) )
18 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐴 ) ∈ ℂ )
19 10 6 6 18 mp3an ⊢ ( 𝐴 𝑃 𝐴 ) ∈ ℂ
20 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝑃 𝐵 ) ∈ ℂ )
21 10 7 7 20 mp3an ⊢ ( 𝐵 𝑃 𝐵 ) ∈ ℂ
22 19 21 addcli ⊢ ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) ) ∈ ℂ
23 22 addid1i ⊢ ( ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) ) + 0 ) = ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) )
24 17 23 eqtrdi ⊢ ( ( 𝐴 𝑃 𝐵 ) = 0 → ( ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) ) + ( ( 𝐴 𝑃 𝐵 ) + ( 𝐵 𝑃 𝐴 ) ) ) = ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) ) )
25 8 24 syl5eq ⊢ ( ( 𝐴 𝑃 𝐵 ) = 0 → ( ( 𝐴 𝐺 𝐵 ) 𝑃 ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) ) )
26 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
27 10 6 7 26 mp3an ⊢ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋
28 1 3 4 ipidsq ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) )
29 10 27 28 mp2an ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝑃 ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 )
30 1 3 4 ipidsq ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐴 ) = ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) )
31 10 6 30 mp2an ⊢ ( 𝐴 𝑃 𝐴 ) = ( ( 𝑁 ‘ 𝐴 ) ↑ 2 )
32 1 3 4 ipidsq ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝑃 𝐵 ) = ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) )
33 10 7 32 mp2an ⊢ ( 𝐵 𝑃 𝐵 ) = ( ( 𝑁 ‘ 𝐵 ) ↑ 2 )
34 31 33 oveq12i ⊢ ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) ) = ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) )
35 25 29 34 3eqtr3g ⊢ ( ( 𝐴 𝑃 𝐵 ) = 0 → ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) = ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )