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