This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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