Metamath Proof Explorer


Theorem resv0g

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

Ref Expression
Hypotheses resvbas.1 H = G 𝑣 A
resv0g.2 0 ˙ = 0 G
Assertion resv0g A V 0 ˙ = 0 H

Proof

Step Hyp Ref Expression
1 resvbas.1 H = G 𝑣 A
2 resv0g.2 0 ˙ = 0 G
3 eqidd A V Base G = Base G
4 eqid Base G = Base G
5 1 4 resvbas A V Base G = Base H
6 eqid + G = + G
7 1 6 resvplusg A V + G = + H
8 7 oveqdr A V x Base G y Base G x + G y = x + H y
9 3 5 8 grpidpropd A V 0 G = 0 H
10 2 9 syl5eq A V 0 ˙ = 0 H