Metamath Proof Explorer

Theorem relexpsucr

Description: A reduction for relation exponentiation to the right. (Contributed by RP, 23-May-2020)

Ref Expression
Assertion relexpsucr 
|- ( ( R e. V /\ Rel R /\ N e. NN0 ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 simp3 
 |-  ( ( N e. NN /\ Rel R /\ R e. V ) -> R e. V )
3 simp1 
 |-  ( ( N e. NN /\ Rel R /\ R e. V ) -> N e. NN )
4 relexpsucnnr 
 |-  ( ( R e. V /\ N e. NN ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )
5 2 3 4 syl2anc 
 |-  ( ( N e. NN /\ Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )
6 5 3expib 
 |-  ( N e. NN -> ( ( Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) )
7 simp2 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> Rel R )
8 relcoi2 
 |-  ( Rel R -> ( ( _I |` U. U. R ) o. R ) = R )
9 8 eqcomd 
 |-  ( Rel R -> R = ( ( _I |` U. U. R ) o. R ) )
10 7 9 syl 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> R = ( ( _I |` U. U. R ) o. R ) )
11 simp1 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> N = 0 )
12 11 oveq1d 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( N + 1 ) = ( 0 + 1 ) )
13 0p1e1 
 |-  ( 0 + 1 ) = 1
14 12 13 eqtrdi 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( N + 1 ) = 1 )
15 14 oveq2d 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( R ^r 1 ) )
16 simp3 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> R e. V )
17 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
18 16 17 syl 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r 1 ) = R )
19 15 18 eqtrd 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = R )
20 11 oveq2d 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
21 relexp0 
 |-  ( ( R e. V /\ Rel R ) -> ( R ^r 0 ) = ( _I |` U. U. R ) )
22 16 7 21 syl2anc 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r 0 ) = ( _I |` U. U. R ) )
23 20 22 eqtrd 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r N ) = ( _I |` U. U. R ) )
24 23 coeq1d 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( ( R ^r N ) o. R ) = ( ( _I |` U. U. R ) o. R ) )
25 10 19 24 3eqtr4d 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )
26 25 3expib 
 |-  ( N = 0 -> ( ( Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) )
27 6 26 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( ( Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) )
28 1 27 sylbi 
 |-  ( N e. NN0 -> ( ( Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) )
29 28 3impib 
 |-  ( ( N e. NN0 /\ Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )
30 29 3com13 
 |-  ( ( R e. V /\ Rel R /\ N e. NN0 ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )