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 \in LNoeM \leftrightarrow (M \in LMod \land \forall i \in S \exists g \in (𝒫 B \cap 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 \in LNoeM \leftrightarrow (M \in LMod \land \forall i \in S M ↾_{𝑠} i \in LFinGen)$
5		eqid	$⊢ M ↾_{𝑠} i = M ↾_{𝑠} i$
6	5 2 3 1	islssfg2	$⊢ (M \in LMod \land i \in S) \to (M ↾_{𝑠} i \in LFinGen \leftrightarrow \exists g \in (𝒫 B \cap Fin) N (g) = i)$
7		eqcom	$⊢ N (g) = i \leftrightarrow i = N (g)$
8	7	rexbii	$⊢ \exists g \in (𝒫 B \cap Fin) N (g) = i \leftrightarrow \exists g \in (𝒫 B \cap Fin) i = N (g)$
9	6 8	bitrdi	$⊢ (M \in LMod \land i \in S) \to (M ↾_{𝑠} i \in LFinGen \leftrightarrow \exists g \in (𝒫 B \cap Fin) i = N (g))$
10	9	ralbidva	$⊢ M \in LMod \to (\forall i \in S M ↾_{𝑠} i \in LFinGen \leftrightarrow \forall i \in S \exists g \in (𝒫 B \cap Fin) i = N (g))$
11	10	pm5.32i	$⊢ (M \in LMod \land \forall i \in S M ↾_{𝑠} i \in LFinGen) \leftrightarrow (M \in LMod \land \forall i \in S \exists g \in (𝒫 B \cap Fin) i = N (g))$
12	4 11	bitri	$⊢ M \in LNoeM \leftrightarrow (M \in LMod \land \forall i \in S \exists g \in (𝒫 B \cap Fin) i = N (g))$