Metamath Proof Explorer

Theorem lringnzr

Description: A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025)

		Ref	Expression
	Assertion	lringnzr	\|- ( R e. LRing -> R e. NzRing )

Proof

Step	Hyp	Ref	Expression
1		df-lring	\|- LRing = { r e. NzRing \| A. x e. ( Base ` r ) A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. ( Unit ` r ) \/ y e. ( Unit ` r ) ) ) }
2	1	ssrab3	\|- LRing C_ NzRing
3	2	sseli	\|- ( R e. LRing -> R e. NzRing )

Step

Hyp

Ref

Expression

df-lring

 |-  LRing = { r e. NzRing | A. x e. ( Base ` r ) A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. ( Unit ` r ) \/ y e. ( Unit ` r ) ) ) }

ssrab3

 |-  LRing C_ NzRing

sseli

 |-  ( R e. LRing -> R e. NzRing )