Database
BASIC ALGEBRAIC STRUCTURES
Rings
Unital rings
ringsubdi
Metamath Proof Explorer
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