isrng

Description: The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020)

	Ref	Expression
Hypotheses	isrng.b	$⊢ B = {Base}_{R}$
	isrng.g	$⊢ G = {mulGrp}_{R}$
	isrng.p	$⊢ \underset{˙}{+} = +_{R}$
	isrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	isrng	$⊢ R \in Rng \leftrightarrow (R \in Abel \land G \in Smgrp \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)))$

Proof

Step	Hyp	Ref	Expression
1		isrng.b	$⊢ B = {Base}_{R}$
2		isrng.g	$⊢ G = {mulGrp}_{R}$
3		isrng.p	$⊢ \underset{˙}{+} = +_{R}$
4		isrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		fveq2	$⊢ r = R \to {mulGrp}_{r} = {mulGrp}_{R}$
6	5 2	eqtr4di	$⊢ r = R \to {mulGrp}_{r} = G$
7	6	eleq1d	$⊢ r = R \to ({mulGrp}_{r} \in Smgrp \leftrightarrow G \in Smgrp)$
8		fvexd	$⊢ r = R \to {Base}_{r} \in V$
9		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
10	9 1	eqtr4di	$⊢ r = R \to {Base}_{r} = B$
11		fvexd	$⊢ (r = R \land b = B) \to +_{r} \in V$
12		fveq2	$⊢ r = R \to +_{r} = +_{R}$
13	12	adantr	$⊢ (r = R \land b = B) \to +_{r} = +_{R}$
14	13 3	eqtr4di	$⊢ (r = R \land b = B) \to +_{r} = \underset{˙}{+}$
15		fvexd	$⊢ ((r = R \land b = B) \land p = \underset{˙}{+}) \to \cdot_{r} \in V$
16		fveq2	$⊢ r = R \to \cdot_{r} = \cdot_{R}$
17	16	adantr	$⊢ (r = R \land b = B) \to \cdot_{r} = \cdot_{R}$
18	17	adantr	$⊢ ((r = R \land b = B) \land p = \underset{˙}{+}) \to \cdot_{r} = \cdot_{R}$
19	18 4	eqtr4di	$⊢ ((r = R \land b = B) \land p = \underset{˙}{+}) \to \cdot_{r} = \underset{˙}{\cdot}$
20		simpllr	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to b = B$
21		simpr	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to t = \underset{˙}{\cdot}$
22		eqidd	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to x = x$
23		oveq	$⊢ p = \underset{˙}{+} \to y p z = y \underset{˙}{+} z$
24	23	ad2antlr	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to y p z = y \underset{˙}{+} z$
25	21 22 24	oveq123d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to x t (y p z) = x \underset{˙}{\cdot} (y \underset{˙}{+} z)$
26		simpr	$⊢ ((r = R \land b = B) \land p = \underset{˙}{+}) \to p = \underset{˙}{+}$
27	26	adantr	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to p = \underset{˙}{+}$
28		oveq	$⊢ t = \underset{˙}{\cdot} \to x t y = x \underset{˙}{\cdot} y$
29	28	adantl	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to x t y = x \underset{˙}{\cdot} y$
30		oveq	$⊢ t = \underset{˙}{\cdot} \to x t z = x \underset{˙}{\cdot} z$
31	30	adantl	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to x t z = x \underset{˙}{\cdot} z$
32	27 29 31	oveq123d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (x t y) p (x t z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z)$
33	25 32	eqeq12d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (x t (y p z) = (x t y) p (x t z) \leftrightarrow x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z))$
34		oveq	$⊢ p = \underset{˙}{+} \to x p y = x \underset{˙}{+} y$
35	34	ad2antlr	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to x p y = x \underset{˙}{+} y$
36		eqidd	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to z = z$
37	21 35 36	oveq123d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (x p y) t z = (x \underset{˙}{+} y) \underset{˙}{\cdot} z$
38		oveq	$⊢ t = \underset{˙}{\cdot} \to y t z = y \underset{˙}{\cdot} z$
39	38	adantl	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to y t z = y \underset{˙}{\cdot} z$
40	27 31 39	oveq123d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (x t z) p (y t z) = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
41	37 40	eqeq12d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to ((x p y) t z = (x t z) p (y t z) \leftrightarrow (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
42	33 41	anbi12d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to ((x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z)) \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)))$
43	20 42	raleqbidv	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (\forall z \in b (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z)) \leftrightarrow \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)))$
44	20 43	raleqbidv	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (\forall y \in b \forall z \in b (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z)) \leftrightarrow \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)))$
45	20 44	raleqbidv	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (\forall x \in b \forall y \in b \forall z \in b (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z)) \leftrightarrow \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)))$
46	15 19 45	sbcied2	$⊢ ((r = R \land b = B) \land p = \underset{˙}{+}) \to (\underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z)) \leftrightarrow \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)))$
47	11 14 46	sbcied2	$⊢ (r = R \land b = B) \to (\underset{˙}{[} +_{r} / p \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z)) \leftrightarrow \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)))$
48	8 10 47	sbcied2	$⊢ r = R \to (\underset{˙}{[} {Base}_{r} / b \underset{˙}{]} \underset{˙}{[} +_{r} / p \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z)) \leftrightarrow \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)))$
49	7 48	anbi12d	$⊢ r = R \to (({mulGrp}_{r} \in Smgrp \land \underset{˙}{[} {Base}_{r} / b \underset{˙}{]} \underset{˙}{[} +_{r} / p \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z))) \leftrightarrow (G \in Smgrp \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))))$
50		df-rng	$⊢ Rng = \{r \in Abel \| ({mulGrp}_{r} \in Smgrp \land \underset{˙}{[} {Base}_{r} / b \underset{˙}{]} \underset{˙}{[} +_{r} / p \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z)))\}$
51	49 50	elrab2	$⊢ R \in Rng \leftrightarrow (R \in Abel \land (G \in Smgrp \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))))$
52		3anass	$⊢ (R \in Abel \land G \in Smgrp \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))) \leftrightarrow (R \in Abel \land (G \in Smgrp \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))))$
53	51 52	bitr4i	$⊢ R \in Rng \leftrightarrow (R \in Abel \land G \in Smgrp \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)))$

Metamath Proof Explorer

Theorem isrng

Proof