Metamath Proof Explorer


Theorem hldir

Description: Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hldi.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
hldi.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
hldi.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
Assertion hldir ( ( ๐‘ˆ โˆˆ CHilOLD โˆง ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ ๐‘‹ ) ) โ†’ ( ( ๐ด + ๐ต ) ๐‘† ๐ถ ) = ( ( ๐ด ๐‘† ๐ถ ) ๐บ ( ๐ต ๐‘† ๐ถ ) ) )

Proof

Step Hyp Ref Expression
1 hldi.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
2 hldi.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
3 hldi.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
4 hlnv โŠข ( ๐‘ˆ โˆˆ CHilOLD โ†’ ๐‘ˆ โˆˆ NrmCVec )
5 1 2 3 nvdir โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ ๐‘‹ ) ) โ†’ ( ( ๐ด + ๐ต ) ๐‘† ๐ถ ) = ( ( ๐ด ๐‘† ๐ถ ) ๐บ ( ๐ต ๐‘† ๐ถ ) ) )
6 4 5 sylan โŠข ( ( ๐‘ˆ โˆˆ CHilOLD โˆง ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ ๐‘‹ ) ) โ†’ ( ( ๐ด + ๐ต ) ๐‘† ๐ถ ) = ( ( ๐ด ๐‘† ๐ถ ) ๐บ ( ๐ต ๐‘† ๐ถ ) ) )