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	⊢ 𝐵 = ( Base ‘ 𝑀 )
	islnm2.s	⊢ 𝑆 = ( LSubSp ‘ 𝑀 )
	islnm2.n	⊢ 𝑁 = ( LSpan ‘ 𝑀 )
Assertion	islnm2	⊢ ( 𝑀 ∈ LNoeM ↔ ( 𝑀 ∈ LMod ∧ ∀ 𝑖 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) )

Proof

Step	Hyp	Ref	Expression
1		islnm2.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		islnm2.s	⊢ 𝑆 = ( LSubSp ‘ 𝑀 )
3		islnm2.n	⊢ 𝑁 = ( LSpan ‘ 𝑀 )
4	2	islnm	⊢ ( 𝑀 ∈ LNoeM ↔ ( 𝑀 ∈ LMod ∧ ∀ 𝑖 ∈ 𝑆 ( 𝑀 ↾s 𝑖 ) ∈ LFinGen ) )
5		eqid	⊢ ( 𝑀 ↾s 𝑖 ) = ( 𝑀 ↾s 𝑖 )
6	5 2 3 1	islssfg2	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑖 ∈ 𝑆 ) → ( ( 𝑀 ↾s 𝑖 ) ∈ LFinGen ↔ ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑁 ‘ 𝑔 ) = 𝑖 ) )
7		eqcom	⊢ ( ( 𝑁 ‘ 𝑔 ) = 𝑖 ↔ 𝑖 = ( 𝑁 ‘ 𝑔 ) )
8	7	rexbii	⊢ ( ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑁 ‘ 𝑔 ) = 𝑖 ↔ ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) )
9	6 8	bitrdi	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑖 ∈ 𝑆 ) → ( ( 𝑀 ↾s 𝑖 ) ∈ LFinGen ↔ ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) )
10	9	ralbidva	⊢ ( 𝑀 ∈ LMod → ( ∀ 𝑖 ∈ 𝑆 ( 𝑀 ↾s 𝑖 ) ∈ LFinGen ↔ ∀ 𝑖 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) )
11	10	pm5.32i	⊢ ( ( 𝑀 ∈ LMod ∧ ∀ 𝑖 ∈ 𝑆 ( 𝑀 ↾s 𝑖 ) ∈ LFinGen ) ↔ ( 𝑀 ∈ LMod ∧ ∀ 𝑖 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) )
12	4 11	bitri	⊢ ( 𝑀 ∈ LNoeM ↔ ( 𝑀 ∈ LMod ∧ ∀ 𝑖 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) )