Metamath Proof Explorer

Theorem matvsca2

Description: Scalar multiplication in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses matvsca2.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
matvsca2.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
matvsca2.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
matvsca2.v ⊢ · = ( ·𝑠 ‘ 𝐴 )
matvsca2.t ⊢ × = ( .r ‘ 𝑅 )
matvsca2.c ⊢ 𝐶 = ( 𝑁 × 𝑁 )
Assertion matvsca2 ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( ( 𝐶 × { 𝑋 } ) ∘f × 𝑌 ) )

Proof

Step Hyp Ref Expression
1 matvsca2.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 matvsca2.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 matvsca2.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 matvsca2.v ⊢ · = ( ·𝑠 ‘ 𝐴 )
5 matvsca2.t ⊢ × = ( .r ‘ 𝑅 )
6 matvsca2.c ⊢ 𝐶 = ( 𝑁 × 𝑁 )
7 1 2 matrcl ⊢ ( 𝑌 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
8 7 adantl ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
9 eqid ⊢ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
10 1 9 matvsca ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( ·𝑠 ‘ 𝐴 ) )
11 8 10 syl ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( ·𝑠 ‘ 𝐴 ) )
12 11 4 eqtr4di ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = · )
13 12 oveqd ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑌 ) = ( 𝑋 · 𝑌 ) )
14 eqid ⊢ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) )
15 8 simpld ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑁 ∈ Fin )
16 xpfi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑁 × 𝑁 ) ∈ Fin )
17 15 15 16 syl2anc ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 × 𝑁 ) ∈ Fin )
18 simpl ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐾 )
19 simpr ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
20 1 9 matbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
21 8 20 syl ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
22 21 2 eqtr4di ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = 𝐵 )
23 19 22 eleqtrrd ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
24 eqid ⊢ ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) )
25 9 14 3 17 18 23 24 5 frlmvscafval ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑌 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f × 𝑌 ) )
26 6 xpeq1i ⊢ ( 𝐶 × { 𝑋 } ) = ( ( 𝑁 × 𝑁 ) × { 𝑋 } )
27 26 oveq1i ⊢ ( ( 𝐶 × { 𝑋 } ) ∘f × 𝑌 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f × 𝑌 )
28 25 27 eqtr4di ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑌 ) = ( ( 𝐶 × { 𝑋 } ) ∘f × 𝑌 ) )
29 13 28 eqtr3d ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( ( 𝐶 × { 𝑋 } ) ∘f × 𝑌 ) )