lmhmfgsplit

Description: If the kernel and range of a homomorphism of left modules are finitely generated, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015) (Revised by Stefan O'Rear, 6-May-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	lmhmfgsplit	$⊢ (F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \to S \in LFinGen$

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		simp3	$⊢ (F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \to V \in LFinGen$
6		lmhmlmod2	$⊢ F \in (S LMHom T) \to T \in LMod$
7	6	3ad2ant1	$⊢ (F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \to T \in LMod$
8		lmhmrnlss	$⊢ F \in (S LMHom T) \to ran F \in LSubSp (T)$
9	8	3ad2ant1	$⊢ (F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \to ran F \in LSubSp (T)$
10		eqid	$⊢ LSubSp (T) = LSubSp (T)$
11		eqid	$⊢ LSpan (T) = LSpan (T)$
12	4 10 11	islssfg	$⊢ (T \in LMod \land ran F \in LSubSp (T)) \to (V \in LFinGen \leftrightarrow \exists a \in 𝒫 ran F (a \in Fin \land LSpan (T) (a) = ran F))$
13	7 9 12	syl2anc	$⊢ (F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \to (V \in LFinGen \leftrightarrow \exists a \in 𝒫 ran F (a \in Fin \land LSpan (T) (a) = ran F))$
14	5 13	mpbid	$⊢ (F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \to \exists a \in 𝒫 ran F (a \in Fin \land LSpan (T) (a) = ran F)$
15		simpl1	$⊢ ((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \to F \in (S LMHom T)$
16		eqid	$⊢ {Base}_{S} = {Base}_{S}$
17		eqid	$⊢ {Base}_{T} = {Base}_{T}$
18	16 17	lmhmf	$⊢ F \in (S LMHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
19		ffn	$⊢ F : {Base}_{S} ⟶ {Base}_{T} \to F Fn {Base}_{S}$
20	15 18 19	3syl	$⊢ ((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \to F Fn {Base}_{S}$
21		elpwi	$⊢ a \in 𝒫 ran F \to a \subseteq ran F$
22	21	ad2antrl	$⊢ ((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \to a \subseteq ran F$
23		simprrl	$⊢ ((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \to a \in Fin$
24		fipreima	$⊢ (F Fn {Base}_{S} \land a \subseteq ran F \land a \in Fin) \to \exists b \in (𝒫 {Base}_{S} \cap Fin) F [b] = a$
25	20 22 23 24	syl3anc	$⊢ ((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \to \exists b \in (𝒫 {Base}_{S} \cap Fin) F [b] = a$
26		eqid	$⊢ LSubSp (S) = LSubSp (S)$
27		eqid	$⊢ LSSum (S) = LSSum (S)$
28		simpll1	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to F \in (S LMHom T)$
29		lmhmlmod1	$⊢ F \in (S LMHom T) \to S \in LMod$
30	29	3ad2ant1	$⊢ (F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \to S \in LMod$
31	30	ad2antrr	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to S \in LMod$
32		inss1	$⊢ 𝒫 {Base}_{S} \cap Fin \subseteq 𝒫 {Base}_{S}$
33	32	sseli	$⊢ b \in (𝒫 {Base}_{S} \cap Fin) \to b \in 𝒫 {Base}_{S}$
34		elpwi	$⊢ b \in 𝒫 {Base}_{S} \to b \subseteq {Base}_{S}$
35	33 34	syl	$⊢ b \in (𝒫 {Base}_{S} \cap Fin) \to b \subseteq {Base}_{S}$
36	35	ad2antrl	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to b \subseteq {Base}_{S}$
37		eqid	$⊢ LSpan (S) = LSpan (S)$
38	16 26 37	lspcl	$⊢ (S \in LMod \land b \subseteq {Base}_{S}) \to LSpan (S) (b) \in LSubSp (S)$
39	31 36 38	syl2anc	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to LSpan (S) (b) \in LSubSp (S)$
40	16 37 11	lmhmlsp	$⊢ (F \in (S LMHom T) \land b \subseteq {Base}_{S}) \to F [LSpan (S) (b)] = LSpan (T) (F [b])$
41	28 36 40	syl2anc	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to F [LSpan (S) (b)] = LSpan (T) (F [b])$
42		fveq2	$⊢ F [b] = a \to LSpan (T) (F [b]) = LSpan (T) (a)$
43	42	ad2antll	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to LSpan (T) (F [b]) = LSpan (T) (a)$
44		simp2rr	$⊢ ((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F)) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to LSpan (T) (a) = ran F$
45	44	3expa	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to LSpan (T) (a) = ran F$
46	41 43 45	3eqtrd	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to F [LSpan (S) (b)] = ran F$
47	26 27 1 2 16 28 39 46	kercvrlsm	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to K LSSum (S) LSpan (S) (b) = {Base}_{S}$
48	47	oveq2d	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to S ↾_{𝑠} (K LSSum (S) LSpan (S) (b)) = S ↾_{𝑠} {Base}_{S}$
49	16	ressid	$⊢ S \in LMod \to S ↾_{𝑠} {Base}_{S} = S$
50	30 49	syl	$⊢ (F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \to S ↾_{𝑠} {Base}_{S} = S$
51	50	ad2antrr	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to S ↾_{𝑠} {Base}_{S} = S$
52	48 51	eqtr2d	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to S = S ↾_{𝑠} (K LSSum (S) LSpan (S) (b))$
53		eqid	$⊢ S ↾_{𝑠} LSpan (S) (b) = S ↾_{𝑠} LSpan (S) (b)$
54		eqid	$⊢ S ↾_{𝑠} (K LSSum (S) LSpan (S) (b)) = S ↾_{𝑠} (K LSSum (S) LSpan (S) (b))$
55	2 1 26	lmhmkerlss	$⊢ F \in (S LMHom T) \to K \in LSubSp (S)$
56	55	3ad2ant1	$⊢ (F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \to K \in LSubSp (S)$
57	56	ad2antrr	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to K \in LSubSp (S)$
58		simpll2	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to U \in LFinGen$
59		inss2	$⊢ 𝒫 {Base}_{S} \cap Fin \subseteq Fin$
60	59	sseli	$⊢ b \in (𝒫 {Base}_{S} \cap Fin) \to b \in Fin$
61	60	ad2antrl	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to b \in Fin$
62	37 16 53	islssfgi	$⊢ (S \in LMod \land b \subseteq {Base}_{S} \land b \in Fin) \to S ↾_{𝑠} LSpan (S) (b) \in LFinGen$
63	31 36 61 62	syl3anc	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to S ↾_{𝑠} LSpan (S) (b) \in LFinGen$
64	26 27 3 53 54 31 57 39 58 63	lsmfgcl	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to S ↾_{𝑠} (K LSSum (S) LSpan (S) (b)) \in LFinGen$
65	52 64	eqeltrd	$⊢ (((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \land (b \in (𝒫 {Base}_{S} \cap Fin) \land F [b] = a)) \to S \in LFinGen$
66	25 65	rexlimddv	$⊢ ((F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \land (a \in 𝒫 ran F \land (a \in Fin \land LSpan (T) (a) = ran F))) \to S \in LFinGen$
67	14 66	rexlimddv	$⊢ (F \in (S LMHom T) \land U \in LFinGen \land V \in LFinGen) \to S \in LFinGen$

Metamath Proof Explorer

Theorem lmhmfgsplit

Proof