Metamath Proof Explorer

Theorem islssfg

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

Ref Expression
Hypotheses islssfg.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
islssfg.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
islssfg.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion islssfg ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑏 ∈ 𝒫 𝑈 ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 islssfg.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2 islssfg.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 islssfg.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5 4 2 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
6 1 4 ressbas2 ⊢ ( 𝑈 ⊆ ( Base ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑋 ) )
7 5 6 syl ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 = ( Base ‘ 𝑋 ) )
8 7 pweqd ⊢ ( 𝑈 ∈ 𝑆 → 𝒫 𝑈 = 𝒫 ( Base ‘ 𝑋 ) )
9 8 rexeqdv ⊢ ( 𝑈 ∈ 𝑆 → ( ∃ 𝑏 ∈ 𝒫 𝑈 ( 𝑏 ∈ Fin ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) ↔ ∃ 𝑏 ∈ 𝒫 ( Base ‘ 𝑋 ) ( 𝑏 ∈ Fin ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) ) )
10 9 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ∃ 𝑏 ∈ 𝒫 𝑈 ( 𝑏 ∈ Fin ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) ↔ ∃ 𝑏 ∈ 𝒫 ( Base ‘ 𝑋 ) ( 𝑏 ∈ Fin ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) ) )
11 elpwi ⊢ ( 𝑏 ∈ 𝒫 𝑈 → 𝑏 ⊆ 𝑈 )
12 eqid ⊢ ( LSpan ‘ 𝑋 ) = ( LSpan ‘ 𝑋 )
13 1 3 12 2 lsslsp ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑏 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝑏 ) = ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) )
14 13 3expa ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑏 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝑏 ) = ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) )
15 11 14 sylan2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝒫 𝑈 ) → ( 𝑁 ‘ 𝑏 ) = ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) )
16 7 ad2antlr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝒫 𝑈 ) → 𝑈 = ( Base ‘ 𝑋 ) )
17 15 16 eqeq12d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝒫 𝑈 ) → ( ( 𝑁 ‘ 𝑏 ) = 𝑈 ↔ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) )
18 17 anbi2d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝒫 𝑈 ) → ( ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ↔ ( 𝑏 ∈ Fin ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) ) )
19 18 rexbidva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ∃ 𝑏 ∈ 𝒫 𝑈 ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ↔ ∃ 𝑏 ∈ 𝒫 𝑈 ( 𝑏 ∈ Fin ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) ) )
20 1 2 lsslmod ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ LMod )
21 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
22 21 12 islmodfg ⊢ ( 𝑋 ∈ LMod → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑏 ∈ 𝒫 ( Base ‘ 𝑋 ) ( 𝑏 ∈ Fin ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) ) )
23 20 22 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑏 ∈ 𝒫 ( Base ‘ 𝑋 ) ( 𝑏 ∈ Fin ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) ) )
24 10 19 23 3bitr4rd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑏 ∈ 𝒫 𝑈 ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ) )