islnm

Description: Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014)

		Ref	Expression
	Hypothesis	islnm.s	$⊢ S = LSubSp (M)$
	Assertion	islnm	$⊢ M \in LNoeM \leftrightarrow (M \in LMod \land \forall i \in S M ↾_{𝑠} i \in LFinGen)$

Step	Hyp	Ref	Expression
1		islnm.s	$⊢ S = LSubSp (M)$
2		fveq2	$⊢ w = M \to LSubSp (w) = LSubSp (M)$
3	2 1	eqtr4di	$⊢ w = M \to LSubSp (w) = S$
4		oveq1	$⊢ w = M \to w ↾_{𝑠} i = M ↾_{𝑠} i$
5	4	eleq1d	$⊢ w = M \to (w ↾_{𝑠} i \in LFinGen \leftrightarrow M ↾_{𝑠} i \in LFinGen)$
6	3 5	raleqbidv	$⊢ w = M \to (\forall i \in LSubSp (w) w ↾_{𝑠} i \in LFinGen \leftrightarrow \forall i \in S M ↾_{𝑠} i \in LFinGen)$
7		df-lnm	$⊢ LNoeM = \{w \in LMod \| \forall i \in LSubSp (w) w ↾_{𝑠} i \in LFinGen\}$
8	6 7	elrab2	$⊢ M \in LNoeM \leftrightarrow (M \in LMod \land \forall i \in S M ↾_{𝑠} i \in LFinGen)$

Metamath Proof Explorer