Metamath Proof Explorer


Theorem subdir

Description: Distribution of multiplication over subtraction. Theorem I.5 of Apostol p. 18. (Contributed by NM, 30-Dec-2005)

Ref Expression
Assertion subdir ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ( ๐ด โˆ’ ๐ต ) ยท ๐ถ ) = ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ๐ถ ) ) )

Proof

Step Hyp Ref Expression
1 subdi โŠข ( ( ๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ๐ถ ยท ( ๐ด โˆ’ ๐ต ) ) = ( ( ๐ถ ยท ๐ด ) โˆ’ ( ๐ถ ยท ๐ต ) ) )
2 1 3coml โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ๐ถ ยท ( ๐ด โˆ’ ๐ต ) ) = ( ( ๐ถ ยท ๐ด ) โˆ’ ( ๐ถ ยท ๐ต ) ) )
3 subcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ๐ด โˆ’ ๐ต ) โˆˆ โ„‚ )
4 mulcom โŠข ( ( ( ๐ด โˆ’ ๐ต ) โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ( ๐ด โˆ’ ๐ต ) ยท ๐ถ ) = ( ๐ถ ยท ( ๐ด โˆ’ ๐ต ) ) )
5 3 4 stoic3 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ( ๐ด โˆ’ ๐ต ) ยท ๐ถ ) = ( ๐ถ ยท ( ๐ด โˆ’ ๐ต ) ) )
6 mulcom โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ๐ด ยท ๐ถ ) = ( ๐ถ ยท ๐ด ) )
7 6 3adant2 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ๐ด ยท ๐ถ ) = ( ๐ถ ยท ๐ด ) )
8 mulcom โŠข ( ( ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ๐ต ยท ๐ถ ) = ( ๐ถ ยท ๐ต ) )
9 8 3adant1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ๐ต ยท ๐ถ ) = ( ๐ถ ยท ๐ต ) )
10 7 9 oveq12d โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ๐ถ ) ) = ( ( ๐ถ ยท ๐ด ) โˆ’ ( ๐ถ ยท ๐ต ) ) )
11 2 5 10 3eqtr4d โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ( ๐ด โˆ’ ๐ต ) ยท ๐ถ ) = ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ๐ถ ) ) )