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 
|- F = ( R freeLMod I )
frlmelbas.n 
|- N = ( Base ` R )
frlmelbas.z 
|- .0. = ( 0g ` R )
frlmelbas.b 
|- B = ( Base ` F )
Assertion frlmelbas 
|- ( ( R e. V /\ I e. W ) -> ( X e. B <-> ( X e. ( N ^m I ) /\ X finSupp .0. ) ) )

Proof

Step Hyp Ref Expression
1 frlmval.f 
 |-  F = ( R freeLMod I )
2 frlmelbas.n 
 |-  N = ( Base ` R )
3 frlmelbas.z 
 |-  .0. = ( 0g ` R )
4 frlmelbas.b 
 |-  B = ( Base ` F )
5 eqid 
 |-  { k e. ( N ^m I ) | k finSupp .0. } = { k e. ( N ^m I ) | k finSupp .0. }
6 1 2 3 5 frlmbas 
 |-  ( ( R e. V /\ I e. W ) -> { k e. ( N ^m I ) | k finSupp .0. } = ( Base ` F ) )
7 4 6 eqtr4id 
 |-  ( ( R e. V /\ I e. W ) -> B = { k e. ( N ^m I ) | k finSupp .0. } )
8 7 eleq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( X e. B <-> X e. { k e. ( N ^m I ) | k finSupp .0. } ) )
9 breq1 
 |-  ( k = X -> ( k finSupp .0. <-> X finSupp .0. ) )
10 9 elrab 
 |-  ( X e. { k e. ( N ^m I ) | k finSupp .0. } <-> ( X e. ( N ^m I ) /\ X finSupp .0. ) )
11 8 10 bitrdi 
 |-  ( ( R e. V /\ I e. W ) -> ( X e. B <-> ( X e. ( N ^m I ) /\ X finSupp .0. ) ) )