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

Metamath Proof Explorer

Theorem mrclsp

Description: Moore closure generalizes module span. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypotheses mrclsp.u 
|- U = ( LSubSp ` W )
mrclsp.k 
|- K = ( LSpan ` W )
mrclsp.f 
|- F = ( mrCls ` U )
Assertion mrclsp 
|- ( W e. LMod -> K = F )

Proof

Step Hyp Ref Expression
1 mrclsp.u 
 |-  U = ( LSubSp ` W )
2 mrclsp.k 
 |-  K = ( LSpan ` W )
3 mrclsp.f 
 |-  F = ( mrCls ` U )
4 eqid 
 |-  ( Base ` W ) = ( Base ` W )
5 4 1 2 lspfval 
 |-  ( W e. LMod -> K = ( a e. ~P ( Base ` W ) |-> |^| { b e. U | a C_ b } ) )
6 4 1 lssmre 
 |-  ( W e. LMod -> U e. ( Moore ` ( Base ` W ) ) )
7 3 mrcfval 
 |-  ( U e. ( Moore ` ( Base ` W ) ) -> F = ( a e. ~P ( Base ` W ) |-> |^| { b e. U | a C_ b } ) )
8 6 7 syl 
 |-  ( W e. LMod -> F = ( a e. ~P ( Base ` W ) |-> |^| { b e. U | a C_ b } ) )
9 5 8 eqtr4d 
 |-  ( W e. LMod -> K = F )