Metamath Proof Explorer

Theorem frlmsca

Description: The ring of scalars of a free module. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypothesis frlmval.f 
|- F = ( R freeLMod I )
Assertion frlmsca 
|- ( ( R e. V /\ I e. W ) -> R = ( Scalar ` F ) )

Proof

Step Hyp Ref Expression
1 frlmval.f 
 |-  F = ( R freeLMod I )
2 fvex 
 |-  ( ringLMod ` R ) e. _V
3 eqid 
 |-  ( ( ringLMod ` R ) ^s I ) = ( ( ringLMod ` R ) ^s I )
4 eqid 
 |-  ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ringLMod ` R ) )
5 3 4 pwssca 
 |-  ( ( ( ringLMod ` R ) e. _V /\ I e. W ) -> ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ( ringLMod ` R ) ^s I ) ) )
6 2 5 mpan 
 |-  ( I e. W -> ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ( ringLMod ` R ) ^s I ) ) )
7 6 adantl 
 |-  ( ( R e. V /\ I e. W ) -> ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ( ringLMod ` R ) ^s I ) ) )
8 fvex 
 |-  ( Base ` F ) e. _V
9 eqid 
 |-  ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) = ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) )
10 eqid 
 |-  ( Scalar ` ( ( ringLMod ` R ) ^s I ) ) = ( Scalar ` ( ( ringLMod ` R ) ^s I ) )
11 9 10 resssca 
 |-  ( ( Base ` F ) e. _V -> ( Scalar ` ( ( ringLMod ` R ) ^s I ) ) = ( Scalar ` ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) ) )
12 8 11 ax-mp 
 |-  ( Scalar ` ( ( ringLMod ` R ) ^s I ) ) = ( Scalar ` ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) )
13 7 12 eqtrdi 
 |-  ( ( R e. V /\ I e. W ) -> ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) ) )
14 rlmsca 
 |-  ( R e. V -> R = ( Scalar ` ( ringLMod ` R ) ) )
15 14 adantr 
 |-  ( ( R e. V /\ I e. W ) -> R = ( Scalar ` ( ringLMod ` R ) ) )
16 eqid 
 |-  ( Base ` F ) = ( Base ` F )
17 1 16 frlmpws 
 |-  ( ( R e. V /\ I e. W ) -> F = ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) )
18 17 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( Scalar ` F ) = ( Scalar ` ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) ) )
19 13 15 18 3eqtr4d 
 |-  ( ( R e. V /\ I e. W ) -> R = ( Scalar ` F ) )