This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ringsubdir

Description: Ring multiplication distributes over subtraction. ( subdir 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	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		ringsubdi.m	$⊢ \underset{˙}{-} = -_{R}$
		ringsubdi.r	$⊢ φ \to R \in Ring$
		ringsubdi.x	$⊢ φ \to X \in B$
		ringsubdi.y	$⊢ φ \to Y \in B$
		ringsubdi.z	$⊢ φ \to Z \in B$
	Assertion	ringsubdir	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{-} (Y \underset{˙}{\cdot} Z)$

Proof

Step	Hyp	Ref	Expression
1		ringsubdi.b	$⊢ B = {Base}_{R}$
2		ringsubdi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		ringsubdi.m	$⊢ \underset{˙}{-} = -_{R}$
4		ringsubdi.r	$⊢ φ \to R \in Ring$
5		ringsubdi.x	$⊢ φ \to X \in B$
6		ringsubdi.y	$⊢ φ \to Y \in B$
7		ringsubdi.z	$⊢ φ \to Z \in B$
8		ringrng	$⊢ R \in Ring \to R \in Rng$
9	4 8	syl	$⊢ φ \to R \in Rng$
10	1 2 3 9 5 6 7	rngsubdir	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{-} (Y \underset{˙}{\cdot} Z)$