Metamath Proof Explorer

Theorem relexpsucl

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

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

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 relexpsucnnl 
 |-  ( ( R e. V /\ N e. NN ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )
5 2 3 4 syl2anc 
 |-  ( ( N e. NN /\ Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )
6 5 3expib 
 |-  ( N e. NN -> ( ( Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) ) )
7 simp2 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> Rel R )
8 relcoi1 
 |-  ( Rel R -> ( R o. ( _I |` U. U. R ) ) = R )
9 7 8 syl 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R o. ( _I |` U. U. R ) ) = R )
10 simp1 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> N = 0 )
11 10 oveq2d 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
12 simp3 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> R e. V )
13 relexp0 
 |-  ( ( R e. V /\ Rel R ) -> ( R ^r 0 ) = ( _I |` U. U. R ) )
14 12 7 13 syl2anc 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r 0 ) = ( _I |` U. U. R ) )
15 11 14 eqtrd 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r N ) = ( _I |` U. U. R ) )
16 15 coeq2d 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R o. ( R ^r N ) ) = ( R o. ( _I |` U. U. R ) ) )
17 10 oveq1d 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( N + 1 ) = ( 0 + 1 ) )
18 0p1e1 
 |-  ( 0 + 1 ) = 1
19 17 18 eqtrdi 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( N + 1 ) = 1 )
20 19 oveq2d 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( R ^r 1 ) )
21 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
22 12 21 syl 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r 1 ) = R )
23 20 22 eqtrd 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = R )
24 9 16 23 3eqtr4rd 
 |-  ( ( N = 0 /\ Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )
25 24 3expib 
 |-  ( N = 0 -> ( ( Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) ) )
26 6 25 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( ( Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) ) )
27 1 26 sylbi 
 |-  ( N e. NN0 -> ( ( Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) ) )
28 27 3impib 
 |-  ( ( N e. NN0 /\ Rel R /\ R e. V ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )
29 28 3com13 
 |-  ( ( R e. V /\ Rel R /\ N e. NN0 ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )