ringi

Description: Properties of a unital ring. (Contributed by NM, 26-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	ringi.b	$⊢ B = {Base}_{R}$
	ringi.p	$⊢ \underset{˙}{+} = +_{R}$
	ringi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	ringi	$⊢ (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))$

Proof

Step	Hyp	Ref	Expression
1		ringi.b	$⊢ B = {Base}_{R}$
2		ringi.p	$⊢ \underset{˙}{+} = +_{R}$
3		ringi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5	1 4 2 3	isring	$⊢ R \in Ring \leftrightarrow (R \in Grp \land {mulGrp}_{R} \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (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)))$
6	5	simp3bi	$⊢ R \in Ring \to \forall x \in B \forall y \in B \forall z \in B (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))$
7	6	adantr	$⊢ (R \in Ring \land (x \in B \land y \in B \land z \in B)) \to \forall x \in B \forall y \in B \forall z \in B (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))$
8		simpr1	$⊢ (R \in Ring \land (x \in B \land y \in B \land z \in B)) \to x \in B$
9		rsp	$⊢ \forall x \in B \forall y \in B \forall z \in B (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)) \to (x \in B \to \forall y \in B \forall z \in B (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)))$
10	7 8 9	sylc	$⊢ (R \in Ring \land (x \in B \land y \in B \land z \in B)) \to \forall y \in B \forall z \in B (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))$
11		simpr2	$⊢ (R \in Ring \land (x \in B \land y \in B \land z \in B)) \to y \in B$
12		rsp	$⊢ \forall y \in B \forall z \in B (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)) \to (y \in B \to \forall z \in B (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)))$
13	10 11 12	sylc	$⊢ (R \in Ring \land (x \in B \land y \in B \land z \in B)) \to \forall z \in B (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))$
14		simpr3	$⊢ (R \in Ring \land (x \in B \land y \in B \land z \in B)) \to z \in B$
15		rsp	$⊢ \forall z \in B (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)) \to (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)))$
16	13 14 15	sylc	$⊢ (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))$
17	16	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)$
18	17	caovdig	$⊢ (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)$
19	16	simprd	$⊢ (R \in Ring \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
20	19	caovdirg	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{+} (Y \underset{˙}{\cdot} Z)$
21	18 20	jca	$⊢ (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))$

Metamath Proof Explorer

Theorem ringi

Proof