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	$$⊢V={\mathrm{Base}}_W$$
	cphpyth.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	cphpyth.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	cphpyth.n	$$⊢N=\mathrm{norm}\left(W\right)$$
	cphpyth.w	$$⊢\phi \to W\in \mathrm{CPreHil}$$
	cphpyth.a	$$⊢\phi \to A\in V$$
	cphpyth.b	$$⊢\phi \to B\in V$$
Assertion	cphpyth	$$⊢\left(\phi \wedge A\underset{\dot{}}{,}B=0\right)\to {N\left(A\underset{\dot{}}{+}B\right)}^2={N\left(A\right)}^2+{N\left(B\right)}^2$$

Proof

Step	Hyp	Ref	Expression
1		cphpyth.v	$$⊢V={\mathrm{Base}}_W$$
2		cphpyth.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		cphpyth.p	$$⊢\underset{\dot{}}{+}={+}_W$$
4		cphpyth.n	$$⊢N=\mathrm{norm}\left(W\right)$$
5		cphpyth.w	$$⊢\phi \to W\in \mathrm{CPreHil}$$
6		cphpyth.a	$$⊢\phi \to A\in V$$
7		cphpyth.b	$$⊢\phi \to B\in V$$
8	2 1 3 5 6 7 6 7	cph2di	$$⊢\phi \to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{+}B\right)=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)+\left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)$$
9	8	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{,}B=0\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{+}B\right)=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)+\left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)$$
10		simpr	$$⊢\left(\phi \wedge A\underset{\dot{}}{,}B=0\right)\to A\underset{\dot{}}{,}B=0$$
11	2 1	cphorthcom	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to \left(A\underset{\dot{}}{,}B=0\leftrightarrow B\underset{\dot{}}{,}A=0\right)$$
12	5 6 7 11	syl3anc	$$⊢\phi \to \left(A\underset{\dot{}}{,}B=0\leftrightarrow B\underset{\dot{}}{,}A=0\right)$$
13	12	biimpa	$$⊢\left(\phi \wedge A\underset{\dot{}}{,}B=0\right)\to B\underset{\dot{}}{,}A=0$$
14	10 13	oveq12d	$$⊢\left(\phi \wedge A\underset{\dot{}}{,}B=0\right)\to \left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)=0+0$$
15		00id	$$⊢0+0=0$$
16	14 15	eqtrdi	$$⊢\left(\phi \wedge A\underset{\dot{}}{,}B=0\right)\to \left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)=0$$
17	16	oveq2d	$$⊢\left(\phi \wedge A\underset{\dot{}}{,}B=0\right)\to \left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)+\left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)+0$$
18	1 2	cphipcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge A\in V\right)\to A\underset{\dot{}}{,}A\in ℂ$$
19	5 6 6 18	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}A\in ℂ$$
20	1 2	cphipcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge B\in V\wedge B\in V\right)\to B\underset{\dot{}}{,}B\in ℂ$$
21	5 7 7 20	syl3anc	$$⊢\phi \to B\underset{\dot{}}{,}B\in ℂ$$
22	19 21	addcld	$$⊢\phi \to \left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)\in ℂ$$
23	22	addridd	$$⊢\phi \to \left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)+0=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)$$
24	23	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{,}B=0\right)\to \left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)+0=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)$$
25	9 17 24	3eqtrd	$$⊢\left(\phi \wedge A\underset{\dot{}}{,}B=0\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{+}B\right)=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)$$
26		cphngp	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{NrmGrp}$$
27		ngpgrp	$$⊢W\in \mathrm{NrmGrp}\to W\in \mathrm{Grp}$$
28	5 26 27	3syl	$$⊢\phi \to W\in \mathrm{Grp}$$
29	1 3 28 6 7	grpcld	$$⊢\phi \to A\underset{\dot{}}{+}B\in V$$
30	1 2 4	nmsq	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\underset{\dot{}}{+}B\in V\right)\to {N\left(A\underset{\dot{}}{+}B\right)}^2=\left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{+}B\right)$$
31	5 29 30	syl2anc	$$⊢\phi \to {N\left(A\underset{\dot{}}{+}B\right)}^2=\left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{+}B\right)$$
32	31	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{,}B=0\right)\to {N\left(A\underset{\dot{}}{+}B\right)}^2=\left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{+}B\right)$$
33	1 2 4	nmsq	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to {N\left(A\right)}^2=A\underset{\dot{}}{,}A$$
34	5 6 33	syl2anc	$$⊢\phi \to {N\left(A\right)}^2=A\underset{\dot{}}{,}A$$
35	1 2 4	nmsq	$$⊢\left(W\in \mathrm{CPreHil}\wedge B\in V\right)\to {N\left(B\right)}^2=B\underset{\dot{}}{,}B$$
36	5 7 35	syl2anc	$$⊢\phi \to {N\left(B\right)}^2=B\underset{\dot{}}{,}B$$
37	34 36	oveq12d	$$⊢\phi \to {N\left(A\right)}^2+{N\left(B\right)}^2=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)$$
38	37	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{,}B=0\right)\to {N\left(A\right)}^2+{N\left(B\right)}^2=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)$$
39	25 32 38	3eqtr4d	$$⊢\left(\phi \wedge A\underset{\dot{}}{,}B=0\right)\to {N\left(A\underset{\dot{}}{+}B\right)}^2={N\left(A\right)}^2+{N\left(B\right)}^2$$