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 = LSubSp W
islssfg.n N = LSpan W
islssfg2.b B = Base W
Assertion islssfg2 W LMod U S X LFinGen b 𝒫 B 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 LMod U S X LFinGen b 𝒫 U b Fin N b = U
6 4 2 lssss N b S N b B
7 6 adantl W LMod N b S N b B
8 sstr2 b N b N b B b B
9 7 8 mpan9 W LMod N b S b N b b B
10 4 3 lspssid W LMod b B b N b
11 10 adantlr W LMod N b S b B b N b
12 9 11 impbida W LMod N b S b N b b B
13 vex b V
14 13 elpw b 𝒫 N b b N b
15 13 elpw b 𝒫 B b B
16 12 14 15 3bitr4g W LMod N b S b 𝒫 N b b 𝒫 B
17 eleq1 N b = U N b S U S
18 17 anbi2d N b = U W LMod N b S W LMod U S
19 pweq N b = U 𝒫 N b = 𝒫 U
20 19 eleq2d N b = U b 𝒫 N b b 𝒫 U
21 20 bibi1d N b = U b 𝒫 N b b 𝒫 B b 𝒫 U b 𝒫 B
22 18 21 imbi12d N b = U W LMod N b S b 𝒫 N b b 𝒫 B W LMod U S b 𝒫 U b 𝒫 B
23 16 22 mpbii N b = U W LMod U S b 𝒫 U b 𝒫 B
24 23 com12 W LMod U S N b = U b 𝒫 U b 𝒫 B
25 24 adantld W LMod U S b Fin N b = U b 𝒫 U b 𝒫 B
26 25 pm5.32rd W LMod U S b 𝒫 U b Fin N b = U b 𝒫 B b Fin N b = U
27 elin b 𝒫 B Fin b 𝒫 B b Fin
28 27 anbi1i b 𝒫 B Fin N b = U b 𝒫 B b Fin N b = U
29 anass b 𝒫 B b Fin N b = U b 𝒫 B b Fin N b = U
30 28 29 bitr2i b 𝒫 B b Fin N b = U b 𝒫 B Fin N b = U
31 26 30 bitrdi W LMod U S b 𝒫 U b Fin N b = U b 𝒫 B Fin N b = U
32 31 rexbidv2 W LMod U S b 𝒫 U b Fin N b = U b 𝒫 B Fin N b = U
33 5 32 bitrd W LMod U S X LFinGen b 𝒫 B Fin N b = U