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 ‘ 𝐴 ) )