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 𝐵 = ( Base ‘ 𝑊 )
islmodfg.n 𝑁 = ( LSpan ‘ 𝑊 )
Assertion islmodfg ( 𝑊 ∈ LMod → ( 𝑊 ∈ LFinGen ↔ ∃ 𝑏 ∈ 𝒫 𝐵 ( 𝑏 ∈ Fin ∧ ( 𝑁𝑏 ) = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 islmodfg.b 𝐵 = ( Base ‘ 𝑊 )
2 islmodfg.n 𝑁 = ( LSpan ‘ 𝑊 )
3 df-lfig LFinGen = { 𝑎 ∈ LMod ∣ ( Base ‘ 𝑎 ) ∈ ( ( LSpan ‘ 𝑎 ) “ ( 𝒫 ( Base ‘ 𝑎 ) ∩ Fin ) ) }
4 3 eleq2i ( 𝑊 ∈ LFinGen ↔ 𝑊 ∈ { 𝑎 ∈ LMod ∣ ( Base ‘ 𝑎 ) ∈ ( ( LSpan ‘ 𝑎 ) “ ( 𝒫 ( Base ‘ 𝑎 ) ∩ Fin ) ) } )
5 fveq2 ( 𝑎 = 𝑊 → ( Base ‘ 𝑎 ) = ( Base ‘ 𝑊 ) )
6 fveq2 ( 𝑎 = 𝑊 → ( LSpan ‘ 𝑎 ) = ( LSpan ‘ 𝑊 ) )
7 6 2 eqtr4di ( 𝑎 = 𝑊 → ( LSpan ‘ 𝑎 ) = 𝑁 )
8 5 pweqd ( 𝑎 = 𝑊 → 𝒫 ( Base ‘ 𝑎 ) = 𝒫 ( Base ‘ 𝑊 ) )
9 8 ineq1d ( 𝑎 = 𝑊 → ( 𝒫 ( Base ‘ 𝑎 ) ∩ Fin ) = ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) )
10 7 9 imaeq12d ( 𝑎 = 𝑊 → ( ( LSpan ‘ 𝑎 ) “ ( 𝒫 ( Base ‘ 𝑎 ) ∩ Fin ) ) = ( 𝑁 “ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ) )
11 5 10 eleq12d ( 𝑎 = 𝑊 → ( ( Base ‘ 𝑎 ) ∈ ( ( LSpan ‘ 𝑎 ) “ ( 𝒫 ( Base ‘ 𝑎 ) ∩ Fin ) ) ↔ ( Base ‘ 𝑊 ) ∈ ( 𝑁 “ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ) ) )
12 11 elrab3 ( 𝑊 ∈ LMod → ( 𝑊 ∈ { 𝑎 ∈ LMod ∣ ( Base ‘ 𝑎 ) ∈ ( ( LSpan ‘ 𝑎 ) “ ( 𝒫 ( Base ‘ 𝑎 ) ∩ Fin ) ) } ↔ ( Base ‘ 𝑊 ) ∈ ( 𝑁 “ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ) ) )
13 4 12 syl5bb ( 𝑊 ∈ LMod → ( 𝑊 ∈ LFinGen ↔ ( Base ‘ 𝑊 ) ∈ ( 𝑁 “ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ) ) )
14 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
15 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
16 14 15 2 lspf ( 𝑊 ∈ LMod → 𝑁 : 𝒫 ( Base ‘ 𝑊 ) ⟶ ( LSubSp ‘ 𝑊 ) )
17 16 ffnd ( 𝑊 ∈ LMod → 𝑁 Fn 𝒫 ( Base ‘ 𝑊 ) )
18 inss1 ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ⊆ 𝒫 ( Base ‘ 𝑊 )
19 fvelimab ( ( 𝑁 Fn 𝒫 ( Base ‘ 𝑊 ) ∧ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ⊆ 𝒫 ( Base ‘ 𝑊 ) ) → ( ( Base ‘ 𝑊 ) ∈ ( 𝑁 “ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ) ↔ ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ( 𝑁𝑏 ) = ( Base ‘ 𝑊 ) ) )
20 17 18 19 sylancl ( 𝑊 ∈ LMod → ( ( Base ‘ 𝑊 ) ∈ ( 𝑁 “ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ) ↔ ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ( 𝑁𝑏 ) = ( Base ‘ 𝑊 ) ) )
21 elin ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ↔ ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑊 ) ∧ 𝑏 ∈ Fin ) )
22 1 eqcomi ( Base ‘ 𝑊 ) = 𝐵
23 22 pweqi 𝒫 ( Base ‘ 𝑊 ) = 𝒫 𝐵
24 23 eleq2i ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑊 ) ↔ 𝑏 ∈ 𝒫 𝐵 )
25 24 anbi1i ( ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑊 ) ∧ 𝑏 ∈ Fin ) ↔ ( 𝑏 ∈ 𝒫 𝐵𝑏 ∈ Fin ) )
26 21 25 bitri ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ↔ ( 𝑏 ∈ 𝒫 𝐵𝑏 ∈ Fin ) )
27 22 eqeq2i ( ( 𝑁𝑏 ) = ( Base ‘ 𝑊 ) ↔ ( 𝑁𝑏 ) = 𝐵 )
28 26 27 anbi12i ( ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ∧ ( 𝑁𝑏 ) = ( Base ‘ 𝑊 ) ) ↔ ( ( 𝑏 ∈ 𝒫 𝐵𝑏 ∈ Fin ) ∧ ( 𝑁𝑏 ) = 𝐵 ) )
29 anass ( ( ( 𝑏 ∈ 𝒫 𝐵𝑏 ∈ Fin ) ∧ ( 𝑁𝑏 ) = 𝐵 ) ↔ ( 𝑏 ∈ 𝒫 𝐵 ∧ ( 𝑏 ∈ Fin ∧ ( 𝑁𝑏 ) = 𝐵 ) ) )
30 28 29 bitri ( ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ∧ ( 𝑁𝑏 ) = ( Base ‘ 𝑊 ) ) ↔ ( 𝑏 ∈ 𝒫 𝐵 ∧ ( 𝑏 ∈ Fin ∧ ( 𝑁𝑏 ) = 𝐵 ) ) )
31 30 rexbii2 ( ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ( 𝑁𝑏 ) = ( Base ‘ 𝑊 ) ↔ ∃ 𝑏 ∈ 𝒫 𝐵 ( 𝑏 ∈ Fin ∧ ( 𝑁𝑏 ) = 𝐵 ) )
32 20 31 bitrdi ( 𝑊 ∈ LMod → ( ( Base ‘ 𝑊 ) ∈ ( 𝑁 “ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ) ↔ ∃ 𝑏 ∈ 𝒫 𝐵 ( 𝑏 ∈ Fin ∧ ( 𝑁𝑏 ) = 𝐵 ) ) )
33 13 32 bitrd ( 𝑊 ∈ LMod → ( 𝑊 ∈ LFinGen ↔ ∃ 𝑏 ∈ 𝒫 𝐵 ( 𝑏 ∈ Fin ∧ ( 𝑁𝑏 ) = 𝐵 ) ) )