Metamath Proof Explorer

Theorem islssfg2

Description: Property of a finitely generated left (sub)module, with a relaxed constraint on the spanning vectors. (Contributed by Stefan O'Rear, 24-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 islssfg.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2 islssfg.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 islssfg.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 islssfg2.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
5 1 2 3 islssfg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑏 ∈ 𝒫 𝑈 ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ) )
6 4 2 lssss ⊢ ( ( 𝑁 ‘ 𝑏 ) ∈ 𝑆 → ( 𝑁 ‘ 𝑏 ) ⊆ 𝐵 )
7 6 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑏 ) ∈ 𝑆 ) → ( 𝑁 ‘ 𝑏 ) ⊆ 𝐵 )
8 sstr2 ⊢ ( 𝑏 ⊆ ( 𝑁 ‘ 𝑏 ) → ( ( 𝑁 ‘ 𝑏 ) ⊆ 𝐵 → 𝑏 ⊆ 𝐵 ) )
9 7 8 mpan9 ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑏 ) ∈ 𝑆 ) ∧ 𝑏 ⊆ ( 𝑁 ‘ 𝑏 ) ) → 𝑏 ⊆ 𝐵 )
10 4 3 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑏 ⊆ 𝐵 ) → 𝑏 ⊆ ( 𝑁 ‘ 𝑏 ) )
11 10 adantlr ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑏 ) ∈ 𝑆 ) ∧ 𝑏 ⊆ 𝐵 ) → 𝑏 ⊆ ( 𝑁 ‘ 𝑏 ) )
12 9 11 impbida ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑏 ) ∈ 𝑆 ) → ( 𝑏 ⊆ ( 𝑁 ‘ 𝑏 ) ↔ 𝑏 ⊆ 𝐵 ) )
13 vex ⊢ 𝑏 ∈ V
14 13 elpw ⊢ ( 𝑏 ∈ 𝒫 ( 𝑁 ‘ 𝑏 ) ↔ 𝑏 ⊆ ( 𝑁 ‘ 𝑏 ) )
15 13 elpw ⊢ ( 𝑏 ∈ 𝒫 𝐵 ↔ 𝑏 ⊆ 𝐵 )
16 12 14 15 3bitr4g ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑏 ) ∈ 𝑆 ) → ( 𝑏 ∈ 𝒫 ( 𝑁 ‘ 𝑏 ) ↔ 𝑏 ∈ 𝒫 𝐵 ) )
17 eleq1 ⊢ ( ( 𝑁 ‘ 𝑏 ) = 𝑈 → ( ( 𝑁 ‘ 𝑏 ) ∈ 𝑆 ↔ 𝑈 ∈ 𝑆 ) )
18 17 anbi2d ⊢ ( ( 𝑁 ‘ 𝑏 ) = 𝑈 → ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑏 ) ∈ 𝑆 ) ↔ ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ) )
19 pweq ⊢ ( ( 𝑁 ‘ 𝑏 ) = 𝑈 → 𝒫 ( 𝑁 ‘ 𝑏 ) = 𝒫 𝑈 )
20 19 eleq2d ⊢ ( ( 𝑁 ‘ 𝑏 ) = 𝑈 → ( 𝑏 ∈ 𝒫 ( 𝑁 ‘ 𝑏 ) ↔ 𝑏 ∈ 𝒫 𝑈 ) )
21 20 bibi1d ⊢ ( ( 𝑁 ‘ 𝑏 ) = 𝑈 → ( ( 𝑏 ∈ 𝒫 ( 𝑁 ‘ 𝑏 ) ↔ 𝑏 ∈ 𝒫 𝐵 ) ↔ ( 𝑏 ∈ 𝒫 𝑈 ↔ 𝑏 ∈ 𝒫 𝐵 ) ) )
22 18 21 imbi12d ⊢ ( ( 𝑁 ‘ 𝑏 ) = 𝑈 → ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑏 ) ∈ 𝑆 ) → ( 𝑏 ∈ 𝒫 ( 𝑁 ‘ 𝑏 ) ↔ 𝑏 ∈ 𝒫 𝐵 ) ) ↔ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑏 ∈ 𝒫 𝑈 ↔ 𝑏 ∈ 𝒫 𝐵 ) ) ) )
23 16 22 mpbii ⊢ ( ( 𝑁 ‘ 𝑏 ) = 𝑈 → ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑏 ∈ 𝒫 𝑈 ↔ 𝑏 ∈ 𝒫 𝐵 ) ) )
24 23 com12 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ( 𝑁 ‘ 𝑏 ) = 𝑈 → ( 𝑏 ∈ 𝒫 𝑈 ↔ 𝑏 ∈ 𝒫 𝐵 ) ) )
25 24 adantld ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) → ( 𝑏 ∈ 𝒫 𝑈 ↔ 𝑏 ∈ 𝒫 𝐵 ) ) )
26 25 pm5.32rd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ( 𝑏 ∈ 𝒫 𝑈 ∧ ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ) ↔ ( 𝑏 ∈ 𝒫 𝐵 ∧ ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ) ) )
27 elin ⊢ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ↔ ( 𝑏 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ Fin ) )
28 27 anbi1i ⊢ ( ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ↔ ( ( 𝑏 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ Fin ) ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) )
29 anass ⊢ ( ( ( 𝑏 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ Fin ) ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ↔ ( 𝑏 ∈ 𝒫 𝐵 ∧ ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ) )
30 28 29 bitr2i ⊢ ( ( 𝑏 ∈ 𝒫 𝐵 ∧ ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ) ↔ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) )
31 26 30 bitrdi ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ( 𝑏 ∈ 𝒫 𝑈 ∧ ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ) ↔ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ) )
32 31 rexbidv2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ∃ 𝑏 ∈ 𝒫 𝑈 ( 𝑏 ∈ Fin ∧ ( 𝑁 ‘ 𝑏 ) = 𝑈 ) ↔ ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑁 ‘ 𝑏 ) = 𝑈 ) )
33 5 32 bitrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑁 ‘ 𝑏 ) = 𝑈 ) )