ringdi

Description: Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007)

	Ref	Expression
Hypotheses	ringdi.b	$⊢ B = {Base}_{R}$
	ringdi.p	$⊢ \underset{˙}{+} = +_{R}$
	ringdi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	ringdi	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\cdot} (Y \underset{˙}{+} Z) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} Z)$

Step	Hyp	Ref	Expression
1		ringdi.b	$⊢ B = {Base}_{R}$
2		ringdi.p	$⊢ \underset{˙}{+} = +_{R}$
3		ringdi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4	1 2 3	ringdilem	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\cdot} (Y \underset{˙}{+} Z) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} Z) \land (X \underset{˙}{+} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{+} (Y \underset{˙}{\cdot} Z))$
5	4	simpld	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\cdot} (Y \underset{˙}{+} Z) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} Z)$

Metamath Proof Explorer