Metamath Proof Explorer

Theorem islnm2

Description: Property of being a Noetherian left module with finite generation expanded in terms of spans. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses islnm2.b ⊢ B = Base M
islnm2.s ⊢ S = LSubSp ⁡ M
islnm2.n ⊢ N = LSpan ⁡ M
Assertion islnm2 ⊢ M ∈ LNoeM ↔ M ∈ LMod ∧ ∀ i ∈ S ∃ g ∈ 𝒫 B ∩ Fin i = N ⁡ g

Proof

Step Hyp Ref Expression
1 islnm2.b ⊢ B = Base M
2 islnm2.s ⊢ S = LSubSp ⁡ M
3 islnm2.n ⊢ N = LSpan ⁡ M
4 2 islnm ⊢ M ∈ LNoeM ↔ M ∈ LMod ∧ ∀ i ∈ S M ↾ 𝑠 i ∈ LFinGen
5 eqid ⊢ M ↾ 𝑠 i = M ↾ 𝑠 i
6 5 2 3 1 islssfg2 ⊢ M ∈ LMod ∧ i ∈ S → M ↾ 𝑠 i ∈ LFinGen ↔ ∃ g ∈ 𝒫 B ∩ Fin N ⁡ g = i
7 eqcom ⊢ N ⁡ g = i ↔ i = N ⁡ g
8 7 rexbii ⊢ ∃ g ∈ 𝒫 B ∩ Fin N ⁡ g = i ↔ ∃ g ∈ 𝒫 B ∩ Fin i = N ⁡ g
9 6 8 bitrdi ⊢ M ∈ LMod ∧ i ∈ S → M ↾ 𝑠 i ∈ LFinGen ↔ ∃ g ∈ 𝒫 B ∩ Fin i = N ⁡ g
10 9 ralbidva ⊢ M ∈ LMod → ∀ i ∈ S M ↾ 𝑠 i ∈ LFinGen ↔ ∀ i ∈ S ∃ g ∈ 𝒫 B ∩ Fin i = N ⁡ g
11 10 pm5.32i ⊢ M ∈ LMod ∧ ∀ i ∈ S M ↾ 𝑠 i ∈ LFinGen ↔ M ∈ LMod ∧ ∀ i ∈ S ∃ g ∈ 𝒫 B ∩ Fin i = N ⁡ g
12 4 11 bitri ⊢ M ∈ LNoeM ↔ M ∈ LMod ∧ ∀ i ∈ S ∃ g ∈ 𝒫 B ∩ Fin i = N ⁡ g