Metamath Proof Explorer


Theorem resv0g

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

Ref Expression
Hypotheses resvbas.1 𝐻 = ( 𝐺v 𝐴 )
resv0g.2 0 = ( 0g𝐺 )
Assertion resv0g ( 𝐴𝑉0 = ( 0g𝐻 ) )

Proof

Step Hyp Ref Expression
1 resvbas.1 𝐻 = ( 𝐺v 𝐴 )
2 resv0g.2 0 = ( 0g𝐺 )
3 eqidd ( 𝐴𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
4 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 1 4 resvbas ( 𝐴𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
6 eqid ( +g𝐺 ) = ( +g𝐺 )
7 1 6 resvplusg ( 𝐴𝑉 → ( +g𝐺 ) = ( +g𝐻 ) )
8 7 oveqdr ( ( 𝐴𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g𝐺 ) 𝑦 ) = ( 𝑥 ( +g𝐻 ) 𝑦 ) )
9 3 5 8 grpidpropd ( 𝐴𝑉 → ( 0g𝐺 ) = ( 0g𝐻 ) )
10 2 9 syl5eq ( 𝐴𝑉0 = ( 0g𝐻 ) )