lsmfgcl

Description: The sum of two finitely generated submodules is finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	lsmfgcl.u	$⊢ U = LSubSp (W)$
	lsmfgcl.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lsmfgcl.d	$⊢ D = W ↾_{𝑠} A$
	lsmfgcl.e	$⊢ E = W ↾_{𝑠} B$
	lsmfgcl.f	$⊢ F = W ↾_{𝑠} (A \underset{˙}{\oplus} B)$
	lsmfgcl.w	$⊢ φ \to W \in LMod$
	lsmfgcl.a	$⊢ φ \to A \in U$
	lsmfgcl.b	$⊢ φ \to B \in U$
	lsmfgcl.df	$⊢ φ \to D \in LFinGen$
	lsmfgcl.ef	$⊢ φ \to E \in LFinGen$
Assertion	lsmfgcl	$⊢ φ \to F \in LFinGen$

Proof

Step	Hyp	Ref	Expression
1		lsmfgcl.u	$⊢ U = LSubSp (W)$
2		lsmfgcl.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		lsmfgcl.d	$⊢ D = W ↾_{𝑠} A$
4		lsmfgcl.e	$⊢ E = W ↾_{𝑠} B$
5		lsmfgcl.f	$⊢ F = W ↾_{𝑠} (A \underset{˙}{\oplus} B)$
6		lsmfgcl.w	$⊢ φ \to W \in LMod$
7		lsmfgcl.a	$⊢ φ \to A \in U$
8		lsmfgcl.b	$⊢ φ \to B \in U$
9		lsmfgcl.df	$⊢ φ \to D \in LFinGen$
10		lsmfgcl.ef	$⊢ φ \to E \in LFinGen$
11		eqid	$⊢ LSpan (W) = LSpan (W)$
12		eqid	$⊢ {Base}_{W} = {Base}_{W}$
13	3 1 11 12	islssfg2	$⊢ (W \in LMod \land A \in U) \to (D \in LFinGen \leftrightarrow \exists a \in (𝒫 {Base}_{W} \cap Fin) LSpan (W) (a) = A)$
14	6 7 13	syl2anc	$⊢ φ \to (D \in LFinGen \leftrightarrow \exists a \in (𝒫 {Base}_{W} \cap Fin) LSpan (W) (a) = A)$
15	9 14	mpbid	$⊢ φ \to \exists a \in (𝒫 {Base}_{W} \cap Fin) LSpan (W) (a) = A$
16	4 1 11 12	islssfg2	$⊢ (W \in LMod \land B \in U) \to (E \in LFinGen \leftrightarrow \exists b \in (𝒫 {Base}_{W} \cap Fin) LSpan (W) (b) = B)$
17	6 8 16	syl2anc	$⊢ φ \to (E \in LFinGen \leftrightarrow \exists b \in (𝒫 {Base}_{W} \cap Fin) LSpan (W) (b) = B)$
18	10 17	mpbid	$⊢ φ \to \exists b \in (𝒫 {Base}_{W} \cap Fin) LSpan (W) (b) = B$
19	18	adantr	$⊢ (φ \land a \in (𝒫 {Base}_{W} \cap Fin)) \to \exists b \in (𝒫 {Base}_{W} \cap Fin) LSpan (W) (b) = B$
20		inss1	$⊢ 𝒫 {Base}_{W} \cap Fin \subseteq 𝒫 {Base}_{W}$
21	20	sseli	$⊢ a \in (𝒫 {Base}_{W} \cap Fin) \to a \in 𝒫 {Base}_{W}$
22	21	elpwid	$⊢ a \in (𝒫 {Base}_{W} \cap Fin) \to a \subseteq {Base}_{W}$
23	20	sseli	$⊢ b \in (𝒫 {Base}_{W} \cap Fin) \to b \in 𝒫 {Base}_{W}$
24	23	elpwid	$⊢ b \in (𝒫 {Base}_{W} \cap Fin) \to b \subseteq {Base}_{W}$
25	12 11 2	lsmsp2	$⊢ (W \in LMod \land a \subseteq {Base}_{W} \land b \subseteq {Base}_{W}) \to LSpan (W) (a) \underset{˙}{\oplus} LSpan (W) (b) = LSpan (W) (a \cup b)$
26	6 22 24 25	syl3an	$⊢ (φ \land a \in (𝒫 {Base}_{W} \cap Fin) \land b \in (𝒫 {Base}_{W} \cap Fin)) \to LSpan (W) (a) \underset{˙}{\oplus} LSpan (W) (b) = LSpan (W) (a \cup b)$
27	26	3expb	$⊢ (φ \land (a \in (𝒫 {Base}_{W} \cap Fin) \land b \in (𝒫 {Base}_{W} \cap Fin))) \to LSpan (W) (a) \underset{˙}{\oplus} LSpan (W) (b) = LSpan (W) (a \cup b)$
28	27	oveq2d	$⊢ (φ \land (a \in (𝒫 {Base}_{W} \cap Fin) \land b \in (𝒫 {Base}_{W} \cap Fin))) \to W ↾_{𝑠} (LSpan (W) (a) \underset{˙}{\oplus} LSpan (W) (b)) = W ↾_{𝑠} LSpan (W) (a \cup b)$
29	6	adantr	$⊢ (φ \land (a \in (𝒫 {Base}_{W} \cap Fin) \land b \in (𝒫 {Base}_{W} \cap Fin))) \to W \in LMod$
30		unss	$⊢ (a \subseteq {Base}_{W} \land b \subseteq {Base}_{W}) \leftrightarrow a \cup b \subseteq {Base}_{W}$
31	30	biimpi	$⊢ (a \subseteq {Base}_{W} \land b \subseteq {Base}_{W}) \to a \cup b \subseteq {Base}_{W}$
32	22 24 31	syl2an	$⊢ (a \in (𝒫 {Base}_{W} \cap Fin) \land b \in (𝒫 {Base}_{W} \cap Fin)) \to a \cup b \subseteq {Base}_{W}$
33	32	adantl	$⊢ (φ \land (a \in (𝒫 {Base}_{W} \cap Fin) \land b \in (𝒫 {Base}_{W} \cap Fin))) \to a \cup b \subseteq {Base}_{W}$
34		inss2	$⊢ 𝒫 {Base}_{W} \cap Fin \subseteq Fin$
35	34	sseli	$⊢ a \in (𝒫 {Base}_{W} \cap Fin) \to a \in Fin$
36	34	sseli	$⊢ b \in (𝒫 {Base}_{W} \cap Fin) \to b \in Fin$
37		unfi	$⊢ (a \in Fin \land b \in Fin) \to a \cup b \in Fin$
38	35 36 37	syl2an	$⊢ (a \in (𝒫 {Base}_{W} \cap Fin) \land b \in (𝒫 {Base}_{W} \cap Fin)) \to a \cup b \in Fin$
39	38	adantl	$⊢ (φ \land (a \in (𝒫 {Base}_{W} \cap Fin) \land b \in (𝒫 {Base}_{W} \cap Fin))) \to a \cup b \in Fin$
40		eqid	$⊢ W ↾_{𝑠} LSpan (W) (a \cup b) = W ↾_{𝑠} LSpan (W) (a \cup b)$
41	11 12 40	islssfgi	$⊢ (W \in LMod \land a \cup b \subseteq {Base}_{W} \land a \cup b \in Fin) \to W ↾_{𝑠} LSpan (W) (a \cup b) \in LFinGen$
42	29 33 39 41	syl3anc	$⊢ (φ \land (a \in (𝒫 {Base}_{W} \cap Fin) \land b \in (𝒫 {Base}_{W} \cap Fin))) \to W ↾_{𝑠} LSpan (W) (a \cup b) \in LFinGen$
43	28 42	eqeltrd	$⊢ (φ \land (a \in (𝒫 {Base}_{W} \cap Fin) \land b \in (𝒫 {Base}_{W} \cap Fin))) \to W ↾_{𝑠} (LSpan (W) (a) \underset{˙}{\oplus} LSpan (W) (b)) \in LFinGen$
44	43	anassrs	$⊢ ((φ \land a \in (𝒫 {Base}_{W} \cap Fin)) \land b \in (𝒫 {Base}_{W} \cap Fin)) \to W ↾_{𝑠} (LSpan (W) (a) \underset{˙}{\oplus} LSpan (W) (b)) \in LFinGen$
45		oveq2	$⊢ LSpan (W) (b) = B \to LSpan (W) (a) \underset{˙}{\oplus} LSpan (W) (b) = LSpan (W) (a) \underset{˙}{\oplus} B$
46	45	oveq2d	$⊢ LSpan (W) (b) = B \to W ↾_{𝑠} (LSpan (W) (a) \underset{˙}{\oplus} LSpan (W) (b)) = W ↾_{𝑠} (LSpan (W) (a) \underset{˙}{\oplus} B)$
47	46	eleq1d	$⊢ LSpan (W) (b) = B \to (W ↾_{𝑠} (LSpan (W) (a) \underset{˙}{\oplus} LSpan (W) (b)) \in LFinGen \leftrightarrow W ↾_{𝑠} (LSpan (W) (a) \underset{˙}{\oplus} B) \in LFinGen)$
48	44 47	syl5ibcom	$⊢ ((φ \land a \in (𝒫 {Base}_{W} \cap Fin)) \land b \in (𝒫 {Base}_{W} \cap Fin)) \to (LSpan (W) (b) = B \to W ↾_{𝑠} (LSpan (W) (a) \underset{˙}{\oplus} B) \in LFinGen)$
49	48	rexlimdva	$⊢ (φ \land a \in (𝒫 {Base}_{W} \cap Fin)) \to (\exists b \in (𝒫 {Base}_{W} \cap Fin) LSpan (W) (b) = B \to W ↾_{𝑠} (LSpan (W) (a) \underset{˙}{\oplus} B) \in LFinGen)$
50	19 49	mpd	$⊢ (φ \land a \in (𝒫 {Base}_{W} \cap Fin)) \to W ↾_{𝑠} (LSpan (W) (a) \underset{˙}{\oplus} B) \in LFinGen$
51		oveq1	$⊢ LSpan (W) (a) = A \to LSpan (W) (a) \underset{˙}{\oplus} B = A \underset{˙}{\oplus} B$
52	51	oveq2d	$⊢ LSpan (W) (a) = A \to W ↾_{𝑠} (LSpan (W) (a) \underset{˙}{\oplus} B) = W ↾_{𝑠} (A \underset{˙}{\oplus} B)$
53	52	eleq1d	$⊢ LSpan (W) (a) = A \to (W ↾_{𝑠} (LSpan (W) (a) \underset{˙}{\oplus} B) \in LFinGen \leftrightarrow W ↾_{𝑠} (A \underset{˙}{\oplus} B) \in LFinGen)$
54	50 53	syl5ibcom	$⊢ (φ \land a \in (𝒫 {Base}_{W} \cap Fin)) \to (LSpan (W) (a) = A \to W ↾_{𝑠} (A \underset{˙}{\oplus} B) \in LFinGen)$
55	54	rexlimdva	$⊢ φ \to (\exists a \in (𝒫 {Base}_{W} \cap Fin) LSpan (W) (a) = A \to W ↾_{𝑠} (A \underset{˙}{\oplus} B) \in LFinGen)$
56	15 55	mpd	$⊢ φ \to W ↾_{𝑠} (A \underset{˙}{\oplus} B) \in LFinGen$
57	5 56	eqeltrid	$⊢ φ \to F \in LFinGen$

Metamath Proof Explorer

Theorem lsmfgcl

Proof