Metamath Proof Explorer


Theorem ringsubdi

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 · ˙ = R
ringsubdi.m - ˙ = - R
ringsubdi.r φ R Ring
ringsubdi.x φ X B
ringsubdi.y φ Y B
ringsubdi.z φ Z B
Assertion ringsubdi φ X · ˙ Y - ˙ Z = X · ˙ Y - ˙ X · ˙ Z

Proof

Step Hyp Ref Expression
1 ringsubdi.b B = Base R
2 ringsubdi.t · ˙ = R
3 ringsubdi.m - ˙ = - R
4 ringsubdi.r φ R Ring
5 ringsubdi.x φ X B
6 ringsubdi.y φ Y B
7 ringsubdi.z φ Z B
8 ringrng R Ring R Rng
9 4 8 syl φ R Rng
10 1 2 3 9 5 6 7 rngsubdi φ X · ˙ Y - ˙ Z = X · ˙ Y - ˙ X · ˙ Z