# 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. This is Metamath 100 proof #4. (Contributed by NM, 17-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses pyth.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
pyth.2 ${⊢}{G}={+}_{v}\left({U}\right)$
pyth.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
pyth.7 ${⊢}{P}={\cdot }_{\mathrm{𝑖OLD}}\left({U}\right)$
pythi.u ${⊢}{U}\in {CPreHil}_{\mathrm{OLD}}$
pythi.a ${⊢}{A}\in {X}$
pythi.b ${⊢}{B}\in {X}$
Assertion pythi ${⊢}{A}{P}{B}=0\to {{N}\left({A}{G}{B}\right)}^{2}={{N}\left({A}\right)}^{2}+{{N}\left({B}\right)}^{2}$

### Proof

Step Hyp Ref Expression
1 pyth.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 pyth.2 ${⊢}{G}={+}_{v}\left({U}\right)$
3 pyth.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
4 pyth.7 ${⊢}{P}={\cdot }_{\mathrm{𝑖OLD}}\left({U}\right)$
5 pythi.u ${⊢}{U}\in {CPreHil}_{\mathrm{OLD}}$
6 pythi.a ${⊢}{A}\in {X}$
7 pythi.b ${⊢}{B}\in {X}$
8 1 2 4 5 6 7 6 7 ip2dii ${⊢}\left({A}{G}{B}\right){P}\left({A}{G}{B}\right)=\left({A}{P}{A}\right)+\left({B}{P}{B}\right)+\left({A}{P}{B}\right)+\left({B}{P}{A}\right)$
9 id ${⊢}{A}{P}{B}=0\to {A}{P}{B}=0$
10 5 phnvi ${⊢}{U}\in \mathrm{NrmCVec}$
11 1 4 diporthcom ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left({A}{P}{B}=0↔{B}{P}{A}=0\right)$
12 10 6 7 11 mp3an ${⊢}{A}{P}{B}=0↔{B}{P}{A}=0$
13 12 biimpi ${⊢}{A}{P}{B}=0\to {B}{P}{A}=0$
14 9 13 oveq12d ${⊢}{A}{P}{B}=0\to \left({A}{P}{B}\right)+\left({B}{P}{A}\right)=0+0$
15 00id ${⊢}0+0=0$
16 14 15 syl6eq ${⊢}{A}{P}{B}=0\to \left({A}{P}{B}\right)+\left({B}{P}{A}\right)=0$
17 16 oveq2d ${⊢}{A}{P}{B}=0\to \left({A}{P}{A}\right)+\left({B}{P}{B}\right)+\left({A}{P}{B}\right)+\left({B}{P}{A}\right)=\left({A}{P}{A}\right)+\left({B}{P}{B}\right)+0$
18 1 4 dipcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {A}\in {X}\right)\to {A}{P}{A}\in ℂ$
19 10 6 6 18 mp3an ${⊢}{A}{P}{A}\in ℂ$
20 1 4 dipcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}\in {X}\wedge {B}\in {X}\right)\to {B}{P}{B}\in ℂ$
21 10 7 7 20 mp3an ${⊢}{B}{P}{B}\in ℂ$
22 19 21 addcli ${⊢}\left({A}{P}{A}\right)+\left({B}{P}{B}\right)\in ℂ$
23 22 addid1i ${⊢}\left({A}{P}{A}\right)+\left({B}{P}{B}\right)+0=\left({A}{P}{A}\right)+\left({B}{P}{B}\right)$
24 17 23 syl6eq ${⊢}{A}{P}{B}=0\to \left({A}{P}{A}\right)+\left({B}{P}{B}\right)+\left({A}{P}{B}\right)+\left({B}{P}{A}\right)=\left({A}{P}{A}\right)+\left({B}{P}{B}\right)$
25 8 24 syl5eq ${⊢}{A}{P}{B}=0\to \left({A}{G}{B}\right){P}\left({A}{G}{B}\right)=\left({A}{P}{A}\right)+\left({B}{P}{B}\right)$
26 1 2 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}\in {X}$
27 10 6 7 26 mp3an ${⊢}{A}{G}{B}\in {X}$
28 1 3 4 ipidsq ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}{G}{B}\in {X}\right)\to \left({A}{G}{B}\right){P}\left({A}{G}{B}\right)={{N}\left({A}{G}{B}\right)}^{2}$
29 10 27 28 mp2an ${⊢}\left({A}{G}{B}\right){P}\left({A}{G}{B}\right)={{N}\left({A}{G}{B}\right)}^{2}$
30 1 3 4 ipidsq ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\right)\to {A}{P}{A}={{N}\left({A}\right)}^{2}$
31 10 6 30 mp2an ${⊢}{A}{P}{A}={{N}\left({A}\right)}^{2}$
32 1 3 4 ipidsq ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}\in {X}\right)\to {B}{P}{B}={{N}\left({B}\right)}^{2}$
33 10 7 32 mp2an ${⊢}{B}{P}{B}={{N}\left({B}\right)}^{2}$
34 31 33 oveq12i ${⊢}\left({A}{P}{A}\right)+\left({B}{P}{B}\right)={{N}\left({A}\right)}^{2}+{{N}\left({B}\right)}^{2}$
35 25 29 34 3eqtr3g ${⊢}{A}{P}{B}=0\to {{N}\left({A}{G}{B}\right)}^{2}={{N}\left({A}\right)}^{2}+{{N}\left({B}\right)}^{2}$