Metamath Proof Explorer


Theorem islnr

Description: Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion islnr ( 𝐴 ∈ LNoeR ↔ ( 𝐴 ∈ Ring ∧ ( ringLMod ‘ 𝐴 ) ∈ LNoeM ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑎 = 𝐴 → ( ringLMod ‘ 𝑎 ) = ( ringLMod ‘ 𝐴 ) )
2 1 eleq1d ( 𝑎 = 𝐴 → ( ( ringLMod ‘ 𝑎 ) ∈ LNoeM ↔ ( ringLMod ‘ 𝐴 ) ∈ LNoeM ) )
3 df-lnr LNoeR = { 𝑎 ∈ Ring ∣ ( ringLMod ‘ 𝑎 ) ∈ LNoeM }
4 2 3 elrab2 ( 𝐴 ∈ LNoeR ↔ ( 𝐴 ∈ Ring ∧ ( ringLMod ‘ 𝐴 ) ∈ LNoeM ) )