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 𝐵 ) )