Theorem resv0g

Description: 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018)

	Ref	Expression
Hypotheses	resvbas.1	|- H = ( G |`v A )
	resv0g.2	|- .0. = ( 0g ` G )
Assertion	resv0g	|- ( A e. V -> .0. = ( 0g ` H ) )

Proof

Step	Hyp	Ref	Expression
1		resvbas.1	|- H = ( G |`v A )
2		resv0g.2	|- .0. = ( 0g ` G )
3		eqidd	|- ( A e. V -> ( Base ` G ) = ( Base ` G ) )
4		eqid	|- ( Base ` G ) = ( Base ` G )
5	1 4	resvbas	|- ( A e. V -> ( Base ` G ) = ( Base ` H ) )
6		eqid	|- ( +g ` G ) = ( +g ` G )
7	1 6	resvplusg	|- ( A e. V -> ( +g ` G ) = ( +g ` H ) )
8	7	oveqdr	|- ( ( A e. V /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
9	3 5 8	grpidpropd	|- ( A e. V -> ( 0g ` G ) = ( 0g ` H ) )
10	2 9	syl5eq	|- ( A e. V -> .0. = ( 0g ` H ) )