# 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 e. ~H`
normpar.2
`|- B e. ~H`
Assertion normpari
`|- ( ( ( normh ` ( A -h B ) ) ^ 2 ) + ( ( normh ` ( A +h B ) ) ^ 2 ) ) = ( ( 2 x. ( ( normh ` A ) ^ 2 ) ) + ( 2 x. ( ( normh ` B ) ^ 2 ) ) )`

### Proof

Step Hyp Ref Expression
1 normpar.1
` |-  A e. ~H`
2 normpar.2
` |-  B e. ~H`
3 1 2 hvsubcli
` |-  ( A -h B ) e. ~H`
4 3 normsqi
` |-  ( ( normh ` ( A -h B ) ) ^ 2 ) = ( ( A -h B ) .ih ( A -h B ) )`
` |-  ( A +h B ) e. ~H`
6 5 normsqi
` |-  ( ( normh ` ( A +h B ) ) ^ 2 ) = ( ( A +h B ) .ih ( A +h B ) )`
7 4 6 oveq12i
` |-  ( ( ( normh ` ( A -h B ) ) ^ 2 ) + ( ( normh ` ( A +h B ) ) ^ 2 ) ) = ( ( ( A -h B ) .ih ( A -h B ) ) + ( ( A +h B ) .ih ( A +h B ) ) )`
8 1 normsqi
` |-  ( ( normh ` A ) ^ 2 ) = ( A .ih A )`
9 8 oveq2i
` |-  ( 2 x. ( ( normh ` A ) ^ 2 ) ) = ( 2 x. ( A .ih A ) )`
10 1 1 hicli
` |-  ( A .ih A ) e. CC`
11 10 2timesi
` |-  ( 2 x. ( A .ih A ) ) = ( ( A .ih A ) + ( A .ih A ) )`
12 9 11 eqtri
` |-  ( 2 x. ( ( normh ` A ) ^ 2 ) ) = ( ( A .ih A ) + ( A .ih A ) )`
13 2 normsqi
` |-  ( ( normh ` B ) ^ 2 ) = ( B .ih B )`
14 13 oveq2i
` |-  ( 2 x. ( ( normh ` B ) ^ 2 ) ) = ( 2 x. ( B .ih B ) )`
15 2 2 hicli
` |-  ( B .ih B ) e. CC`
16 15 2timesi
` |-  ( 2 x. ( B .ih B ) ) = ( ( B .ih B ) + ( B .ih B ) )`
17 14 16 eqtri
` |-  ( 2 x. ( ( normh ` B ) ^ 2 ) ) = ( ( B .ih B ) + ( B .ih B ) )`
18 12 17 oveq12i
` |-  ( ( 2 x. ( ( normh ` A ) ^ 2 ) ) + ( 2 x. ( ( normh ` B ) ^ 2 ) ) ) = ( ( ( A .ih A ) + ( A .ih A ) ) + ( ( B .ih B ) + ( B .ih B ) ) )`
19 1 2 1 2 normlem9
` |-  ( ( A -h B ) .ih ( A -h B ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) - ( ( A .ih B ) + ( B .ih A ) ) )`
` |-  ( ( A .ih A ) + ( B .ih B ) ) e. CC`
21 1 2 hicli
` |-  ( A .ih B ) e. CC`
22 2 1 hicli
` |-  ( B .ih A ) e. CC`
` |-  ( ( A .ih B ) + ( B .ih A ) ) e. CC`
24 20 23 negsubi
` |-  ( ( ( A .ih A ) + ( B .ih B ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) - ( ( A .ih B ) + ( B .ih A ) ) )`
25 19 24 eqtr4i
` |-  ( ( A -h B ) .ih ( A -h B ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) )`
26 1 2 1 2 normlem8
` |-  ( ( A +h B ) .ih ( A +h B ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) )`
27 25 26 oveq12i
` |-  ( ( ( A -h B ) .ih ( A -h B ) ) + ( ( A +h B ) .ih ( A +h B ) ) ) = ( ( ( ( A .ih A ) + ( B .ih B ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) + ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) ) )`
28 23 negcli
` |-  -u ( ( A .ih B ) + ( B .ih A ) ) e. CC`
29 20 28 20 23 add42i
` |-  ( ( ( ( A .ih A ) + ( B .ih B ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) + ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) ) ) = ( ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) + ( ( ( A .ih B ) + ( B .ih A ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) )`
30 23 negidi
` |-  ( ( ( A .ih B ) + ( B .ih A ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) = 0`
31 30 oveq2i
` |-  ( ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) + ( ( ( A .ih B ) + ( B .ih A ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) ) = ( ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) + 0 )`
` |-  ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) e. CC`
` |-  ( ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) + 0 ) = ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) )`
` |-  ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) = ( ( ( A .ih A ) + ( A .ih A ) ) + ( ( B .ih B ) + ( B .ih B ) ) )`
` |-  ( ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) + ( ( ( A .ih B ) + ( B .ih A ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) ) = ( ( ( A .ih A ) + ( A .ih A ) ) + ( ( B .ih B ) + ( B .ih B ) ) )`
` |-  ( ( ( A -h B ) .ih ( A -h B ) ) + ( ( A +h B ) .ih ( A +h B ) ) ) = ( ( ( A .ih A ) + ( A .ih A ) ) + ( ( B .ih B ) + ( B .ih B ) ) )`
` |-  ( ( 2 x. ( ( normh ` A ) ^ 2 ) ) + ( 2 x. ( ( normh ` B ) ^ 2 ) ) ) = ( ( ( A -h B ) .ih ( A -h B ) ) + ( ( A +h B ) .ih ( A +h B ) ) )`
` |-  ( ( ( normh ` ( A -h B ) ) ^ 2 ) + ( ( normh ` ( A +h B ) ) ^ 2 ) ) = ( ( 2 x. ( ( normh ` A ) ^ 2 ) ) + ( 2 x. ( ( normh ` B ) ^ 2 ) ) )`