Theorem matlmod

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

	Ref	Expression
Hypothesis	matlmod.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
Assertion	matlmod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		matlmod.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		sqxpexg	⊢ ( 𝑁 ∈ Fin → ( 𝑁 × 𝑁 ) ∈ V )
3		eqid	⊢ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
4	3	frlmlmod	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 × 𝑁 ) ∈ V ) → ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ∈ LMod )
5	4	ancoms	⊢ ( ( ( 𝑁 × 𝑁 ) ∈ V ∧ 𝑅 ∈ Ring ) → ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ∈ LMod )
6	2 5	sylan	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ∈ LMod )
7		eqidd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
8	1 3	matbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
9	1 3	matplusg	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( +g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( +g ‘ 𝐴 ) )
10	9	oveqdr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) ) ) → ( 𝑥 ( +g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) )
11		eqidd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
12	1 3	matsca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Scalar ‘ 𝐴 ) )
13		eqid	⊢ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
14	1 3	matvsca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( ·𝑠 ‘ 𝐴 ) )
15	14	oveqdr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑦 ) )
16	7 8 10 11 12 13 15	lmodpropd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ∈ LMod ↔ 𝐴 ∈ LMod ) )
17	6 16	mpbid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )