# 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 ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( R e. V /\ I e. W ) -> R = ( Scalar ` ( ringLMod ` R ) ) )`
` |-  ( Base ` F ) = ( Base ` F )`
` |-  ( ( R e. V /\ I e. W ) -> F = ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) )`
` |-  ( ( R e. V /\ I e. W ) -> ( Scalar ` F ) = ( Scalar ` ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) ) )`
` |-  ( ( R e. V /\ I e. W ) -> R = ( Scalar ` F ) )`