Description: Ring multiplication distributes over subtraction. ( subdi analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ringsubdi.b | |- B = ( Base ` R ) |
|
ringsubdi.t | |- .x. = ( .r ` R ) |
||
ringsubdi.m | |- .- = ( -g ` R ) |
||
ringsubdi.r | |- ( ph -> R e. Ring ) |
||
ringsubdi.x | |- ( ph -> X e. B ) |
||
ringsubdi.y | |- ( ph -> Y e. B ) |
||
ringsubdi.z | |- ( ph -> Z e. B ) |
||
Assertion | ringsubdi | |- ( ph -> ( X .x. ( Y .- Z ) ) = ( ( X .x. Y ) .- ( X .x. Z ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringsubdi.b | |- B = ( Base ` R ) |
|
2 | ringsubdi.t | |- .x. = ( .r ` R ) |
|
3 | ringsubdi.m | |- .- = ( -g ` R ) |
|
4 | ringsubdi.r | |- ( ph -> R e. Ring ) |
|
5 | ringsubdi.x | |- ( ph -> X e. B ) |
|
6 | ringsubdi.y | |- ( ph -> Y e. B ) |
|
7 | ringsubdi.z | |- ( ph -> Z e. B ) |
|
8 | ringrng | |- ( R e. Ring -> R e. Rng ) |
|
9 | 4 8 | syl | |- ( ph -> R e. Rng ) |
10 | 1 2 3 9 5 6 7 | rngsubdi | |- ( ph -> ( X .x. ( Y .- Z ) ) = ( ( X .x. Y ) .- ( X .x. Z ) ) ) |