lnmlmic

Description: Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015)

		Ref	Expression
	Assertion	lnmlmic	$⊢ R ≃_{𝑚} S \to (R \in LNoeM \leftrightarrow S \in LNoeM)$

Proof

Step	Hyp	Ref	Expression
1		brlmic	$⊢ R ≃_{𝑚} S \leftrightarrow R LMIso S \neq \emptyset$
2		n0	$⊢ R LMIso S \neq \emptyset \leftrightarrow \exists a a \in (R LMIso S)$
3	1 2	bitri	$⊢ R ≃_{𝑚} S \leftrightarrow \exists a a \in (R LMIso S)$
4		lmimlmhm	$⊢ a \in (R LMIso S) \to a \in (R LMHom S)$
5	4	adantr	$⊢ (a \in (R LMIso S) \land R \in LNoeM) \to a \in (R LMHom S)$
6		simpr	$⊢ (a \in (R LMIso S) \land R \in LNoeM) \to R \in LNoeM$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8		eqid	$⊢ {Base}_{S} = {Base}_{S}$
9	7 8	lmimf1o	$⊢ a \in (R LMIso S) \to a : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S}$
10		f1ofo	$⊢ a : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S} \to a : {Base}_{R} \underset{onto}{⟶} {Base}_{S}$
11		forn	$⊢ a : {Base}_{R} \underset{onto}{⟶} {Base}_{S} \to ran a = {Base}_{S}$
12	9 10 11	3syl	$⊢ a \in (R LMIso S) \to ran a = {Base}_{S}$
13	12	adantr	$⊢ (a \in (R LMIso S) \land R \in LNoeM) \to ran a = {Base}_{S}$
14	8	lnmepi	$⊢ (a \in (R LMHom S) \land R \in LNoeM \land ran a = {Base}_{S}) \to S \in LNoeM$
15	5 6 13 14	syl3anc	$⊢ (a \in (R LMIso S) \land R \in LNoeM) \to S \in LNoeM$
16		islmim2	$⊢ a \in (R LMIso S) \leftrightarrow (a \in (R LMHom S) \land a^{-1} \in (S LMHom R))$
17	16	simprbi	$⊢ a \in (R LMIso S) \to a^{-1} \in (S LMHom R)$
18	17	adantr	$⊢ (a \in (R LMIso S) \land S \in LNoeM) \to a^{-1} \in (S LMHom R)$
19		simpr	$⊢ (a \in (R LMIso S) \land S \in LNoeM) \to S \in LNoeM$
20		dfdm4	$⊢ dom a = ran a^{-1}$
21		f1odm	$⊢ a : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S} \to dom a = {Base}_{R}$
22	9 21	syl	$⊢ a \in (R LMIso S) \to dom a = {Base}_{R}$
23	22	adantr	$⊢ (a \in (R LMIso S) \land S \in LNoeM) \to dom a = {Base}_{R}$
24	20 23	eqtr3id	$⊢ (a \in (R LMIso S) \land S \in LNoeM) \to ran a^{-1} = {Base}_{R}$
25	7	lnmepi	$⊢ (a^{-1} \in (S LMHom R) \land S \in LNoeM \land ran a^{-1} = {Base}_{R}) \to R \in LNoeM$
26	18 19 24 25	syl3anc	$⊢ (a \in (R LMIso S) \land S \in LNoeM) \to R \in LNoeM$
27	15 26	impbida	$⊢ a \in (R LMIso S) \to (R \in LNoeM \leftrightarrow S \in LNoeM)$
28	27	exlimiv	$⊢ \exists a a \in (R LMIso S) \to (R \in LNoeM \leftrightarrow S \in LNoeM)$
29	3 28	sylbi	$⊢ R ≃_{𝑚} S \to (R \in LNoeM \leftrightarrow S \in LNoeM)$

Metamath Proof Explorer

Theorem lnmlmic

Proof