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	Could not format ( R e. Rng -> ( mulGrp ` R ) e. Smgrp ) : No typesetting found for \|- ( R e. Rng -> ( mulGrp ` R ) e. Smgrp ) with typecode \|-
14	13	anim1i	Could not format ( ( R e. Rng /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) -> ( ( mulGrp ` R ) e. Smgrp /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) : No typesetting found for \|- ( ( R e. Rng /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) -> ( ( mulGrp ` R ) e. Smgrp /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) with typecode \|-
15	12 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
16	12 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
17	15 16	ismnddef	Could not format ( ( mulGrp ` R ) e. Mnd <-> ( ( mulGrp ` R ) e. Smgrp /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) : No typesetting found for \|- ( ( mulGrp ` R ) e. Mnd <-> ( ( mulGrp ` R ) e. Smgrp /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) with typecode \|-
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	Could not format ( R e. Rng <-> ( R e. Abel /\ ( mulGrp ` R ) e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y ( +g ` R ) z ) ) = ( ( x .x. y ) ( +g ` R ) ( x .x. z ) ) /\ ( ( x ( +g ` R ) y ) .x. z ) = ( ( x .x. z ) ( +g ` R ) ( y .x. z ) ) ) ) ) : No typesetting found for \|- ( R e. Rng <-> ( R e. Abel /\ ( mulGrp ` R ) e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y ( +g ` R ) z ) ) = ( ( x .x. y ) ( +g ` R ) ( x .x. z ) ) /\ ( ( x ( +g ` R ) y ) .x. z ) = ( ( x .x. z ) ( +g ` R ) ( y .x. z ) ) ) ) ) with typecode \|-
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