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	bitrid	⊢ ( 𝑊 ∈ 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 ∧ ( 𝑁 ‘ 𝑏 ) = 𝐵 ) ) )