Metamath Proof Explorer


Theorem 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 0 ˙ = 0 T
lmhmfgsplit.k K = F -1 0 ˙
lmhmfgsplit.u U = S 𝑠 K
lmhmfgsplit.v V = T 𝑠 ran F
Assertion lmhmfgsplit F S LMHom T U LFinGen V LFinGen S LFinGen

Proof

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