# Metamath Proof Explorer

## 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 ℋ$
normpar.2 ${⊢}{B}\in ℋ$
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 ℋ$
2 normpar.2 ${⊢}{B}\in ℋ$
3 1 2 hvsubcli ${⊢}{A}{-}_{ℎ}{B}\in ℋ$
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 ℋ$
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 addid1i ${⊢}\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}$