This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → 0 = ( 0g ‘ 𝐻 ) )