Theorem lnrring

Description: Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Assertion	lnrring	⊢ ( 𝐴 ∈ LNoeR → 𝐴 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		islnr	⊢ ( 𝐴 ∈ LNoeR ↔ ( 𝐴 ∈ Ring ∧ ( ringLMod ‘ 𝐴 ) ∈ LNoeM ) )
2	1	simplbi	⊢ ( 𝐴 ∈ LNoeR → 𝐴 ∈ Ring )