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 = BaseSet (U)$
	pyth.2	$⊢ G = +_{v} (U)$
	pyth.6	$⊢ N = {norm}_{CV} (U)$
	pyth.7	$⊢ P = \cdot_{𝑖OLD} (U)$
	pythi.u	$⊢ U \in {CPreHil}_{OLD}$
	pythi.a	$⊢ A \in X$
	pythi.b	$⊢ B \in X$
Assertion	pythi	$⊢ A P B = 0 \to {N (A G B)}^{2} = {N (A)}^{2} + {N (B)}^{2}$

Proof

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

Metamath Proof Explorer

Theorem pythi

Proof