Theorem dfring2

Description: The predicate "is a unital ring" based on a ring being abelian. Definition of "ring with unit" in Lang p. 83. (Contributed by Jeff Hankins, 21-Nov-2006) (Revised by AV, 8-Aug-2026)

	Ref	Expression
Hypotheses	isringrng.b	|- B = ( Base ` R )
	isringrng.t	|- .x. = ( .r ` R )
	dfring2.g	|- G = ( mulGrp ` R )
	dfring2.p	|- .+ = ( +g ` R )
Assertion	dfring2	|- ( R e. Ring <-> ( R e. Abel /\ G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isringrng.b	|- B = ( Base ` R )
2		isringrng.t	|- .x. = ( .r ` R )
3		dfring2.g	|- G = ( mulGrp ` R )
4		dfring2.p	|- .+ = ( +g ` R )
5		ringabl	|- ( R e. Ring -> R e. Abel )
6	3	ringmgp	|- ( R e. Ring -> G e. Mnd )
7	1 3 4 2	isring	|- ( R e. Ring <-> ( R e. Grp /\ G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
8	7	simp3bi	|- ( R e. Ring -> A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) )
9	5 6 8	3jca	|- ( R e. Ring -> ( R e. Abel /\ G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
10		ablgrp	|- ( R e. Abel -> R e. Grp )
11	10	3anim1i	|- ( ( R e. Abel /\ G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) -> ( R e. Grp /\ G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
12	11 7	sylibr	|- ( ( R e. Abel /\ G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) -> R e. Ring )
13	9 12	impbii	|- ( R e. Ring <-> ( R e. Abel /\ G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )