islssfg

Description: Property of a finitely generated left (sub)module. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Hypotheses	islssfg.x	$⊢ X = W ↾_{𝑠} U$
	islssfg.s	$⊢ S = LSubSp (W)$
	islssfg.n	$⊢ N = LSpan (W)$
Assertion	islssfg	$⊢ (W \in LMod \land U \in S) \to (X \in LFinGen \leftrightarrow \exists b \in 𝒫 U (b \in Fin \land N (b) = U))$

Proof

Step	Hyp	Ref	Expression
1		islssfg.x	$⊢ X = W ↾_{𝑠} U$
2		islssfg.s	$⊢ S = LSubSp (W)$
3		islssfg.n	$⊢ N = LSpan (W)$
4		eqid	$⊢ {Base}_{W} = {Base}_{W}$
5	4 2	lssss	$⊢ U \in S \to U \subseteq {Base}_{W}$
6	1 4	ressbas2	$⊢ U \subseteq {Base}_{W} \to U = {Base}_{X}$
7	5 6	syl	$⊢ U \in S \to U = {Base}_{X}$
8	7	pweqd	$⊢ U \in S \to 𝒫 U = 𝒫 {Base}_{X}$
9	8	rexeqdv	$⊢ U \in S \to (\exists b \in 𝒫 U (b \in Fin \land LSpan (X) (b) = {Base}_{X}) \leftrightarrow \exists b \in 𝒫 {Base}_{X} (b \in Fin \land LSpan (X) (b) = {Base}_{X}))$
10	9	adantl	$⊢ (W \in LMod \land U \in S) \to (\exists b \in 𝒫 U (b \in Fin \land LSpan (X) (b) = {Base}_{X}) \leftrightarrow \exists b \in 𝒫 {Base}_{X} (b \in Fin \land LSpan (X) (b) = {Base}_{X}))$
11		elpwi	$⊢ b \in 𝒫 U \to b \subseteq U$
12		eqid	$⊢ LSpan (X) = LSpan (X)$
13	1 3 12 2	lsslsp	$⊢ (W \in LMod \land U \in S \land b \subseteq U) \to N (b) = LSpan (X) (b)$
14	13	3expa	$⊢ ((W \in LMod \land U \in S) \land b \subseteq U) \to N (b) = LSpan (X) (b)$
15	11 14	sylan2	$⊢ ((W \in LMod \land U \in S) \land b \in 𝒫 U) \to N (b) = LSpan (X) (b)$
16	7	ad2antlr	$⊢ ((W \in LMod \land U \in S) \land b \in 𝒫 U) \to U = {Base}_{X}$
17	15 16	eqeq12d	$⊢ ((W \in LMod \land U \in S) \land b \in 𝒫 U) \to (N (b) = U \leftrightarrow LSpan (X) (b) = {Base}_{X})$
18	17	anbi2d	$⊢ ((W \in LMod \land U \in S) \land b \in 𝒫 U) \to ((b \in Fin \land N (b) = U) \leftrightarrow (b \in Fin \land LSpan (X) (b) = {Base}_{X}))$
19	18	rexbidva	$⊢ (W \in LMod \land U \in S) \to (\exists b \in 𝒫 U (b \in Fin \land N (b) = U) \leftrightarrow \exists b \in 𝒫 U (b \in Fin \land LSpan (X) (b) = {Base}_{X}))$
20	1 2	lsslmod	$⊢ (W \in LMod \land U \in S) \to X \in LMod$
21		eqid	$⊢ {Base}_{X} = {Base}_{X}$
22	21 12	islmodfg	$⊢ X \in LMod \to (X \in LFinGen \leftrightarrow \exists b \in 𝒫 {Base}_{X} (b \in Fin \land LSpan (X) (b) = {Base}_{X}))$
23	20 22	syl	$⊢ (W \in LMod \land U \in S) \to (X \in LFinGen \leftrightarrow \exists b \in 𝒫 {Base}_{X} (b \in Fin \land LSpan (X) (b) = {Base}_{X}))$
24	10 19 23	3bitr4rd	$⊢ (W \in LMod \land U \in S) \to (X \in LFinGen \leftrightarrow \exists b \in 𝒫 U (b \in Fin \land N (b) = U))$

Metamath Proof Explorer

Theorem islssfg

Proof