Metamath Proof Explorer

Theorem relexpiidm

Description: Any power of any restriction of the identity relation is itself. (Contributed by RP, 12-Jun-2020)

Ref Expression
Assertion relexpiidm 
|- ( ( A e. V /\ N e. NN0 ) -> ( ( _I |` A ) ^r N ) = ( _I |` A ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = 0 -> ( ( _I |` A ) ^r x ) = ( ( _I |` A ) ^r 0 ) )
2 1 eqeq1d 
 |-  ( x = 0 -> ( ( ( _I |` A ) ^r x ) = ( _I |` A ) <-> ( ( _I |` A ) ^r 0 ) = ( _I |` A ) ) )
3 2 imbi2d 
 |-  ( x = 0 -> ( ( A e. V -> ( ( _I |` A ) ^r x ) = ( _I |` A ) ) <-> ( A e. V -> ( ( _I |` A ) ^r 0 ) = ( _I |` A ) ) ) )
4 oveq2 
 |-  ( x = y -> ( ( _I |` A ) ^r x ) = ( ( _I |` A ) ^r y ) )
5 4 eqeq1d 
 |-  ( x = y -> ( ( ( _I |` A ) ^r x ) = ( _I |` A ) <-> ( ( _I |` A ) ^r y ) = ( _I |` A ) ) )
6 5 imbi2d 
 |-  ( x = y -> ( ( A e. V -> ( ( _I |` A ) ^r x ) = ( _I |` A ) ) <-> ( A e. V -> ( ( _I |` A ) ^r y ) = ( _I |` A ) ) ) )
7 oveq2 
 |-  ( x = ( y + 1 ) -> ( ( _I |` A ) ^r x ) = ( ( _I |` A ) ^r ( y + 1 ) ) )
8 7 eqeq1d 
 |-  ( x = ( y + 1 ) -> ( ( ( _I |` A ) ^r x ) = ( _I |` A ) <-> ( ( _I |` A ) ^r ( y + 1 ) ) = ( _I |` A ) ) )
9 8 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( A e. V -> ( ( _I |` A ) ^r x ) = ( _I |` A ) ) <-> ( A e. V -> ( ( _I |` A ) ^r ( y + 1 ) ) = ( _I |` A ) ) ) )
10 oveq2 
 |-  ( x = N -> ( ( _I |` A ) ^r x ) = ( ( _I |` A ) ^r N ) )
11 10 eqeq1d 
 |-  ( x = N -> ( ( ( _I |` A ) ^r x ) = ( _I |` A ) <-> ( ( _I |` A ) ^r N ) = ( _I |` A ) ) )
12 11 imbi2d 
 |-  ( x = N -> ( ( A e. V -> ( ( _I |` A ) ^r x ) = ( _I |` A ) ) <-> ( A e. V -> ( ( _I |` A ) ^r N ) = ( _I |` A ) ) ) )
13 resiexg 
 |-  ( A e. V -> ( _I |` A ) e. _V )
14 relexp0g 
 |-  ( ( _I |` A ) e. _V -> ( ( _I |` A ) ^r 0 ) = ( _I |` ( dom ( _I |` A ) u. ran ( _I |` A ) ) ) )
15 13 14 syl 
 |-  ( A e. V -> ( ( _I |` A ) ^r 0 ) = ( _I |` ( dom ( _I |` A ) u. ran ( _I |` A ) ) ) )
16 dmresi 
 |-  dom ( _I |` A ) = A
17 rnresi 
 |-  ran ( _I |` A ) = A
18 16 17 uneq12i 
 |-  ( dom ( _I |` A ) u. ran ( _I |` A ) ) = ( A u. A )
19 unidm 
 |-  ( A u. A ) = A
20 18 19 eqtri 
 |-  ( dom ( _I |` A ) u. ran ( _I |` A ) ) = A
21 20 reseq2i 
 |-  ( _I |` ( dom ( _I |` A ) u. ran ( _I |` A ) ) ) = ( _I |` A )
22 15 21 eqtrdi 
 |-  ( A e. V -> ( ( _I |` A ) ^r 0 ) = ( _I |` A ) )
23 relres 
 |-  Rel ( _I |` A )
24 23 a1i 
 |-  ( ( ( ( _I |` A ) ^r y ) = ( _I |` A ) /\ A e. V /\ y e. NN0 ) -> Rel ( _I |` A ) )
25 simp3 
 |-  ( ( ( ( _I |` A ) ^r y ) = ( _I |` A ) /\ A e. V /\ y e. NN0 ) -> y e. NN0 )
26 24 25 relexpsucrd 
 |-  ( ( ( ( _I |` A ) ^r y ) = ( _I |` A ) /\ A e. V /\ y e. NN0 ) -> ( ( _I |` A ) ^r ( y + 1 ) ) = ( ( ( _I |` A ) ^r y ) o. ( _I |` A ) ) )
27 simp1 
 |-  ( ( ( ( _I |` A ) ^r y ) = ( _I |` A ) /\ A e. V /\ y e. NN0 ) -> ( ( _I |` A ) ^r y ) = ( _I |` A ) )
28 27 coeq1d 
 |-  ( ( ( ( _I |` A ) ^r y ) = ( _I |` A ) /\ A e. V /\ y e. NN0 ) -> ( ( ( _I |` A ) ^r y ) o. ( _I |` A ) ) = ( ( _I |` A ) o. ( _I |` A ) ) )
29 coires1 
 |-  ( ( _I |` A ) o. ( _I |` A ) ) = ( ( _I |` A ) |` A )
30 residm 
 |-  ( ( _I |` A ) |` A ) = ( _I |` A )
31 29 30 eqtri 
 |-  ( ( _I |` A ) o. ( _I |` A ) ) = ( _I |` A )
32 28 31 eqtrdi 
 |-  ( ( ( ( _I |` A ) ^r y ) = ( _I |` A ) /\ A e. V /\ y e. NN0 ) -> ( ( ( _I |` A ) ^r y ) o. ( _I |` A ) ) = ( _I |` A ) )
33 26 32 eqtrd 
 |-  ( ( ( ( _I |` A ) ^r y ) = ( _I |` A ) /\ A e. V /\ y e. NN0 ) -> ( ( _I |` A ) ^r ( y + 1 ) ) = ( _I |` A ) )
34 33 3exp 
 |-  ( ( ( _I |` A ) ^r y ) = ( _I |` A ) -> ( A e. V -> ( y e. NN0 -> ( ( _I |` A ) ^r ( y + 1 ) ) = ( _I |` A ) ) ) )
35 34 com13 
 |-  ( y e. NN0 -> ( A e. V -> ( ( ( _I |` A ) ^r y ) = ( _I |` A ) -> ( ( _I |` A ) ^r ( y + 1 ) ) = ( _I |` A ) ) ) )
36 35 a2d 
 |-  ( y e. NN0 -> ( ( A e. V -> ( ( _I |` A ) ^r y ) = ( _I |` A ) ) -> ( A e. V -> ( ( _I |` A ) ^r ( y + 1 ) ) = ( _I |` A ) ) ) )
37 3 6 9 12 22 36 nn0ind 
 |-  ( N e. NN0 -> ( A e. V -> ( ( _I |` A ) ^r N ) = ( _I |` A ) ) )
38 37 impcom 
 |-  ( ( A e. V /\ N e. NN0 ) -> ( ( _I |` A ) ^r N ) = ( _I |` A ) )