# Metamath Proof Explorer

## Theorem normpar

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

Ref Expression
Assertion normpar ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {{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 fvoveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}{-}_{ℎ}{B}\right)={norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)$
2 1 oveq1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {{norm}_{ℎ}\left({A}{-}_{ℎ}{B}\right)}^{2}={{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)}^{2}$
3 fvoveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}{+}_{ℎ}{B}\right)={norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)$
4 3 oveq1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {{norm}_{ℎ}\left({A}{+}_{ℎ}{B}\right)}^{2}={{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)}^{2}$
5 2 4 oveq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {{norm}_{ℎ}\left({A}{-}_{ℎ}{B}\right)}^{2}+{{norm}_{ℎ}\left({A}{+}_{ℎ}{B}\right)}^{2}={{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)}^{2}+{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)}^{2}$
6 fveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}\right)={norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
7 6 oveq1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {{norm}_{ℎ}\left({A}\right)}^{2}={{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)}^{2}$
8 7 oveq2d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to 2{{norm}_{ℎ}\left({A}\right)}^{2}=2{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)}^{2}$
9 8 oveq1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to 2{{norm}_{ℎ}\left({A}\right)}^{2}+2{{norm}_{ℎ}\left({B}\right)}^{2}=2{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)}^{2}+2{{norm}_{ℎ}\left({B}\right)}^{2}$
10 5 9 eqeq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({{norm}_{ℎ}\left({A}{-}_{ℎ}{B}\right)}^{2}+{{norm}_{ℎ}\left({A}{+}_{ℎ}{B}\right)}^{2}=2{{norm}_{ℎ}\left({A}\right)}^{2}+2{{norm}_{ℎ}\left({B}\right)}^{2}↔{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)}^{2}+{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)}^{2}=2{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)}^{2}+2{{norm}_{ℎ}\left({B}\right)}^{2}\right)$
11 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
12 11 fveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)={norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
13 12 oveq1d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)}^{2}={{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}$
14 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
15 14 fveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)={norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
16 15 oveq1d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)}^{2}={{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}$
17 13 16 oveq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)}^{2}+{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)}^{2}={{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}+{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}$
18 fveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {norm}_{ℎ}\left({B}\right)={norm}_{ℎ}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
19 18 oveq1d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {{norm}_{ℎ}\left({B}\right)}^{2}={{norm}_{ℎ}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}$
20 19 oveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to 2{{norm}_{ℎ}\left({B}\right)}^{2}=2{{norm}_{ℎ}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}$
21 20 oveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to 2{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)}^{2}+2{{norm}_{ℎ}\left({B}\right)}^{2}=2{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)}^{2}+2{{norm}_{ℎ}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}$
22 17 21 eqeq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left({{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)}^{2}+{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)}^{2}=2{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)}^{2}+2{{norm}_{ℎ}\left({B}\right)}^{2}↔{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}+{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}=2{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)}^{2}+2{{norm}_{ℎ}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}\right)$
23 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
24 ifhvhv0 ${⊢}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\in ℋ$
25 23 24 normpari ${⊢}{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}+{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}=2{{norm}_{ℎ}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)}^{2}+2{{norm}_{ℎ}\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)}^{2}$
26 10 22 25 dedth2h ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {{norm}_{ℎ}\left({A}{-}_{ℎ}{B}\right)}^{2}+{{norm}_{ℎ}\left({A}{+}_{ℎ}{B}\right)}^{2}=2{{norm}_{ℎ}\left({A}\right)}^{2}+2{{norm}_{ℎ}\left({B}\right)}^{2}$