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	addridi	⊢ ( ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) ) + 0 ) = ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) )
24	17 23	eqtrdi	⊢ ( ( 𝐴 𝑃 𝐵 ) = 0 → ( ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) ) + ( ( 𝐴 𝑃 𝐵 ) + ( 𝐵 𝑃 𝐴 ) ) ) = ( ( 𝐴 𝑃 𝐴 ) + ( 𝐵 𝑃 𝐵 ) ) )
25	8 24	eqtrid	⊢ ( ( 𝐴 𝑃 𝐵 ) = 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 ) ) )