islssfg2

Description: Property of a finitely generated left (sub)module, with a relaxed constraint on the spanning vectors. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	islssfg.x	$⊢ X = W ↾_{𝑠} U$
	islssfg.s	$⊢ S = LSubSp (W)$
	islssfg.n	$⊢ N = LSpan (W)$
	islssfg2.b	$⊢ B = {Base}_{W}$
Assertion	islssfg2	$⊢ (W \in LMod \land U \in S) \to (X \in LFinGen \leftrightarrow \exists b \in (𝒫 B \cap Fin) 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		islssfg2.b	$⊢ B = {Base}_{W}$
5	1 2 3	islssfg	$⊢ (W \in LMod \land U \in S) \to (X \in LFinGen \leftrightarrow \exists b \in 𝒫 U (b \in Fin \land N (b) = U))$
6	4 2	lssss	$⊢ N (b) \in S \to N (b) \subseteq B$
7	6	adantl	$⊢ (W \in LMod \land N (b) \in S) \to N (b) \subseteq B$
8		sstr2	$⊢ b \subseteq N (b) \to (N (b) \subseteq B \to b \subseteq B)$
9	7 8	mpan9	$⊢ ((W \in LMod \land N (b) \in S) \land b \subseteq N (b)) \to b \subseteq B$
10	4 3	lspssid	$⊢ (W \in LMod \land b \subseteq B) \to b \subseteq N (b)$
11	10	adantlr	$⊢ ((W \in LMod \land N (b) \in S) \land b \subseteq B) \to b \subseteq N (b)$
12	9 11	impbida	$⊢ (W \in LMod \land N (b) \in S) \to (b \subseteq N (b) \leftrightarrow b \subseteq B)$
13		vex	$⊢ b \in V$
14	13	elpw	$⊢ b \in 𝒫 N (b) \leftrightarrow b \subseteq N (b)$
15	13	elpw	$⊢ b \in 𝒫 B \leftrightarrow b \subseteq B$
16	12 14 15	3bitr4g	$⊢ (W \in LMod \land N (b) \in S) \to (b \in 𝒫 N (b) \leftrightarrow b \in 𝒫 B)$
17		eleq1	$⊢ N (b) = U \to (N (b) \in S \leftrightarrow U \in S)$
18	17	anbi2d	$⊢ N (b) = U \to ((W \in LMod \land N (b) \in S) \leftrightarrow (W \in LMod \land U \in S))$
19		pweq	$⊢ N (b) = U \to 𝒫 N (b) = 𝒫 U$
20	19	eleq2d	$⊢ N (b) = U \to (b \in 𝒫 N (b) \leftrightarrow b \in 𝒫 U)$
21	20	bibi1d	$⊢ N (b) = U \to ((b \in 𝒫 N (b) \leftrightarrow b \in 𝒫 B) \leftrightarrow (b \in 𝒫 U \leftrightarrow b \in 𝒫 B))$
22	18 21	imbi12d	$⊢ N (b) = U \to (((W \in LMod \land N (b) \in S) \to (b \in 𝒫 N (b) \leftrightarrow b \in 𝒫 B)) \leftrightarrow ((W \in LMod \land U \in S) \to (b \in 𝒫 U \leftrightarrow b \in 𝒫 B)))$
23	16 22	mpbii	$⊢ N (b) = U \to ((W \in LMod \land U \in S) \to (b \in 𝒫 U \leftrightarrow b \in 𝒫 B))$
24	23	com12	$⊢ (W \in LMod \land U \in S) \to (N (b) = U \to (b \in 𝒫 U \leftrightarrow b \in 𝒫 B))$
25	24	adantld	$⊢ (W \in LMod \land U \in S) \to ((b \in Fin \land N (b) = U) \to (b \in 𝒫 U \leftrightarrow b \in 𝒫 B))$
26	25	pm5.32rd	$⊢ (W \in LMod \land U \in S) \to ((b \in 𝒫 U \land (b \in Fin \land N (b) = U)) \leftrightarrow (b \in 𝒫 B \land (b \in Fin \land N (b) = U)))$
27		elin	$⊢ b \in (𝒫 B \cap Fin) \leftrightarrow (b \in 𝒫 B \land b \in Fin)$
28	27	anbi1i	$⊢ (b \in (𝒫 B \cap Fin) \land N (b) = U) \leftrightarrow ((b \in 𝒫 B \land b \in Fin) \land N (b) = U)$
29		anass	$⊢ ((b \in 𝒫 B \land b \in Fin) \land N (b) = U) \leftrightarrow (b \in 𝒫 B \land (b \in Fin \land N (b) = U))$
30	28 29	bitr2i	$⊢ (b \in 𝒫 B \land (b \in Fin \land N (b) = U)) \leftrightarrow (b \in (𝒫 B \cap Fin) \land N (b) = U)$
31	26 30	bitrdi	$⊢ (W \in LMod \land U \in S) \to ((b \in 𝒫 U \land (b \in Fin \land N (b) = U)) \leftrightarrow (b \in (𝒫 B \cap Fin) \land N (b) = U))$
32	31	rexbidv2	$⊢ (W \in LMod \land U \in S) \to (\exists b \in 𝒫 U (b \in Fin \land N (b) = U) \leftrightarrow \exists b \in (𝒫 B \cap Fin) N (b) = U)$
33	5 32	bitrd	$⊢ (W \in LMod \land U \in S) \to (X \in LFinGen \leftrightarrow \exists b \in (𝒫 B \cap Fin) N (b) = U)$

Metamath Proof Explorer

Theorem islssfg2

Proof