lmhmlnmsplit

Description: If the kernel and range of a homomorphism of left modules are Noetherian, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015) (Revised by Stefan O'Rear, 12-Jun-2015)

	Ref	Expression
Hypotheses	lmhmfgsplit.z	$⊢ \underset{˙}{0} = 0_{T}$
	lmhmfgsplit.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
	lmhmfgsplit.u	$⊢ U = S ↾_{𝑠} K$
	lmhmfgsplit.v	$⊢ V = T ↾_{𝑠} ran F$
Assertion	lmhmlnmsplit	$⊢ (F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \to S \in LNoeM$

Proof

Step	Hyp	Ref	Expression
1		lmhmfgsplit.z	$⊢ \underset{˙}{0} = 0_{T}$
2		lmhmfgsplit.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
3		lmhmfgsplit.u	$⊢ U = S ↾_{𝑠} K$
4		lmhmfgsplit.v	$⊢ V = T ↾_{𝑠} ran F$
5		lmhmlmod1	$⊢ F \in (S LMHom T) \to S \in LMod$
6	5	3ad2ant1	$⊢ (F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \to S \in LMod$
7		eqid	$⊢ LSubSp (S) = LSubSp (S)$
8		eqid	$⊢ S ↾_{𝑠} a = S ↾_{𝑠} a$
9	7 8	reslmhm	$⊢ (F \in (S LMHom T) \land a \in LSubSp (S)) \to {F ↾}_{a} \in ((S ↾_{𝑠} a) LMHom T)$
10	9	3ad2antl1	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to {F ↾}_{a} \in ((S ↾_{𝑠} a) LMHom T)$
11		cnvresima	$⊢ {({F ↾}_{a})}^{-1} [\{\underset{˙}{0}\}] = F^{-1} [\{\underset{˙}{0}\}] \cap a$
12	2	eqcomi	$⊢ F^{-1} [\{\underset{˙}{0}\}] = K$
13	12	ineq1i	$⊢ F^{-1} [\{\underset{˙}{0}\}] \cap a = K \cap a$
14		incom	$⊢ K \cap a = a \cap K$
15	11 13 14	3eqtri	$⊢ {({F ↾}_{a})}^{-1} [\{\underset{˙}{0}\}] = a \cap K$
16	15	oveq2i	$⊢ (S ↾_{𝑠} a) ↾_{𝑠} {({F ↾}_{a})}^{-1} [\{\underset{˙}{0}\}] = (S ↾_{𝑠} a) ↾_{𝑠} (a \cap K)$
17		vex	$⊢ a \in V$
18		inss1	$⊢ a \cap K \subseteq a$
19		ressabs	$⊢ (a \in V \land a \cap K \subseteq a) \to (S ↾_{𝑠} a) ↾_{𝑠} (a \cap K) = S ↾_{𝑠} (a \cap K)$
20	17 18 19	mp2an	$⊢ (S ↾_{𝑠} a) ↾_{𝑠} (a \cap K) = S ↾_{𝑠} (a \cap K)$
21	3	oveq1i	$⊢ U ↾_{𝑠} (a \cap K) = (S ↾_{𝑠} K) ↾_{𝑠} (a \cap K)$
22		simpl1	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to F \in (S LMHom T)$
23		cnvexg	$⊢ F \in (S LMHom T) \to F^{-1} \in V$
24		imaexg	$⊢ F^{-1} \in V \to F^{-1} [\{\underset{˙}{0}\}] \in V$
25	23 24	syl	$⊢ F \in (S LMHom T) \to F^{-1} [\{\underset{˙}{0}\}] \in V$
26	2 25	eqeltrid	$⊢ F \in (S LMHom T) \to K \in V$
27	22 26	syl	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to K \in V$
28		inss2	$⊢ a \cap K \subseteq K$
29		ressabs	$⊢ (K \in V \land a \cap K \subseteq K) \to (S ↾_{𝑠} K) ↾_{𝑠} (a \cap K) = S ↾_{𝑠} (a \cap K)$
30	27 28 29	sylancl	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to (S ↾_{𝑠} K) ↾_{𝑠} (a \cap K) = S ↾_{𝑠} (a \cap K)$
31	21 30	syl5eq	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to U ↾_{𝑠} (a \cap K) = S ↾_{𝑠} (a \cap K)$
32	20 31	eqtr4id	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to (S ↾_{𝑠} a) ↾_{𝑠} (a \cap K) = U ↾_{𝑠} (a \cap K)$
33	16 32	syl5eq	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to (S ↾_{𝑠} a) ↾_{𝑠} {({F ↾}_{a})}^{-1} [\{\underset{˙}{0}\}] = U ↾_{𝑠} (a \cap K)$
34		simpl2	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to U \in LNoeM$
35	6	adantr	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to S \in LMod$
36		simpr	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to a \in LSubSp (S)$
37	2 1 7	lmhmkerlss	$⊢ F \in (S LMHom T) \to K \in LSubSp (S)$
38	22 37	syl	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to K \in LSubSp (S)$
39	7	lssincl	$⊢ (S \in LMod \land a \in LSubSp (S) \land K \in LSubSp (S)) \to a \cap K \in LSubSp (S)$
40	35 36 38 39	syl3anc	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to a \cap K \in LSubSp (S)$
41	28	a1i	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to a \cap K \subseteq K$
42		eqid	$⊢ LSubSp (U) = LSubSp (U)$
43	3 7 42	lsslss	$⊢ (S \in LMod \land K \in LSubSp (S)) \to (a \cap K \in LSubSp (U) \leftrightarrow (a \cap K \in LSubSp (S) \land a \cap K \subseteq K))$
44	35 38 43	syl2anc	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to (a \cap K \in LSubSp (U) \leftrightarrow (a \cap K \in LSubSp (S) \land a \cap K \subseteq K))$
45	40 41 44	mpbir2and	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to a \cap K \in LSubSp (U)$
46		eqid	$⊢ U ↾_{𝑠} (a \cap K) = U ↾_{𝑠} (a \cap K)$
47	42 46	lnmlssfg	$⊢ (U \in LNoeM \land a \cap K \in LSubSp (U)) \to U ↾_{𝑠} (a \cap K) \in LFinGen$
48	34 45 47	syl2anc	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to U ↾_{𝑠} (a \cap K) \in LFinGen$
49	33 48	eqeltrd	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to (S ↾_{𝑠} a) ↾_{𝑠} {({F ↾}_{a})}^{-1} [\{\underset{˙}{0}\}] \in LFinGen$
50		incom	$⊢ ran F \cap ran ({F ↾}_{a}) = ran ({F ↾}_{a}) \cap ran F$
51		resss	$⊢ {F ↾}_{a} \subseteq F$
52		rnss	$⊢ {F ↾}_{a} \subseteq F \to ran ({F ↾}_{a}) \subseteq ran F$
53	51 52	ax-mp	$⊢ ran ({F ↾}_{a}) \subseteq ran F$
54		df-ss	$⊢ ran ({F ↾}_{a}) \subseteq ran F \leftrightarrow ran ({F ↾}_{a}) \cap ran F = ran ({F ↾}_{a})$
55	53 54	mpbi	$⊢ ran ({F ↾}_{a}) \cap ran F = ran ({F ↾}_{a})$
56	50 55	eqtr2i	$⊢ ran ({F ↾}_{a}) = ran F \cap ran ({F ↾}_{a})$
57	56	oveq2i	$⊢ T ↾_{𝑠} ran ({F ↾}_{a}) = T ↾_{𝑠} (ran F \cap ran ({F ↾}_{a}))$
58	4	oveq1i	$⊢ V ↾_{𝑠} ran ({F ↾}_{a}) = (T ↾_{𝑠} ran F) ↾_{𝑠} ran ({F ↾}_{a})$
59		rnexg	$⊢ F \in (S LMHom T) \to ran F \in V$
60		resexg	$⊢ F \in (S LMHom T) \to {F ↾}_{a} \in V$
61		rnexg	$⊢ {F ↾}_{a} \in V \to ran ({F ↾}_{a}) \in V$
62	60 61	syl	$⊢ F \in (S LMHom T) \to ran ({F ↾}_{a}) \in V$
63		ressress	$⊢ (ran F \in V \land ran ({F ↾}_{a}) \in V) \to (T ↾_{𝑠} ran F) ↾_{𝑠} ran ({F ↾}_{a}) = T ↾_{𝑠} (ran F \cap ran ({F ↾}_{a}))$
64	59 62 63	syl2anc	$⊢ F \in (S LMHom T) \to (T ↾_{𝑠} ran F) ↾_{𝑠} ran ({F ↾}_{a}) = T ↾_{𝑠} (ran F \cap ran ({F ↾}_{a}))$
65	58 64	syl5eq	$⊢ F \in (S LMHom T) \to V ↾_{𝑠} ran ({F ↾}_{a}) = T ↾_{𝑠} (ran F \cap ran ({F ↾}_{a}))$
66	57 65	eqtr4id	$⊢ F \in (S LMHom T) \to T ↾_{𝑠} ran ({F ↾}_{a}) = V ↾_{𝑠} ran ({F ↾}_{a})$
67	22 66	syl	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to T ↾_{𝑠} ran ({F ↾}_{a}) = V ↾_{𝑠} ran ({F ↾}_{a})$
68		simpl3	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to V \in LNoeM$
69		lmhmrnlss	$⊢ {F ↾}_{a} \in ((S ↾_{𝑠} a) LMHom T) \to ran ({F ↾}_{a}) \in LSubSp (T)$
70	10 69	syl	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to ran ({F ↾}_{a}) \in LSubSp (T)$
71	53	a1i	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to ran ({F ↾}_{a}) \subseteq ran F$
72		lmhmlmod2	$⊢ F \in (S LMHom T) \to T \in LMod$
73	22 72	syl	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to T \in LMod$
74		lmhmrnlss	$⊢ F \in (S LMHom T) \to ran F \in LSubSp (T)$
75	22 74	syl	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to ran F \in LSubSp (T)$
76		eqid	$⊢ LSubSp (T) = LSubSp (T)$
77		eqid	$⊢ LSubSp (V) = LSubSp (V)$
78	4 76 77	lsslss	$⊢ (T \in LMod \land ran F \in LSubSp (T)) \to (ran ({F ↾}_{a}) \in LSubSp (V) \leftrightarrow (ran ({F ↾}_{a}) \in LSubSp (T) \land ran ({F ↾}_{a}) \subseteq ran F))$
79	73 75 78	syl2anc	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to (ran ({F ↾}_{a}) \in LSubSp (V) \leftrightarrow (ran ({F ↾}_{a}) \in LSubSp (T) \land ran ({F ↾}_{a}) \subseteq ran F))$
80	70 71 79	mpbir2and	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to ran ({F ↾}_{a}) \in LSubSp (V)$
81		eqid	$⊢ V ↾_{𝑠} ran ({F ↾}_{a}) = V ↾_{𝑠} ran ({F ↾}_{a})$
82	77 81	lnmlssfg	$⊢ (V \in LNoeM \land ran ({F ↾}_{a}) \in LSubSp (V)) \to V ↾_{𝑠} ran ({F ↾}_{a}) \in LFinGen$
83	68 80 82	syl2anc	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to V ↾_{𝑠} ran ({F ↾}_{a}) \in LFinGen$
84	67 83	eqeltrd	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to T ↾_{𝑠} ran ({F ↾}_{a}) \in LFinGen$
85		eqid	$⊢ {({F ↾}_{a})}^{-1} [\{\underset{˙}{0}\}] = {({F ↾}_{a})}^{-1} [\{\underset{˙}{0}\}]$
86		eqid	$⊢ (S ↾_{𝑠} a) ↾_{𝑠} {({F ↾}_{a})}^{-1} [\{\underset{˙}{0}\}] = (S ↾_{𝑠} a) ↾_{𝑠} {({F ↾}_{a})}^{-1} [\{\underset{˙}{0}\}]$
87		eqid	$⊢ T ↾_{𝑠} ran ({F ↾}_{a}) = T ↾_{𝑠} ran ({F ↾}_{a})$
88	1 85 86 87	lmhmfgsplit	$⊢ ({F ↾}_{a} \in ((S ↾_{𝑠} a) LMHom T) \land (S ↾_{𝑠} a) ↾_{𝑠} {({F ↾}_{a})}^{-1} [\{\underset{˙}{0}\}] \in LFinGen \land T ↾_{𝑠} ran ({F ↾}_{a}) \in LFinGen) \to S ↾_{𝑠} a \in LFinGen$
89	10 49 84 88	syl3anc	$⊢ ((F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \land a \in LSubSp (S)) \to S ↾_{𝑠} a \in LFinGen$
90	89	ralrimiva	$⊢ (F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \to \forall a \in LSubSp (S) S ↾_{𝑠} a \in LFinGen$
91	7	islnm	$⊢ S \in LNoeM \leftrightarrow (S \in LMod \land \forall a \in LSubSp (S) S ↾_{𝑠} a \in LFinGen)$
92	6 90 91	sylanbrc	$⊢ (F \in (S LMHom T) \land U \in LNoeM \land V \in LNoeM) \to S \in LNoeM$

Metamath Proof Explorer

Theorem lmhmlnmsplit

Proof