# Metamath Proof Explorer

## Theorem 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}=\mathrm{LSubSp}\left({W}\right)$
islssfg.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
islssfg2.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
Assertion islssfg2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \left({X}\in \mathrm{LFinGen}↔\exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{N}\left({b}\right)={U}\right)$

### Proof

Step Hyp Ref Expression
1 islssfg.x ${⊢}{X}={W}{↾}_{𝑠}{U}$
2 islssfg.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
3 islssfg.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
4 islssfg2.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
5 1 2 3 islssfg ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \left({X}\in \mathrm{LFinGen}↔\exists {b}\in 𝒫{U}\phantom{\rule{.4em}{0ex}}\left({b}\in \mathrm{Fin}\wedge {N}\left({b}\right)={U}\right)\right)$
6 4 2 lssss ${⊢}{N}\left({b}\right)\in {S}\to {N}\left({b}\right)\subseteq {B}$
7 6 adantl ${⊢}\left({W}\in \mathrm{LMod}\wedge {N}\left({b}\right)\in {S}\right)\to {N}\left({b}\right)\subseteq {B}$
8 sstr2 ${⊢}{b}\subseteq {N}\left({b}\right)\to \left({N}\left({b}\right)\subseteq {B}\to {b}\subseteq {B}\right)$
9 7 8 mpan9 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {N}\left({b}\right)\in {S}\right)\wedge {b}\subseteq {N}\left({b}\right)\right)\to {b}\subseteq {B}$
10 4 3 lspssid ${⊢}\left({W}\in \mathrm{LMod}\wedge {b}\subseteq {B}\right)\to {b}\subseteq {N}\left({b}\right)$
11 10 adantlr ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {N}\left({b}\right)\in {S}\right)\wedge {b}\subseteq {B}\right)\to {b}\subseteq {N}\left({b}\right)$
12 9 11 impbida ${⊢}\left({W}\in \mathrm{LMod}\wedge {N}\left({b}\right)\in {S}\right)\to \left({b}\subseteq {N}\left({b}\right)↔{b}\subseteq {B}\right)$
13 vex ${⊢}{b}\in \mathrm{V}$
14 13 elpw ${⊢}{b}\in 𝒫{N}\left({b}\right)↔{b}\subseteq {N}\left({b}\right)$
15 13 elpw ${⊢}{b}\in 𝒫{B}↔{b}\subseteq {B}$
16 12 14 15 3bitr4g ${⊢}\left({W}\in \mathrm{LMod}\wedge {N}\left({b}\right)\in {S}\right)\to \left({b}\in 𝒫{N}\left({b}\right)↔{b}\in 𝒫{B}\right)$
17 eleq1 ${⊢}{N}\left({b}\right)={U}\to \left({N}\left({b}\right)\in {S}↔{U}\in {S}\right)$
18 17 anbi2d ${⊢}{N}\left({b}\right)={U}\to \left(\left({W}\in \mathrm{LMod}\wedge {N}\left({b}\right)\in {S}\right)↔\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\right)$
19 pweq ${⊢}{N}\left({b}\right)={U}\to 𝒫{N}\left({b}\right)=𝒫{U}$
20 19 eleq2d ${⊢}{N}\left({b}\right)={U}\to \left({b}\in 𝒫{N}\left({b}\right)↔{b}\in 𝒫{U}\right)$
21 20 bibi1d ${⊢}{N}\left({b}\right)={U}\to \left(\left({b}\in 𝒫{N}\left({b}\right)↔{b}\in 𝒫{B}\right)↔\left({b}\in 𝒫{U}↔{b}\in 𝒫{B}\right)\right)$
22 18 21 imbi12d ${⊢}{N}\left({b}\right)={U}\to \left(\left(\left({W}\in \mathrm{LMod}\wedge {N}\left({b}\right)\in {S}\right)\to \left({b}\in 𝒫{N}\left({b}\right)↔{b}\in 𝒫{B}\right)\right)↔\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \left({b}\in 𝒫{U}↔{b}\in 𝒫{B}\right)\right)\right)$
23 16 22 mpbii ${⊢}{N}\left({b}\right)={U}\to \left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \left({b}\in 𝒫{U}↔{b}\in 𝒫{B}\right)\right)$
24 23 com12 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \left({N}\left({b}\right)={U}\to \left({b}\in 𝒫{U}↔{b}\in 𝒫{B}\right)\right)$
25 24 adantld ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \left(\left({b}\in \mathrm{Fin}\wedge {N}\left({b}\right)={U}\right)\to \left({b}\in 𝒫{U}↔{b}\in 𝒫{B}\right)\right)$
26 25 pm5.32rd ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \left(\left({b}\in 𝒫{U}\wedge \left({b}\in \mathrm{Fin}\wedge {N}\left({b}\right)={U}\right)\right)↔\left({b}\in 𝒫{B}\wedge \left({b}\in \mathrm{Fin}\wedge {N}\left({b}\right)={U}\right)\right)\right)$
27 elin ${⊢}{b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)↔\left({b}\in 𝒫{B}\wedge {b}\in \mathrm{Fin}\right)$
28 27 anbi1i ${⊢}\left({b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\wedge {N}\left({b}\right)={U}\right)↔\left(\left({b}\in 𝒫{B}\wedge {b}\in \mathrm{Fin}\right)\wedge {N}\left({b}\right)={U}\right)$
29 anass ${⊢}\left(\left({b}\in 𝒫{B}\wedge {b}\in \mathrm{Fin}\right)\wedge {N}\left({b}\right)={U}\right)↔\left({b}\in 𝒫{B}\wedge \left({b}\in \mathrm{Fin}\wedge {N}\left({b}\right)={U}\right)\right)$
30 28 29 bitr2i ${⊢}\left({b}\in 𝒫{B}\wedge \left({b}\in \mathrm{Fin}\wedge {N}\left({b}\right)={U}\right)\right)↔\left({b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\wedge {N}\left({b}\right)={U}\right)$
31 26 30 syl6bb ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \left(\left({b}\in 𝒫{U}\wedge \left({b}\in \mathrm{Fin}\wedge {N}\left({b}\right)={U}\right)\right)↔\left({b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\wedge {N}\left({b}\right)={U}\right)\right)$
32 31 rexbidv2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \left(\exists {b}\in 𝒫{U}\phantom{\rule{.4em}{0ex}}\left({b}\in \mathrm{Fin}\wedge {N}\left({b}\right)={U}\right)↔\exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{N}\left({b}\right)={U}\right)$
33 5 32 bitrd ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \left({X}\in \mathrm{LFinGen}↔\exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{N}\left({b}\right)={U}\right)$