Theorem resv0g

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

	Ref	Expression
Hypotheses	resvbas.1	$$⊢H=G{\upharpoonright }_{𝑣}A$$
	resv0g.2	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	resv0g	$$⊢A\in V\to \underset{\dot{}}{0}=0_H$$

Proof

Step	Hyp	Ref	Expression
1		resvbas.1	$$⊢H=G{\upharpoonright }_{𝑣}A$$
2		resv0g.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		eqidd	$$⊢A\in V\to {\mathrm{Base}}_G={\mathrm{Base}}_G$$
4		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
5	1 4	resvbas	$$⊢A\in V\to {\mathrm{Base}}_G={\mathrm{Base}}_H$$
6		eqid	$$⊢{+}_G={+}_G$$
7	1 6	resvplusg	$$⊢A\in V\to {+}_G={+}_H$$
8	7	oveqdr	$$⊢\left(A\in V\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to x{+}_{G}y=x{+}_{H}y$$
9	3 5 8	grpidpropd	$$⊢A\in V\to 0_G=0_H$$
10	2 9	syl5eq	$$⊢A\in V\to \underset{\dot{}}{0}=0_H$$