rngdir

Description: Distributive law for the multiplication operation of a non-unital ring (right-distributivity). (Contributed by AV, 17-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		rngdi.b	$⊢ B = {Base}_{R}$
2		rngdi.p	$⊢ \underset{˙}{+} = +_{R}$
3		rngdi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5	1 4 2 3	isrng	$⊢ R \in Rng \leftrightarrow (R \in Abel \land {mulGrp}_{R} \in Smgrp \land \forall a \in B \forall b \in B \forall c \in B (a \underset{˙}{\cdot} (b \underset{˙}{+} c) = (a \underset{˙}{\cdot} b) \underset{˙}{+} (a \underset{˙}{\cdot} c) \land (a \underset{˙}{+} b) \underset{˙}{\cdot} c = (a \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c)))$
6		oveq1	$⊢ a = X \to a \underset{˙}{\cdot} (b \underset{˙}{+} c) = X \underset{˙}{\cdot} (b \underset{˙}{+} c)$
7		oveq1	$⊢ a = X \to a \underset{˙}{\cdot} b = X \underset{˙}{\cdot} b$
8		oveq1	$⊢ a = X \to a \underset{˙}{\cdot} c = X \underset{˙}{\cdot} c$
9	7 8	oveq12d	$⊢ a = X \to (a \underset{˙}{\cdot} b) \underset{˙}{+} (a \underset{˙}{\cdot} c) = (X \underset{˙}{\cdot} b) \underset{˙}{+} (X \underset{˙}{\cdot} c)$
10	6 9	eqeq12d	$⊢ a = X \to (a \underset{˙}{\cdot} (b \underset{˙}{+} c) = (a \underset{˙}{\cdot} b) \underset{˙}{+} (a \underset{˙}{\cdot} c) \leftrightarrow X \underset{˙}{\cdot} (b \underset{˙}{+} c) = (X \underset{˙}{\cdot} b) \underset{˙}{+} (X \underset{˙}{\cdot} c))$
11		oveq1	$⊢ a = X \to a \underset{˙}{+} b = X \underset{˙}{+} b$
12	11	oveq1d	$⊢ a = X \to (a \underset{˙}{+} b) \underset{˙}{\cdot} c = (X \underset{˙}{+} b) \underset{˙}{\cdot} c$
13	8	oveq1d	$⊢ a = X \to (a \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c) = (X \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c)$
14	12 13	eqeq12d	$⊢ a = X \to ((a \underset{˙}{+} b) \underset{˙}{\cdot} c = (a \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c) \leftrightarrow (X \underset{˙}{+} b) \underset{˙}{\cdot} c = (X \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c))$
15	10 14	anbi12d	$⊢ a = X \to ((a \underset{˙}{\cdot} (b \underset{˙}{+} c) = (a \underset{˙}{\cdot} b) \underset{˙}{+} (a \underset{˙}{\cdot} c) \land (a \underset{˙}{+} b) \underset{˙}{\cdot} c = (a \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c)) \leftrightarrow (X \underset{˙}{\cdot} (b \underset{˙}{+} c) = (X \underset{˙}{\cdot} b) \underset{˙}{+} (X \underset{˙}{\cdot} c) \land (X \underset{˙}{+} b) \underset{˙}{\cdot} c = (X \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c)))$
16		oveq1	$⊢ b = Y \to b \underset{˙}{+} c = Y \underset{˙}{+} c$
17	16	oveq2d	$⊢ b = Y \to X \underset{˙}{\cdot} (b \underset{˙}{+} c) = X \underset{˙}{\cdot} (Y \underset{˙}{+} c)$
18		oveq2	$⊢ b = Y \to X \underset{˙}{\cdot} b = X \underset{˙}{\cdot} Y$
19	18	oveq1d	$⊢ b = Y \to (X \underset{˙}{\cdot} b) \underset{˙}{+} (X \underset{˙}{\cdot} c) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} c)$
20	17 19	eqeq12d	$⊢ b = Y \to (X \underset{˙}{\cdot} (b \underset{˙}{+} c) = (X \underset{˙}{\cdot} b) \underset{˙}{+} (X \underset{˙}{\cdot} c) \leftrightarrow X \underset{˙}{\cdot} (Y \underset{˙}{+} c) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} c))$
21		oveq2	$⊢ b = Y \to X \underset{˙}{+} b = X \underset{˙}{+} Y$
22	21	oveq1d	$⊢ b = Y \to (X \underset{˙}{+} b) \underset{˙}{\cdot} c = (X \underset{˙}{+} Y) \underset{˙}{\cdot} c$
23		oveq1	$⊢ b = Y \to b \underset{˙}{\cdot} c = Y \underset{˙}{\cdot} c$
24	23	oveq2d	$⊢ b = Y \to (X \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c) = (X \underset{˙}{\cdot} c) \underset{˙}{+} (Y \underset{˙}{\cdot} c)$
25	22 24	eqeq12d	$⊢ b = Y \to ((X \underset{˙}{+} b) \underset{˙}{\cdot} c = (X \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c) \leftrightarrow (X \underset{˙}{+} Y) \underset{˙}{\cdot} c = (X \underset{˙}{\cdot} c) \underset{˙}{+} (Y \underset{˙}{\cdot} c))$
26	20 25	anbi12d	$⊢ b = Y \to ((X \underset{˙}{\cdot} (b \underset{˙}{+} c) = (X \underset{˙}{\cdot} b) \underset{˙}{+} (X \underset{˙}{\cdot} c) \land (X \underset{˙}{+} b) \underset{˙}{\cdot} c = (X \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c)) \leftrightarrow (X \underset{˙}{\cdot} (Y \underset{˙}{+} c) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} c) \land (X \underset{˙}{+} Y) \underset{˙}{\cdot} c = (X \underset{˙}{\cdot} c) \underset{˙}{+} (Y \underset{˙}{\cdot} c)))$
27		oveq2	$⊢ c = Z \to Y \underset{˙}{+} c = Y \underset{˙}{+} Z$
28	27	oveq2d	$⊢ c = Z \to X \underset{˙}{\cdot} (Y \underset{˙}{+} c) = X \underset{˙}{\cdot} (Y \underset{˙}{+} Z)$
29		oveq2	$⊢ c = Z \to X \underset{˙}{\cdot} c = X \underset{˙}{\cdot} Z$
30	29	oveq2d	$⊢ c = Z \to (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} c) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} Z)$
31	28 30	eqeq12d	$⊢ c = Z \to (X \underset{˙}{\cdot} (Y \underset{˙}{+} c) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} c) \leftrightarrow X \underset{˙}{\cdot} (Y \underset{˙}{+} Z) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} Z))$
32		oveq2	$⊢ c = Z \to (X \underset{˙}{+} Y) \underset{˙}{\cdot} c = (X \underset{˙}{+} Y) \underset{˙}{\cdot} Z$
33		oveq2	$⊢ c = Z \to Y \underset{˙}{\cdot} c = Y \underset{˙}{\cdot} Z$
34	29 33	oveq12d	$⊢ c = Z \to (X \underset{˙}{\cdot} c) \underset{˙}{+} (Y \underset{˙}{\cdot} c) = (X \underset{˙}{\cdot} Z) \underset{˙}{+} (Y \underset{˙}{\cdot} Z)$
35	32 34	eqeq12d	$⊢ c = Z \to ((X \underset{˙}{+} Y) \underset{˙}{\cdot} c = (X \underset{˙}{\cdot} c) \underset{˙}{+} (Y \underset{˙}{\cdot} c) \leftrightarrow (X \underset{˙}{+} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{+} (Y \underset{˙}{\cdot} Z))$
36	31 35	anbi12d	$⊢ c = Z \to ((X \underset{˙}{\cdot} (Y \underset{˙}{+} c) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} c) \land (X \underset{˙}{+} Y) \underset{˙}{\cdot} c = (X \underset{˙}{\cdot} c) \underset{˙}{+} (Y \underset{˙}{\cdot} c)) \leftrightarrow (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)))$
37	15 26 36	rspc3v	$⊢ (X \in B \land Y \in B \land Z \in B) \to (\forall a \in B \forall b \in B \forall c \in B (a \underset{˙}{\cdot} (b \underset{˙}{+} c) = (a \underset{˙}{\cdot} b) \underset{˙}{+} (a \underset{˙}{\cdot} c) \land (a \underset{˙}{+} b) \underset{˙}{\cdot} c = (a \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c)) \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)))$
38		simpr	$⊢ (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 \underset{˙}{+} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{+} (Y \underset{˙}{\cdot} Z)$
39	37 38	syl6com	$⊢ \forall a \in B \forall b \in B \forall c \in B (a \underset{˙}{\cdot} (b \underset{˙}{+} c) = (a \underset{˙}{\cdot} b) \underset{˙}{+} (a \underset{˙}{\cdot} c) \land (a \underset{˙}{+} b) \underset{˙}{\cdot} c = (a \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c)) \to ((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))$
40	39	3ad2ant3	$⊢ (R \in Abel \land {mulGrp}_{R} \in Smgrp \land \forall a \in B \forall b \in B \forall c \in B (a \underset{˙}{\cdot} (b \underset{˙}{+} c) = (a \underset{˙}{\cdot} b) \underset{˙}{+} (a \underset{˙}{\cdot} c) \land (a \underset{˙}{+} b) \underset{˙}{\cdot} c = (a \underset{˙}{\cdot} c) \underset{˙}{+} (b \underset{˙}{\cdot} c))) \to ((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))$
41	5 40	sylbi	$⊢ R \in Rng \to ((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))$
42	41	imp	$⊢ (R \in Rng \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)$

Metamath Proof Explorer

Theorem rngdir

Proof