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 syl6bb ⊢ ( 𝑊 ∈ LMod → ( ( Base ‘ 𝑊 ) ∈ ( 𝑁 “ ( 𝒫 ( Base ‘ 𝑊 ) ∩ Fin ) ) ↔ ∃ 𝑏 ∈ 𝒫 𝐵 ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝐵 ) ) )
33 13 32 bitrd ⊢ ( 𝑊 ∈ LMod → ( 𝑊 ∈ LFinGen ↔ ∃ 𝑏 ∈ 𝒫 𝐵 ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝐵 ) ) )