Metamath Proof Explorer


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