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	addid1d	⊢ ( 𝜑 → ( ( ( 𝐴 , 𝐴 ) + ( 𝐵 , 𝐵 ) ) + 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 ) ) )