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 |`v A )
resv1r.2 
|- .1. = ( 1r ` G )
Assertion resv1r 
|- ( A e. V -> .1. = ( 1r ` H ) )

Proof

Step Hyp Ref Expression
1 resvbas.1 
 |-  H = ( G |`v A )
2 resv1r.2 
 |-  .1. = ( 1r ` G )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 1 3 resvbas 
 |-  ( A e. V -> ( Base ` G ) = ( Base ` H ) )
5 4 eleq2d 
 |-  ( A e. V -> ( e e. ( Base ` G ) <-> e e. ( Base ` H ) ) )
6 eqid 
 |-  ( .r ` G ) = ( .r ` G )
7 1 6 resvmulr 
 |-  ( A e. V -> ( .r ` G ) = ( .r ` H ) )
8 7 oveqd 
 |-  ( A e. V -> ( e ( .r ` G ) x ) = ( e ( .r ` H ) x ) )
9 8 eqeq1d 
 |-  ( A e. V -> ( ( e ( .r ` G ) x ) = x <-> ( e ( .r ` H ) x ) = x ) )
10 7 oveqd 
 |-  ( A e. V -> ( x ( .r ` G ) e ) = ( x ( .r ` H ) e ) )
11 10 eqeq1d 
 |-  ( A e. V -> ( ( x ( .r ` G ) e ) = x <-> ( x ( .r ` H ) e ) = x ) )
12 9 11 anbi12d 
 |-  ( A e. V -> ( ( ( e ( .r ` G ) x ) = x /\ ( x ( .r ` G ) e ) = x ) <-> ( ( e ( .r ` H ) x ) = x /\ ( x ( .r ` H ) e ) = x ) ) )
13 4 12 raleqbidv 
 |-  ( A e. V -> ( A. x e. ( Base ` G ) ( ( e ( .r ` G ) x ) = x /\ ( x ( .r ` G ) e ) = x ) <-> A. x e. ( Base ` H ) ( ( e ( .r ` H ) x ) = x /\ ( x ( .r ` H ) e ) = x ) ) )
14 5 13 anbi12d 
 |-  ( A e. V -> ( ( e e. ( Base ` G ) /\ A. x e. ( Base ` G ) ( ( e ( .r ` G ) x ) = x /\ ( x ( .r ` G ) e ) = x ) ) <-> ( e e. ( Base ` H ) /\ A. x e. ( Base ` H ) ( ( e ( .r ` H ) x ) = x /\ ( x ( .r ` H ) e ) = x ) ) ) )
15 14 iotabidv 
 |-  ( A e. V -> ( iota e ( e e. ( Base ` G ) /\ A. x e. ( Base ` G ) ( ( e ( .r ` G ) x ) = x /\ ( x ( .r ` G ) e ) = x ) ) ) = ( iota e ( e e. ( Base ` H ) /\ A. x e. ( Base ` H ) ( ( e ( .r ` H ) x ) = x /\ ( x ( .r ` H ) e ) = x ) ) ) )
16 3 6 2 dfur2 
 |-  .1. = ( iota e ( e e. ( Base ` G ) /\ A. x e. ( Base ` G ) ( ( e ( .r ` G ) x ) = x /\ ( x ( .r ` G ) e ) = x ) ) )
17 eqid 
 |-  ( Base ` H ) = ( Base ` H )
18 eqid 
 |-  ( .r ` H ) = ( .r ` H )
19 eqid 
 |-  ( 1r ` H ) = ( 1r ` H )
20 17 18 19 dfur2 
 |-  ( 1r ` H ) = ( iota e ( e e. ( Base ` H ) /\ A. x e. ( Base ` H ) ( ( e ( .r ` H ) x ) = x /\ ( x ( .r ` H ) e ) = x ) ) )
21 15 16 20 3eqtr4g 
 |-  ( A e. V -> .1. = ( 1r ` H ) )