Metamath Proof Explorer


Theorem hvdistr1i

Description: Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvdistr1.1 โŠข ๐ด โˆˆ โ„‚
hvdistr1.2 โŠข ๐ต โˆˆ โ„‹
hvdistr1.3 โŠข ๐ถ โˆˆ โ„‹
Assertion hvdistr1i ( ๐ด ยทโ„Ž ( ๐ต +โ„Ž ๐ถ ) ) = ( ( ๐ด ยทโ„Ž ๐ต ) +โ„Ž ( ๐ด ยทโ„Ž ๐ถ ) )

Proof

Step Hyp Ref Expression
1 hvdistr1.1 โŠข ๐ด โˆˆ โ„‚
2 hvdistr1.2 โŠข ๐ต โˆˆ โ„‹
3 hvdistr1.3 โŠข ๐ถ โˆˆ โ„‹
4 ax-hvdistr1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ( ๐ต +โ„Ž ๐ถ ) ) = ( ( ๐ด ยทโ„Ž ๐ต ) +โ„Ž ( ๐ด ยทโ„Ž ๐ถ ) ) )
5 1 2 3 4 mp3an โŠข ( ๐ด ยทโ„Ž ( ๐ต +โ„Ž ๐ถ ) ) = ( ( ๐ด ยทโ„Ž ๐ต ) +โ„Ž ( ๐ด ยทโ„Ž ๐ถ ) )