Theorem frlmelbas

Description: Membership in the base set of the free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by AV, 23-Jun-2019)

	Ref	Expression
Hypotheses	frlmval.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlmelbas.n	⊢ 𝑁 = ( Base ‘ 𝑅 )
	frlmelbas.z	⊢ 0 = ( 0g ‘ 𝑅 )
	frlmelbas.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
Assertion	frlmelbas	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∈ ( 𝑁 ↑m 𝐼 ) ∧ 𝑋 finSupp 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		frlmelbas.n	⊢ 𝑁 = ( Base ‘ 𝑅 )
3		frlmelbas.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		frlmelbas.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
5		eqid	⊢ { 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑘 finSupp 0 } = { 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑘 finSupp 0 }
6	1 2 3 5	frlmbas	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → { 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑘 finSupp 0 } = ( Base ‘ 𝐹 ) )
7	4 6	eqtr4id	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐵 = { 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑘 finSupp 0 } )
8	7	eleq2d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ { 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑘 finSupp 0 } ) )
9		breq1	⊢ ( 𝑘 = 𝑋 → ( 𝑘 finSupp 0 ↔ 𝑋 finSupp 0 ) )
10	9	elrab	⊢ ( 𝑋 ∈ { 𝑘 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑘 finSupp 0 } ↔ ( 𝑋 ∈ ( 𝑁 ↑m 𝐼 ) ∧ 𝑋 finSupp 0 ) )
11	8 10	bitrdi	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∈ ( 𝑁 ↑m 𝐼 ) ∧ 𝑋 finSupp 0 ) ) )