Theorem mat0

Description: The matrix ring has the same zero as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015)

	Ref	Expression
Hypotheses	matbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matbas.g	⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
Assertion	mat0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		matbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matbas.g	⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
3		eqidd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
4	1 2	matbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐴 ) )
5	1 2	matplusg	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐴 ) )
6	5	oveqdr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) )
7	3 4 6	grpidpropd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐴 ) )