Theorem normpythi

Description: Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of Beran p. 98. (Contributed by NM, 17-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	normsub.1	$$⊢A\in \mathscr{H}$$
	normsub.2	$$⊢B\in \mathscr{H}$$
Assertion	normpythi	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to {{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2={{norm}_{ℎ}\left(A\right)}^2+{{norm}_{ℎ}\left(B\right)}^2$$

Proof

Step	Hyp	Ref	Expression
1		normsub.1	$$⊢A\in \mathscr{H}$$
2		normsub.2	$$⊢B\in \mathscr{H}$$
3	1 2 1 2	normlem8	$$⊢\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)$$
4		id	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to A{\cdot }_{\mathrm{ih}}B=0$$
5		orthcom	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left(A{\cdot }_{\mathrm{ih}}B=0\leftrightarrow B{\cdot }_{\mathrm{ih}}A=0\right)$$
6	1 2 5	mp2an	$$⊢A{\cdot }_{\mathrm{ih}}B=0\leftrightarrow B{\cdot }_{\mathrm{ih}}A=0$$
7	6	biimpi	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to B{\cdot }_{\mathrm{ih}}A=0$$
8	4 7	oveq12d	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to \left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)=0+0$$
9		00id	$$⊢0+0=0$$
10	8 9	eqtrdi	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to \left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)=0$$
11	10	oveq2d	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to \left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+0$$
12	1 1	hicli	$$⊢A{\cdot }_{\mathrm{ih}}A\in ℂ$$
13	2 2	hicli	$$⊢B{\cdot }_{\mathrm{ih}}B\in ℂ$$
14	12 13	addcli	$$⊢\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\in ℂ$$
15	14	addid1i	$$⊢\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+0=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)$$
16	11 15	eqtrdi	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to \left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)$$
17	3 16	syl5eq	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to \left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)$$
18	1 2	hvaddcli	$$⊢A{+}_{ℎ}B\in \mathscr{H}$$
19	18	normsqi	$$⊢{{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2=\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)$$
20	1	normsqi	$$⊢{{norm}_{ℎ}\left(A\right)}^2=A{\cdot }_{\mathrm{ih}}A$$
21	2	normsqi	$$⊢{{norm}_{ℎ}\left(B\right)}^2=B{\cdot }_{\mathrm{ih}}B$$
22	20 21	oveq12i	$$⊢{{norm}_{ℎ}\left(A\right)}^2+{{norm}_{ℎ}\left(B\right)}^2=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)$$
23	17 19 22	3eqtr4g	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to {{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2={{norm}_{ℎ}\left(A\right)}^2+{{norm}_{ℎ}\left(B\right)}^2$$