This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem matmulr

Description: Multiplication in the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Hypotheses matmulr.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
matmulr.t ⊢ · = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
Assertion matmulr ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → · = ( .r ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 matmulr.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 matmulr.t ⊢ · = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
3 ovex ⊢ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ∈ V
4 2 ovexi ⊢ · ∈ V
5 3 4 pm3.2i ⊢ ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ∈ V ∧ · ∈ V )
6 mulridx ⊢ .r = Slot ( .r ‘ ndx )
7 6 setsid ⊢ ( ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ∈ V ∧ · ∈ V ) → · = ( .r ‘ ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) sSet ⟨ ( .r ‘ ndx ) , · ⟩ ) ) )
8 5 7 mp1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → · = ( .r ‘ ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) sSet ⟨ ( .r ‘ ndx ) , · ⟩ ) ) )
9 eqid ⊢ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
10 1 9 2 matval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐴 = ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) sSet ⟨ ( .r ‘ ndx ) , · ⟩ ) )
11 10 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( .r ‘ 𝐴 ) = ( .r ‘ ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) sSet ⟨ ( .r ‘ ndx ) , · ⟩ ) ) )
12 8 11 eqtr4d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → · = ( .r ‘ 𝐴 ) )