Metamath Proof Explorer


Theorem frlmpws

Description: The free module as a restriction of the power module. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses frlmval.f 𝐹 = ( 𝑅 freeLMod 𝐼 )
frlmpws.b 𝐵 = ( Base ‘ 𝐹 )
Assertion frlmpws ( ( 𝑅𝑉𝐼𝑊 ) → 𝐹 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )

Proof

Step Hyp Ref Expression
1 frlmval.f 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 frlmpws.b 𝐵 = ( Base ‘ 𝐹 )
3 eqid ( Base ‘ ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = ( Base ‘ ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
4 3 dsmmval2 ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ↾s ( Base ‘ ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) )
5 rlmsca ( 𝑅𝑉𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
6 5 adantr ( ( 𝑅𝑉𝐼𝑊 ) → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
7 6 oveq1d ( ( 𝑅𝑉𝐼𝑊 ) → ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
8 1 frlmval ( ( 𝑅𝑉𝐼𝑊 ) → 𝐹 = ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
9 8 eqcomd ( ( 𝑅𝑉𝐼𝑊 ) → ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = 𝐹 )
10 9 fveq2d ( ( 𝑅𝑉𝐼𝑊 ) → ( Base ‘ ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = ( Base ‘ 𝐹 ) )
11 10 2 eqtr4di ( ( 𝑅𝑉𝐼𝑊 ) → ( Base ‘ ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) = 𝐵 )
12 7 11 oveq12d ( ( 𝑅𝑉𝐼𝑊 ) → ( ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ↾s ( Base ‘ ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ) ) = ( ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ↾s 𝐵 ) )
13 4 12 syl5eq ( ( 𝑅𝑉𝐼𝑊 ) → ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ↾s 𝐵 ) )
14 fvex ( ringLMod ‘ 𝑅 ) ∈ V
15 eqid ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 )
16 eqid ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
17 15 16 pwsval ( ( ( ringLMod ‘ 𝑅 ) ∈ V ∧ 𝐼𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
18 14 17 mpan ( 𝐼𝑊 → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
19 18 adantl ( ( 𝑅𝑉𝐼𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
20 19 oveq1d ( ( 𝑅𝑉𝐼𝑊 ) → ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) = ( ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ↾s 𝐵 ) )
21 13 8 20 3eqtr4d ( ( 𝑅𝑉𝐼𝑊 ) → 𝐹 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )