Metamath Proof Explorer


Theorem islmodfg

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

Ref Expression
Hypotheses islmodfg.b B = Base W
islmodfg.n N = LSpan W
Assertion islmodfg W LMod W LFinGen b 𝒫 B b Fin N b = B

Proof

Step Hyp Ref Expression
1 islmodfg.b B = Base W
2 islmodfg.n N = LSpan W
3 df-lfig LFinGen = a LMod | Base a LSpan a 𝒫 Base a Fin
4 3 eleq2i W LFinGen W a LMod | Base a LSpan a 𝒫 Base a Fin
5 fveq2 a = W Base a = Base W
6 fveq2 a = W LSpan a = LSpan W
7 6 2 eqtr4di a = W LSpan a = N
8 5 pweqd a = W 𝒫 Base a = 𝒫 Base W
9 8 ineq1d a = W 𝒫 Base a Fin = 𝒫 Base W Fin
10 7 9 imaeq12d a = W LSpan a 𝒫 Base a Fin = N 𝒫 Base W Fin
11 5 10 eleq12d a = W Base a LSpan a 𝒫 Base a Fin Base W N 𝒫 Base W Fin
12 11 elrab3 W LMod W a LMod | Base a LSpan a 𝒫 Base a Fin Base W N 𝒫 Base W Fin
13 4 12 syl5bb W LMod W LFinGen Base W N 𝒫 Base W Fin
14 eqid Base W = Base W
15 eqid LSubSp W = LSubSp W
16 14 15 2 lspf W LMod N : 𝒫 Base W LSubSp W
17 16 ffnd W LMod N Fn 𝒫 Base W
18 inss1 𝒫 Base W Fin 𝒫 Base W
19 fvelimab N Fn 𝒫 Base W 𝒫 Base W Fin 𝒫 Base W Base W N 𝒫 Base W Fin b 𝒫 Base W Fin N b = Base W
20 17 18 19 sylancl W LMod Base W N 𝒫 Base W Fin b 𝒫 Base W Fin N b = Base W
21 elin b 𝒫 Base W Fin b 𝒫 Base W b Fin
22 1 eqcomi Base W = B
23 22 pweqi 𝒫 Base W = 𝒫 B
24 23 eleq2i b 𝒫 Base W b 𝒫 B
25 24 anbi1i b 𝒫 Base W b Fin b 𝒫 B b Fin
26 21 25 bitri b 𝒫 Base W Fin b 𝒫 B b Fin
27 22 eqeq2i N b = Base W N b = B
28 26 27 anbi12i b 𝒫 Base W Fin N b = Base W b 𝒫 B b Fin N b = B
29 anass b 𝒫 B b Fin N b = B b 𝒫 B b Fin N b = B
30 28 29 bitri b 𝒫 Base W Fin N b = Base W b 𝒫 B b Fin N b = B
31 30 rexbii2 b 𝒫 Base W Fin N b = Base W b 𝒫 B b Fin N b = B
32 20 31 bitrdi W LMod Base W N 𝒫 Base W Fin b 𝒫 B b Fin N b = B
33 13 32 bitrd W LMod W LFinGen b 𝒫 B b Fin N b = B