Description: The parallelogram law satisfied by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hlpar2.1 | |- X = ( BaseSet ` U ) |
|
| hlpar2.2 | |- G = ( +v ` U ) |
||
| hlpar2.3 | |- M = ( -v ` U ) |
||
| hlpar2.6 | |- N = ( normCV ` U ) |
||
| Assertion | hlpar2 | |- ( ( U e. CHilOLD /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A M B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hlpar2.1 | |- X = ( BaseSet ` U ) |
|
| 2 | hlpar2.2 | |- G = ( +v ` U ) |
|
| 3 | hlpar2.3 | |- M = ( -v ` U ) |
|
| 4 | hlpar2.6 | |- N = ( normCV ` U ) |
|
| 5 | hlph | |- ( U e. CHilOLD -> U e. CPreHilOLD ) |
|
| 6 | 1 2 3 4 | phpar2 | |- ( ( U e. CPreHilOLD /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A M B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) ) |
| 7 | 5 6 | syl3an1 | |- ( ( U e. CHilOLD /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A M B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) ) |