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

Metamath Proof Explorer

Theorem frlmbasfsupp

Description: Elements of the free module are finitely supported. (Contributed by Stefan O'Rear, 3-Feb-2015) (Revised by Thierry Arnoux, 21-Jun-2019) (Proof shortened by AV, 20-Jul-2019)

Ref Expression
Hypotheses frlmval.f 
|- F = ( R freeLMod I )
frlmbasfsupp.z 
|- .0. = ( 0g ` R )
frlmbasfsupp.b 
|- B = ( Base ` F )
Assertion frlmbasfsupp 
|- ( ( I e. W /\ X e. B ) -> X finSupp .0. )

Proof

Step Hyp Ref Expression
1 frlmval.f 
 |-  F = ( R freeLMod I )
2 frlmbasfsupp.z 
 |-  .0. = ( 0g ` R )
3 frlmbasfsupp.b 
 |-  B = ( Base ` F )
4 simpr 
 |-  ( ( I e. W /\ X e. B ) -> X e. B )
5 1 3 frlmrcl 
 |-  ( X e. B -> R e. _V )
6 simpl 
 |-  ( ( I e. W /\ X e. B ) -> I e. W )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 1 7 2 3 frlmelbas 
 |-  ( ( R e. _V /\ I e. W ) -> ( X e. B <-> ( X e. ( ( Base ` R ) ^m I ) /\ X finSupp .0. ) ) )
9 5 6 8 syl2an2 
 |-  ( ( I e. W /\ X e. B ) -> ( X e. B <-> ( X e. ( ( Base ` R ) ^m I ) /\ X finSupp .0. ) ) )
10 4 9 mpbid 
 |-  ( ( I e. W /\ X e. B ) -> ( X e. ( ( Base ` R ) ^m I ) /\ X finSupp .0. ) )
11 10 simprd 
 |-  ( ( I e. W /\ X e. B ) -> X finSupp .0. )