Metamath Proof Explorer

Theorem resv1r

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

Ref Expression
Hypotheses resvbas.1 ⊢H=G↾𝑣A
resv1r.2 ⊢1˙=1G
Assertion resv1r ⊢A∈V→1˙=1H

Proof

Step Hyp Ref Expression
1 resvbas.1 ⊢H=G↾𝑣A
2 resv1r.2 ⊢1˙=1G
3 eqid ⊢BaseG=BaseG
4 1 3 resvbas ⊢A∈V→BaseG=BaseH
5 4 eleq2d ⊢A∈V→e∈BaseG↔e∈BaseH
6 eqid ⊢⋅G=⋅G
7 1 6 resvmulr ⊢A∈V→⋅G=⋅H
8 7 oveqd ⊢A∈V→e⋅Gx=e⋅Hx
9 8 eqeq1d ⊢A∈V→e⋅Gx=x↔e⋅Hx=x
10 7 oveqd ⊢A∈V→x⋅Ge=x⋅He
11 10 eqeq1d ⊢A∈V→x⋅Ge=x↔x⋅He=x
12 9 11 anbi12d ⊢A∈V→e⋅Gx=x∧x⋅Ge=x↔e⋅Hx=x∧x⋅He=x
13 4 12 raleqbidv ⊢A∈V→∀x∈BaseGe⋅Gx=x∧x⋅Ge=x↔∀x∈BaseHe⋅Hx=x∧x⋅He=x
14 5 13 anbi12d ⊢A∈V→e∈BaseG∧∀x∈BaseGe⋅Gx=x∧x⋅Ge=x↔e∈BaseH∧∀x∈BaseHe⋅Hx=x∧x⋅He=x
15 14 iotabidv ⊢A∈V→ιe|e∈BaseG∧∀x∈BaseGe⋅Gx=x∧x⋅Ge=x=ιe|e∈BaseH∧∀x∈BaseHe⋅Hx=x∧x⋅He=x
16 3 6 2 dfur2 ⊢1˙=ιe|e∈BaseG∧∀x∈BaseGe⋅Gx=x∧x⋅Ge=x
17 eqid ⊢BaseH=BaseH
18 eqid ⊢⋅H=⋅H
19 eqid ⊢1H=1H
20 17 18 19 dfur2 ⊢1H=ιe|e∈BaseH∧∀x∈BaseHe⋅Hx=x∧x⋅He=x
21 15 16 20 3eqtr4g ⊢A∈V→1˙=1H