Theorem normpari

Description: Parallelogram law for norms. Remark 3.4(B) of Beran p. 98. (Contributed by NM, 21-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	normpar.1	$$⊢A\in \mathscr{H}$$
	normpar.2	$$⊢B\in \mathscr{H}$$
Assertion	normpari	$$⊢{{norm}_{ℎ}\left(A{-}_{ℎ}B\right)}^2+{{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2=2{{norm}_{ℎ}\left(A\right)}^2+2{{norm}_{ℎ}\left(B\right)}^2$$

Proof

Step	Hyp	Ref	Expression
1		normpar.1	$$⊢A\in \mathscr{H}$$
2		normpar.2	$$⊢B\in \mathscr{H}$$
3	1 2	hvsubcli	$$⊢A{-}_{ℎ}B\in \mathscr{H}$$
4	3	normsqi	$$⊢{{norm}_{ℎ}\left(A{-}_{ℎ}B\right)}^2=\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}B\right)$$
5	1 2	hvaddcli	$$⊢A{+}_{ℎ}B\in \mathscr{H}$$
6	5	normsqi	$$⊢{{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2=\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)$$
7	4 6	oveq12i	$$⊢{{norm}_{ℎ}\left(A{-}_{ℎ}B\right)}^2+{{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2=\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}B\right)\right)+\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\right)$$
8	1	normsqi	$$⊢{{norm}_{ℎ}\left(A\right)}^2=A{\cdot }_{\mathrm{ih}}A$$
9	8	oveq2i	$$⊢2{{norm}_{ℎ}\left(A\right)}^2=2\left(A{\cdot }_{\mathrm{ih}}A\right)$$
10	1 1	hicli	$$⊢A{\cdot }_{\mathrm{ih}}A\in ℂ$$
11	10	2timesi	$$⊢2\left(A{\cdot }_{\mathrm{ih}}A\right)=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}A\right)$$
12	9 11	eqtri	$$⊢2{{norm}_{ℎ}\left(A\right)}^2=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}A\right)$$
13	2	normsqi	$$⊢{{norm}_{ℎ}\left(B\right)}^2=B{\cdot }_{\mathrm{ih}}B$$
14	13	oveq2i	$$⊢2{{norm}_{ℎ}\left(B\right)}^2=2\left(B{\cdot }_{\mathrm{ih}}B\right)$$
15	2 2	hicli	$$⊢B{\cdot }_{\mathrm{ih}}B\in ℂ$$
16	15	2timesi	$$⊢2\left(B{\cdot }_{\mathrm{ih}}B\right)=\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)$$
17	14 16	eqtri	$$⊢2{{norm}_{ℎ}\left(B\right)}^2=\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)$$
18	12 17	oveq12i	$$⊢2{{norm}_{ℎ}\left(A\right)}^2+2{{norm}_{ℎ}\left(B\right)}^2=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)$$
19	1 2 1 2	normlem9	$$⊢\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(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)$$
20	10 15	addcli	$$⊢\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\in ℂ$$
21	1 2	hicli	$$⊢A{\cdot }_{\mathrm{ih}}B\in ℂ$$
22	2 1	hicli	$$⊢B{\cdot }_{\mathrm{ih}}A\in ℂ$$
23	21 22	addcli	$$⊢\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\in ℂ$$
24	20 23	negsubi	$$⊢\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(-\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)\right)=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)-\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)$$
25	19 24	eqtr4i	$$⊢\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(-\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)\right)$$
26	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)$$
27	25 26	oveq12i	$$⊢\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}B\right)\right)+\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\right)=\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+\left(-\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)\right)+\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)$$
28	23	negcli	$$⊢-\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)\in ℂ$$
29	20 28 20 23	add42i	$$⊢\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+\left(-\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)\right)+\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)=\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)+\left(-\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)\right)$$
30	23	negidi	$$⊢\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)+\left(-\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)\right)=0$$
31	30	oveq2i	$$⊢\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)+\left(-\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)\right)=\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+0$$
32	20 20	addcli	$$⊢\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\in ℂ$$
33	32	addridi	$$⊢\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+0=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)$$
34	10 15 10 15	add4i	$$⊢\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)$$
35	31 33 34	3eqtri	$$⊢\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+\left(\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)\right)+\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)+\left(-\left(\left(A{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}A\right)\right)\right)=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)$$
36	27 29 35	3eqtri	$$⊢\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}B\right)\right)+\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\right)=\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(A{\cdot }_{\mathrm{ih}}A\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)+\left(B{\cdot }_{\mathrm{ih}}B\right)$$
37	18 36	eqtr4i	$$⊢2{{norm}_{ℎ}\left(A\right)}^2+2{{norm}_{ℎ}\left(B\right)}^2=\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}B\right)\right)+\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\right)$$
38	7 37	eqtr4i	$$⊢{{norm}_{ℎ}\left(A{-}_{ℎ}B\right)}^2+{{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2=2{{norm}_{ℎ}\left(A\right)}^2+2{{norm}_{ℎ}\left(B\right)}^2$$