Theorem lringnzr

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

	Ref	Expression
Assertion	lringnzr	⊢ ( 𝑅 ∈ LRing → 𝑅 ∈ NzRing )

Proof

Step	Hyp	Ref	Expression
1		df-lring	⊢ LRing = { 𝑟 ∈ NzRing ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 ) → ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) ) ) }
2	1	ssrab3	⊢ LRing ⊆ NzRing
3	2	sseli	⊢ ( 𝑅 ∈ LRing → 𝑅 ∈ NzRing )