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	|- A = ( N Mat R )
	matbas.g	|- G = ( R freeLMod ( N X. N ) )
Assertion	mat0	|- ( ( N e. Fin /\ R e. V ) -> ( 0g ` G ) = ( 0g ` A ) )

Proof

Step	Hyp	Ref	Expression
1		matbas.a	|- A = ( N Mat R )
2		matbas.g	|- G = ( R freeLMod ( N X. N ) )
3		eqidd	|- ( ( N e. Fin /\ R e. V ) -> ( Base ` G ) = ( Base ` G ) )
4	1 2	matbas	|- ( ( N e. Fin /\ R e. V ) -> ( Base ` G ) = ( Base ` A ) )
5	1 2	matplusg	|- ( ( N e. Fin /\ R e. V ) -> ( +g ` G ) = ( +g ` A ) )
6	5	oveqdr	|- ( ( ( N e. Fin /\ R e. V ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` A ) y ) )
7	3 4 6	grpidpropd	|- ( ( N e. Fin /\ R e. V ) -> ( 0g ` G ) = ( 0g ` A ) )