matmulr

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

	Ref	Expression
Hypotheses	matmulr.a	$⊢ A = N Mat R$
	matmulr.t	$⊢ \underset{˙}{\cdot} = R maMul ⟨N, N, N⟩$
Assertion	matmulr	$⊢ (N \in Fin \land R \in V) \to \underset{˙}{\cdot} = \cdot_{A}$

Step	Hyp	Ref	Expression
1		matmulr.a	$⊢ A = N Mat R$
2		matmulr.t	$⊢ \underset{˙}{\cdot} = R maMul ⟨N, N, N⟩$
3		ovex	$⊢ R freeLMod (N \times N) \in V$
4	2	ovexi	$⊢ \underset{˙}{\cdot} \in V$
5	3 4	pm3.2i	$⊢ (R freeLMod (N \times N) \in V \land \underset{˙}{\cdot} \in V)$
6		mulrid	$⊢ \cdot_{𝑟} = Slot \cdot_{ndx}$
7	6	setsid	$⊢ (R freeLMod (N \times N) \in V \land \underset{˙}{\cdot} \in V) \to \underset{˙}{\cdot} = \cdot_{((R freeLMod (N \times N)) sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩)}$
8	5 7	mp1i	$⊢ (N \in Fin \land R \in V) \to \underset{˙}{\cdot} = \cdot_{((R freeLMod (N \times N)) sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩)}$
9		eqid	$⊢ R freeLMod (N \times N) = R freeLMod (N \times N)$
10	1 9 2	matval	$⊢ (N \in Fin \land R \in V) \to A = (R freeLMod (N \times N)) sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩$
11	10	fveq2d	$⊢ (N \in Fin \land R \in V) \to \cdot_{A} = \cdot_{((R freeLMod (N \times N)) sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩)}$
12	8 11	eqtr4d	$⊢ (N \in Fin \land R \in V) \to \underset{˙}{\cdot} = \cdot_{A}$

Metamath Proof Explorer