isringrng

Description: The predicate "is a unital ring" as extension of the predicate "is a non-unital ring". (Contributed by AV, 17-Feb-2020)

	Ref	Expression
Hypotheses	isringrng.b	$⊢ B = {Base}_{R}$
	isringrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	isringrng	$⊢ R \in Ring \leftrightarrow (R \in Rng \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$

Proof

Step	Hyp	Ref	Expression
1		isringrng.b	$⊢ B = {Base}_{R}$
2		isringrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		ringrng	$⊢ R \in Ring \to R \in Rng$
4	1 2	ringideu	$⊢ R \in Ring \to \exists! x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)$
5		reurex	$⊢ \exists! x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y) \to \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)$
6	4 5	syl	$⊢ R \in Ring \to \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)$
7	3 6	jca	$⊢ R \in Ring \to (R \in Rng \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$
8		rngabl	$⊢ R \in Rng \to R \in Abel$
9		ablgrp	$⊢ R \in Abel \to R \in Grp$
10	8 9	syl	$⊢ R \in Rng \to R \in Grp$
11	10	adantr	$⊢ (R \in Rng \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \to R \in Grp$
12		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
13	12	rngmgp	$⊢ R \in Rng \to {mulGrp}_{R} \in Smgrp$
14	13	anim1i	$⊢ (R \in Rng \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \to ({mulGrp}_{R} \in Smgrp \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$
15	12 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
16	12 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
17	15 16	ismnddef	$⊢ {mulGrp}_{R} \in Mnd \leftrightarrow ({mulGrp}_{R} \in Smgrp \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$
18	14 17	sylibr	$⊢ (R \in Rng \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \to {mulGrp}_{R} \in Mnd$
19		eqid	$⊢ +_{R} = +_{R}$
20	1 12 19 2	isrng	$⊢ R \in Rng \leftrightarrow (R \in Abel \land {mulGrp}_{R} \in Smgrp \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y +_{R} z) = (x \underset{˙}{\cdot} y) +_{R} (x \underset{˙}{\cdot} z) \land (x +_{R} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) +_{R} (y \underset{˙}{\cdot} z)))$
21	20	simp3bi	$⊢ R \in Rng \to \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y +_{R} z) = (x \underset{˙}{\cdot} y) +_{R} (x \underset{˙}{\cdot} z) \land (x +_{R} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) +_{R} (y \underset{˙}{\cdot} z))$
22	21	adantr	$⊢ (R \in Rng \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \to \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y +_{R} z) = (x \underset{˙}{\cdot} y) +_{R} (x \underset{˙}{\cdot} z) \land (x +_{R} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) +_{R} (y \underset{˙}{\cdot} z))$
23	1 12 19 2	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 +_{R} z) = (x \underset{˙}{\cdot} y) +_{R} (x \underset{˙}{\cdot} z) \land (x +_{R} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) +_{R} (y \underset{˙}{\cdot} z)))$
24	11 18 22 23	syl3anbrc	$⊢ (R \in Rng \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \to R \in Ring$
25	7 24	impbii	$⊢ R \in Ring \leftrightarrow (R \in Rng \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$

Metamath Proof Explorer

Theorem isringrng

Proof