Metamath Proof Explorer

Theorem hlpar2

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 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
hlpar2.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
hlpar2.3 โŠข ๐‘€ = ( โˆ’๐‘ฃ โ€˜ ๐‘ˆ )
hlpar2.6 โŠข ๐‘ = ( normCV โ€˜ ๐‘ˆ )
Assertion hlpar2 ( ( ๐‘ˆ โˆˆ CHilOLD โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ๐ต ) ) โ†‘ 2 ) + ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ๐ต ) ) โ†‘ 2 ) ) = ( 2 ยท ( ( ( ๐‘ โ€˜ ๐ด ) โ†‘ 2 ) + ( ( ๐‘ โ€˜ ๐ต ) โ†‘ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 hlpar2.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
2 hlpar2.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
3 hlpar2.3 โŠข ๐‘€ = ( โˆ’๐‘ฃ โ€˜ ๐‘ˆ )
4 hlpar2.6 โŠข ๐‘ = ( normCV โ€˜ ๐‘ˆ )
5 hlph โŠข ( ๐‘ˆ โˆˆ CHilOLD โ†’ ๐‘ˆ โˆˆ CPreHilOLD )
6 1 2 3 4 phpar2 โŠข ( ( ๐‘ˆ โˆˆ CPreHilOLD โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ๐ต ) ) โ†‘ 2 ) + ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ๐ต ) ) โ†‘ 2 ) ) = ( 2 ยท ( ( ( ๐‘ โ€˜ ๐ด ) โ†‘ 2 ) + ( ( ๐‘ โ€˜ ๐ต ) โ†‘ 2 ) ) ) )
7 5 6 syl3an1 โŠข ( ( ๐‘ˆ โˆˆ CHilOLD โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ๐ต ) ) โ†‘ 2 ) + ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ๐ต ) ) โ†‘ 2 ) ) = ( 2 ยท ( ( ( ๐‘ โ€˜ ๐ด ) โ†‘ 2 ) + ( ( ๐‘ โ€˜ ๐ต ) โ†‘ 2 ) ) ) )