Metamath Proof Explorer
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 |
โข ( ๐ด ยทโ ( ๐ต +โ ๐ถ ) ) = ( ( ๐ด ยทโ ๐ต ) +โ ( ๐ด ยทโ ๐ถ ) ) |