Theorem lringnzr

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

	Ref	Expression
Assertion	lringnzr	Could not format assertion : No typesetting found for |- ( R e. LRing -> R e. NzRing ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-lring	Could not format 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 ) ) ) } : No typesetting found for |- 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 ) ) ) } with typecode |-
2	1	ssrab3	Could not format LRing C_ NzRing : No typesetting found for |- LRing C_ NzRing with typecode |-
3	2	sseli	Could not format ( R e. LRing -> R e. NzRing ) : No typesetting found for |- ( R e. LRing -> R e. NzRing ) with typecode |-