Metamath Proof Explorer


Theorem frlmvscafval

Description: Scalar multiplication in a free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses frlmvscafval.y 𝑌 = ( 𝑅 freeLMod 𝐼 )
frlmvscafval.b 𝐵 = ( Base ‘ 𝑌 )
frlmvscafval.k 𝐾 = ( Base ‘ 𝑅 )
frlmvscafval.i ( 𝜑𝐼𝑊 )
frlmvscafval.a ( 𝜑𝐴𝐾 )
frlmvscafval.x ( 𝜑𝑋𝐵 )
frlmvscafval.v = ( ·𝑠𝑌 )
frlmvscafval.t · = ( .r𝑅 )
Assertion frlmvscafval ( 𝜑 → ( 𝐴 𝑋 ) = ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 frlmvscafval.y 𝑌 = ( 𝑅 freeLMod 𝐼 )
2 frlmvscafval.b 𝐵 = ( Base ‘ 𝑌 )
3 frlmvscafval.k 𝐾 = ( Base ‘ 𝑅 )
4 frlmvscafval.i ( 𝜑𝐼𝑊 )
5 frlmvscafval.a ( 𝜑𝐴𝐾 )
6 frlmvscafval.x ( 𝜑𝑋𝐵 )
7 frlmvscafval.v = ( ·𝑠𝑌 )
8 frlmvscafval.t · = ( .r𝑅 )
9 1 2 frlmrcl ( 𝑋𝐵𝑅 ∈ V )
10 6 9 syl ( 𝜑𝑅 ∈ V )
11 1 2 frlmpws ( ( 𝑅 ∈ V ∧ 𝐼𝑊 ) → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
12 10 4 11 syl2anc ( 𝜑𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
13 12 fveq2d ( 𝜑 → ( ·𝑠𝑌 ) = ( ·𝑠 ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
14 2 fvexi 𝐵 ∈ V
15 eqid ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 )
16 eqid ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
17 15 16 ressvsca ( 𝐵 ∈ V → ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( ·𝑠 ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
18 14 17 ax-mp ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( ·𝑠 ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
19 13 7 18 3eqtr4g ( 𝜑 = ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
20 19 oveqd ( 𝜑 → ( 𝐴 𝑋 ) = ( 𝐴 ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) 𝑋 ) )
21 eqid ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 )
22 eqid ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
23 rlmvsca ( .r𝑅 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
24 8 23 eqtri · = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
25 eqid ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
26 eqid ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
27 fvexd ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ V )
28 rlmsca ( 𝑅 ∈ V → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
29 10 28 syl ( 𝜑𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
30 29 fveq2d ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
31 3 30 syl5eq ( 𝜑𝐾 = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
32 5 31 eleqtrd ( 𝜑𝐴 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
33 12 fveq2d ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
34 2 33 syl5eq ( 𝜑𝐵 = ( Base ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
35 15 22 ressbasss ( Base ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) ⊆ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
36 34 35 eqsstrdi ( 𝜑𝐵 ⊆ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
37 36 6 sseldd ( 𝜑𝑋 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
38 21 22 24 16 25 26 27 4 32 37 pwsvscafval ( 𝜑 → ( 𝐴 ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) 𝑋 ) = ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) )
39 20 38 eqtrd ( 𝜑 → ( 𝐴 𝑋 ) = ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) )