Metamath Proof Explorer

Theorem matlmod

Description: The matrix ring is a linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015)

		Ref	Expression
	Hypothesis	matlmod.a	$⊢ A = N Mat R$
	Assertion	matlmod	$⊢ (N \in Fin \land R \in Ring) \to A \in LMod$

Proof

Step	Hyp	Ref	Expression
1		matlmod.a	$⊢ A = N Mat R$
2		sqxpexg	$⊢ N \in Fin \to N \times N \in V$
3		eqid	$⊢ R freeLMod (N \times N) = R freeLMod (N \times N)$
4	3	frlmlmod	$⊢ (R \in Ring \land N \times N \in V) \to R freeLMod (N \times N) \in LMod$
5	4	ancoms	$⊢ (N \times N \in V \land R \in Ring) \to R freeLMod (N \times N) \in LMod$
6	2 5	sylan	$⊢ (N \in Fin \land R \in Ring) \to R freeLMod (N \times N) \in LMod$
7		eqidd	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{(R freeLMod (N \times N))} = {Base}_{(R freeLMod (N \times N))}$
8	1 3	matbas	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{(R freeLMod (N \times N))} = {Base}_{A}$
9	1 3	matplusg	$⊢ (N \in Fin \land R \in Ring) \to +_{(R freeLMod (N \times N))} = +_{A}$
10	9	oveqdr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in {Base}_{(R freeLMod (N \times N))} \land y \in {Base}_{(R freeLMod (N \times N))})) \to x +_{(R freeLMod (N \times N))} y = x +_{A} y$
11		eqidd	$⊢ (N \in Fin \land R \in Ring) \to Scalar (R freeLMod (N \times N)) = Scalar (R freeLMod (N \times N))$
12	1 3	matsca	$⊢ (N \in Fin \land R \in Ring) \to Scalar (R freeLMod (N \times N)) = Scalar (A)$
13		eqid	$⊢ {Base}_{Scalar (R freeLMod (N \times N))} = {Base}_{Scalar (R freeLMod (N \times N))}$
14	1 3	matvsca	$⊢ (N \in Fin \land R \in Ring) \to \cdot_{(R freeLMod (N \times N))} = \cdot_{A}$
15	14	oveqdr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in {Base}_{Scalar (R freeLMod (N \times N))} \land y \in {Base}_{(R freeLMod (N \times N))})) \to x \cdot_{(R freeLMod (N \times N))} y = x \cdot_{A} y$
16	7 8 10 11 12 13 15	lmodpropd	$⊢ (N \in Fin \land R \in Ring) \to (R freeLMod (N \times N) \in LMod \leftrightarrow A \in LMod)$
17	6 16	mpbid	$⊢ (N \in Fin \land R \in Ring) \to A \in LMod$