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 ˙ = 1 G
Assertion resv1r A V 1 ˙ = 1 H

Proof

Step Hyp Ref Expression
1 resvbas.1 H = G 𝑣 A
2 resv1r.2 1 ˙ = 1 G
3 eqid Base G = Base G
4 1 3 resvbas A V Base G = Base H
5 4 eleq2d A V e Base G e Base H
6 eqid G = G
7 1 6 resvmulr A V G = H
8 7 oveqd A V e G x = e H x
9 8 eqeq1d A V e G x = x e H x = x
10 7 oveqd A V x G e = x H e
11 10 eqeq1d A V x G e = x x H e = x
12 9 11 anbi12d A V e G x = x x G e = x e H x = x x H e = x
13 4 12 raleqbidv A V x Base G e G x = x x G e = x x Base H e H x = x x H e = x
14 5 13 anbi12d A V e Base G x Base G e G x = x x G e = x e Base H x Base H e H x = x x H e = x
15 14 iotabidv A V ι e | e Base G x Base G e G x = x x G e = x = ι e | e Base H x Base H e H x = x x H e = x
16 3 6 2 dfur2 1 ˙ = ι e | e Base G x Base G e G x = x x G e = x
17 eqid Base H = Base H
18 eqid H = H
19 eqid 1 H = 1 H
20 17 18 19 dfur2 1 H = ι e | e Base H x Base H e H x = x x H e = x
21 15 16 20 3eqtr4g A V 1 ˙ = 1 H