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 · 𝑋 ) )