lmhmfgima

Description: A homomorphism maps finitely generated submodules to finitely generated submodules. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	lmhmfgima.y	$⊢ Y = T ↾_{𝑠} F [A]$
	lmhmfgima.x	$⊢ X = S ↾_{𝑠} A$
	lmhmfgima.u	$⊢ U = LSubSp (S)$
	lmhmfgima.xf	$⊢ φ \to X \in LFinGen$
	lmhmfgima.a	$⊢ φ \to A \in U$
	lmhmfgima.f	$⊢ φ \to F \in (S LMHom T)$
Assertion	lmhmfgima	$⊢ φ \to Y \in LFinGen$

Proof

Step	Hyp	Ref	Expression
1		lmhmfgima.y	$⊢ Y = T ↾_{𝑠} F [A]$
2		lmhmfgima.x	$⊢ X = S ↾_{𝑠} A$
3		lmhmfgima.u	$⊢ U = LSubSp (S)$
4		lmhmfgima.xf	$⊢ φ \to X \in LFinGen$
5		lmhmfgima.a	$⊢ φ \to A \in U$
6		lmhmfgima.f	$⊢ φ \to F \in (S LMHom T)$
7		lmhmlmod1	$⊢ F \in (S LMHom T) \to S \in LMod$
8	6 7	syl	$⊢ φ \to S \in LMod$
9		eqid	$⊢ LSpan (S) = LSpan (S)$
10		eqid	$⊢ {Base}_{S} = {Base}_{S}$
11	2 3 9 10	islssfg2	$⊢ (S \in LMod \land A \in U) \to (X \in LFinGen \leftrightarrow \exists x \in (𝒫 {Base}_{S} \cap Fin) LSpan (S) (x) = A)$
12	8 5 11	syl2anc	$⊢ φ \to (X \in LFinGen \leftrightarrow \exists x \in (𝒫 {Base}_{S} \cap Fin) LSpan (S) (x) = A)$
13	4 12	mpbid	$⊢ φ \to \exists x \in (𝒫 {Base}_{S} \cap Fin) LSpan (S) (x) = A$
14		inss1	$⊢ 𝒫 {Base}_{S} \cap Fin \subseteq 𝒫 {Base}_{S}$
15	14	sseli	$⊢ x \in (𝒫 {Base}_{S} \cap Fin) \to x \in 𝒫 {Base}_{S}$
16	15	elpwid	$⊢ x \in (𝒫 {Base}_{S} \cap Fin) \to x \subseteq {Base}_{S}$
17		eqid	$⊢ LSpan (T) = LSpan (T)$
18	10 9 17	lmhmlsp	$⊢ (F \in (S LMHom T) \land x \subseteq {Base}_{S}) \to F [LSpan (S) (x)] = LSpan (T) (F [x])$
19	6 16 18	syl2an	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to F [LSpan (S) (x)] = LSpan (T) (F [x])$
20	19	oveq2d	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to T ↾_{𝑠} F [LSpan (S) (x)] = T ↾_{𝑠} LSpan (T) (F [x])$
21		lmhmlmod2	$⊢ F \in (S LMHom T) \to T \in LMod$
22	6 21	syl	$⊢ φ \to T \in LMod$
23	22	adantr	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to T \in LMod$
24		imassrn	$⊢ F [x] \subseteq ran F$
25		eqid	$⊢ {Base}_{T} = {Base}_{T}$
26	10 25	lmhmf	$⊢ F \in (S LMHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
27	6 26	syl	$⊢ φ \to F : {Base}_{S} ⟶ {Base}_{T}$
28	27	frnd	$⊢ φ \to ran F \subseteq {Base}_{T}$
29	24 28	sstrid	$⊢ φ \to F [x] \subseteq {Base}_{T}$
30	29	adantr	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to F [x] \subseteq {Base}_{T}$
31		inss2	$⊢ 𝒫 {Base}_{S} \cap Fin \subseteq Fin$
32	31	sseli	$⊢ x \in (𝒫 {Base}_{S} \cap Fin) \to x \in Fin$
33	32	adantl	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to x \in Fin$
34	27	ffund	$⊢ φ \to Fun F$
35	34	adantr	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to Fun F$
36	16	adantl	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to x \subseteq {Base}_{S}$
37	27	fdmd	$⊢ φ \to dom F = {Base}_{S}$
38	37	adantr	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to dom F = {Base}_{S}$
39	36 38	sseqtrrd	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to x \subseteq dom F$
40		fores	$⊢ (Fun F \land x \subseteq dom F) \to ({F ↾}_{x}) : x \underset{onto}{⟶} F [x]$
41	35 39 40	syl2anc	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to ({F ↾}_{x}) : x \underset{onto}{⟶} F [x]$
42		fofi	$⊢ (x \in Fin \land ({F ↾}_{x}) : x \underset{onto}{⟶} F [x]) \to F [x] \in Fin$
43	33 41 42	syl2anc	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to F [x] \in Fin$
44		eqid	$⊢ T ↾_{𝑠} LSpan (T) (F [x]) = T ↾_{𝑠} LSpan (T) (F [x])$
45	17 25 44	islssfgi	$⊢ (T \in LMod \land F [x] \subseteq {Base}_{T} \land F [x] \in Fin) \to T ↾_{𝑠} LSpan (T) (F [x]) \in LFinGen$
46	23 30 43 45	syl3anc	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to T ↾_{𝑠} LSpan (T) (F [x]) \in LFinGen$
47	20 46	eqeltrd	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to T ↾_{𝑠} F [LSpan (S) (x)] \in LFinGen$
48		imaeq2	$⊢ LSpan (S) (x) = A \to F [LSpan (S) (x)] = F [A]$
49	48	oveq2d	$⊢ LSpan (S) (x) = A \to T ↾_{𝑠} F [LSpan (S) (x)] = T ↾_{𝑠} F [A]$
50	49	eleq1d	$⊢ LSpan (S) (x) = A \to (T ↾_{𝑠} F [LSpan (S) (x)] \in LFinGen \leftrightarrow T ↾_{𝑠} F [A] \in LFinGen)$
51	47 50	syl5ibcom	$⊢ (φ \land x \in (𝒫 {Base}_{S} \cap Fin)) \to (LSpan (S) (x) = A \to T ↾_{𝑠} F [A] \in LFinGen)$
52	51	rexlimdva	$⊢ φ \to (\exists x \in (𝒫 {Base}_{S} \cap Fin) LSpan (S) (x) = A \to T ↾_{𝑠} F [A] \in LFinGen)$
53	13 52	mpd	$⊢ φ \to T ↾_{𝑠} F [A] \in LFinGen$
54	1 53	eqeltrid	$⊢ φ \to Y \in LFinGen$

Metamath Proof Explorer

Theorem lmhmfgima

Proof