This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
cphpyth.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
cphpyth.p ⊢ + = ( +g ‘ 𝑊 )
cphpyth.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
cphpyth.w ⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
cphpyth.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
cphpyth.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
Assertion cphpyth ( ( 𝜑 ∧ ( 𝐴 , 𝐵 ) = 0 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 cphpyth.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 cphpyth.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 cphpyth.p ⊢ + = ( +g ‘ 𝑊 )
4 cphpyth.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
5 cphpyth.w ⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
6 cphpyth.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7 cphpyth.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
8 2 1 3 5 6 7 6 7 cph2di ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) )
9 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 , 𝐵 ) = 0 ) → ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) )
10 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 , 𝐵 ) = 0 ) → ( 𝐴 , 𝐵 ) = 0 )
11 2 1 cphorthcom ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 , 𝐵 ) = 0 ↔ ( 𝐵 , 𝐴 ) = 0 ) )
12 5 6 7 11 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 , 𝐵 ) = 0 ↔ ( 𝐵 , 𝐴 ) = 0 ) )
13 12 biimpa ⊢ ( ( 𝜑 ∧ ( 𝐴 , 𝐵 ) = 0 ) → ( 𝐵 , 𝐴 ) = 0 )
14 10 13 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝐴 , 𝐵 ) = 0 ) → ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) = ( 0 + 0 ) )
15 00id ⊢ ( 0 + 0 ) = 0
16 14 15 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝐴 , 𝐵 ) = 0 ) → ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) = 0 )
17 16 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 , 𝐵 ) = 0 ) → ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + ( ( 𝐴 , 𝐵 ) + ( 𝐵 , 𝐴 ) ) ) = ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + 0 ) )
18 1 2 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 , 𝐴 ) ∈ ℂ )
19 5 6 6 18 syl3anc ⊢ ( 𝜑 → ( 𝐴 , 𝐴 ) ∈ ℂ )
20 1 2 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐵 , 𝐵 ) ∈ ℂ )
21 5 7 7 20 syl3anc ⊢ ( 𝜑 → ( 𝐵 , 𝐵 ) ∈ ℂ )
22 19 21 addcld ⊢ ( 𝜑 → ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) ∈ ℂ )
23 22 addridd ⊢ ( 𝜑 → ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + 0 ) = ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 , 𝐵 ) = 0 ) → ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + 0 ) = ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) )
25 9 17 24 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 , 𝐵 ) = 0 ) → ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) = ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) )
26 cphngp ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp )
27 ngpgrp ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ Grp )
28 5 26 27 3syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
29 1 3 28 6 7 grpcld ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ 𝑉 )
30 1 2 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 + 𝐵 ) ∈ 𝑉 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) )
31 5 29 30 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 , 𝐵 ) = 0 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) , ( 𝐴 + 𝐵 ) ) )
33 1 2 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 , 𝐴 ) )
34 5 6 33 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 , 𝐴 ) )
35 1 2 4 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) = ( 𝐵 , 𝐵 ) )
36 5 7 35 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) = ( 𝐵 , 𝐵 ) )
37 34 36 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) = ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 , 𝐵 ) = 0 ) → ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) = ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) )
39 25 32 38 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝐴 , 𝐵 ) = 0 ) → ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )