Metamath Proof Explorer


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 ) ) )