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 15 eqcomd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝒫 𝑈 ) → ( 𝑁 ‘ 𝑏 ) = ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) )
17 7 ad2antlr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝒫 𝑈 ) → 𝑈 = ( Base ‘ 𝑋 ) )
18 16 17 eqeq12d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝒫 𝑈 ) → ( ( 𝑁 ‘ 𝑏 ) = 𝑈 ↔ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) )
19 18 anbi2d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝒫 𝑈 ) → ( ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ↔ ( 𝑏 ∈ Fin ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) ) )
20 19 rexbidva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ∃ 𝑏 ∈ 𝒫 𝑈 ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ↔ ∃ 𝑏 ∈ 𝒫 𝑈 ( 𝑏 ∈ Fin ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) ) )
21 1 2 lsslmod ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ LMod )
22 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
23 22 12 islmodfg ⊢ ( 𝑋 ∈ LMod → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑏 ∈ 𝒫 ( Base ‘ 𝑋 ) ( 𝑏 ∈ Fin ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) ) )
24 21 23 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑏 ∈ 𝒫 ( Base ‘ 𝑋 ) ( 𝑏 ∈ Fin ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑏 ) = ( Base ‘ 𝑋 ) ) ) )
25 10 20 24 3bitr4rd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑏 ∈ 𝒫 𝑈 ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ) )