Metamath Proof Explorer

Theorem hiassdi

Description: Distributive/associative law for inner product, useful for linearity proofs. (Contributed by NM, 10-May-2005) (New usage is discouraged.)

Ref Expression
Assertion hiassdi ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โˆง ( ๐ถ โˆˆ โ„‹ โˆง ๐ท โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐ด ยทโ„Ž ๐ต ) +โ„Ž ๐ถ ) ยทih ๐ท ) = ( ( ๐ด ยท ( ๐ต ยทih ๐ท ) ) + ( ๐ถ ยทih ๐ท ) ) )

Proof

Step Hyp Ref Expression
1 hvmulcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ๐ต ) โˆˆ โ„‹ )
2 ax-his2 โŠข ( ( ( ๐ด ยทโ„Ž ๐ต ) โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹ โˆง ๐ท โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด ยทโ„Ž ๐ต ) +โ„Ž ๐ถ ) ยทih ๐ท ) = ( ( ( ๐ด ยทโ„Ž ๐ต ) ยทih ๐ท ) + ( ๐ถ ยทih ๐ท ) ) )
3 2 3expb โŠข ( ( ( ๐ด ยทโ„Ž ๐ต ) โˆˆ โ„‹ โˆง ( ๐ถ โˆˆ โ„‹ โˆง ๐ท โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐ด ยทโ„Ž ๐ต ) +โ„Ž ๐ถ ) ยทih ๐ท ) = ( ( ( ๐ด ยทโ„Ž ๐ต ) ยทih ๐ท ) + ( ๐ถ ยทih ๐ท ) ) )
4 1 3 sylan โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โˆง ( ๐ถ โˆˆ โ„‹ โˆง ๐ท โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐ด ยทโ„Ž ๐ต ) +โ„Ž ๐ถ ) ยทih ๐ท ) = ( ( ( ๐ด ยทโ„Ž ๐ต ) ยทih ๐ท ) + ( ๐ถ ยทih ๐ท ) ) )
5 ax-his3 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ท โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทโ„Ž ๐ต ) ยทih ๐ท ) = ( ๐ด ยท ( ๐ต ยทih ๐ท ) ) )
6 5 3expa โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โˆง ๐ท โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทโ„Ž ๐ต ) ยทih ๐ท ) = ( ๐ด ยท ( ๐ต ยทih ๐ท ) ) )
7 6 adantrl โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โˆง ( ๐ถ โˆˆ โ„‹ โˆง ๐ท โˆˆ โ„‹ ) ) โ†’ ( ( ๐ด ยทโ„Ž ๐ต ) ยทih ๐ท ) = ( ๐ด ยท ( ๐ต ยทih ๐ท ) ) )
8 7 oveq1d โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โˆง ( ๐ถ โˆˆ โ„‹ โˆง ๐ท โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐ด ยทโ„Ž ๐ต ) ยทih ๐ท ) + ( ๐ถ ยทih ๐ท ) ) = ( ( ๐ด ยท ( ๐ต ยทih ๐ท ) ) + ( ๐ถ ยทih ๐ท ) ) )
9 4 8 eqtrd โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โˆง ( ๐ถ โˆˆ โ„‹ โˆง ๐ท โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐ด ยทโ„Ž ๐ต ) +โ„Ž ๐ถ ) ยทih ๐ท ) = ( ( ๐ด ยท ( ๐ต ยทih ๐ท ) ) + ( ๐ถ ยทih ๐ท ) ) )