Metamath Proof Explorer

Theorem relexpsucnnl

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

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

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( n = 1 -> ( n + 1 ) = ( 1 + 1 ) )
2 1 oveq2d 
 |-  ( n = 1 -> ( R ^r ( n + 1 ) ) = ( R ^r ( 1 + 1 ) ) )
3 oveq2 
 |-  ( n = 1 -> ( R ^r n ) = ( R ^r 1 ) )
4 3 coeq2d 
 |-  ( n = 1 -> ( R o. ( R ^r n ) ) = ( R o. ( R ^r 1 ) ) )
5 2 4 eqeq12d 
 |-  ( n = 1 -> ( ( R ^r ( n + 1 ) ) = ( R o. ( R ^r n ) ) <-> ( R ^r ( 1 + 1 ) ) = ( R o. ( R ^r 1 ) ) ) )
6 5 imbi2d 
 |-  ( n = 1 -> ( ( R e. V -> ( R ^r ( n + 1 ) ) = ( R o. ( R ^r n ) ) ) <-> ( R e. V -> ( R ^r ( 1 + 1 ) ) = ( R o. ( R ^r 1 ) ) ) ) )
7 oveq1 
 |-  ( n = m -> ( n + 1 ) = ( m + 1 ) )
8 7 oveq2d 
 |-  ( n = m -> ( R ^r ( n + 1 ) ) = ( R ^r ( m + 1 ) ) )
9 oveq2 
 |-  ( n = m -> ( R ^r n ) = ( R ^r m ) )
10 9 coeq2d 
 |-  ( n = m -> ( R o. ( R ^r n ) ) = ( R o. ( R ^r m ) ) )
11 8 10 eqeq12d 
 |-  ( n = m -> ( ( R ^r ( n + 1 ) ) = ( R o. ( R ^r n ) ) <-> ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) ) )
12 11 imbi2d 
 |-  ( n = m -> ( ( R e. V -> ( R ^r ( n + 1 ) ) = ( R o. ( R ^r n ) ) ) <-> ( R e. V -> ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) ) ) )
13 oveq1 
 |-  ( n = ( m + 1 ) -> ( n + 1 ) = ( ( m + 1 ) + 1 ) )
14 13 oveq2d 
 |-  ( n = ( m + 1 ) -> ( R ^r ( n + 1 ) ) = ( R ^r ( ( m + 1 ) + 1 ) ) )
15 oveq2 
 |-  ( n = ( m + 1 ) -> ( R ^r n ) = ( R ^r ( m + 1 ) ) )
16 15 coeq2d 
 |-  ( n = ( m + 1 ) -> ( R o. ( R ^r n ) ) = ( R o. ( R ^r ( m + 1 ) ) ) )
17 14 16 eqeq12d 
 |-  ( n = ( m + 1 ) -> ( ( R ^r ( n + 1 ) ) = ( R o. ( R ^r n ) ) <-> ( R ^r ( ( m + 1 ) + 1 ) ) = ( R o. ( R ^r ( m + 1 ) ) ) ) )
18 17 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( R e. V -> ( R ^r ( n + 1 ) ) = ( R o. ( R ^r n ) ) ) <-> ( R e. V -> ( R ^r ( ( m + 1 ) + 1 ) ) = ( R o. ( R ^r ( m + 1 ) ) ) ) ) )
19 oveq1 
 |-  ( n = N -> ( n + 1 ) = ( N + 1 ) )
20 19 oveq2d 
 |-  ( n = N -> ( R ^r ( n + 1 ) ) = ( R ^r ( N + 1 ) ) )
21 oveq2 
 |-  ( n = N -> ( R ^r n ) = ( R ^r N ) )
22 21 coeq2d 
 |-  ( n = N -> ( R o. ( R ^r n ) ) = ( R o. ( R ^r N ) ) )
23 20 22 eqeq12d 
 |-  ( n = N -> ( ( R ^r ( n + 1 ) ) = ( R o. ( R ^r n ) ) <-> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) ) )
24 23 imbi2d 
 |-  ( n = N -> ( ( R e. V -> ( R ^r ( n + 1 ) ) = ( R o. ( R ^r n ) ) ) <-> ( R e. V -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) ) ) )
25 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
26 25 coeq1d 
 |-  ( R e. V -> ( ( R ^r 1 ) o. R ) = ( R o. R ) )
27 1nn 
 |-  1 e. NN
28 relexpsucnnr 
 |-  ( ( R e. V /\ 1 e. NN ) -> ( R ^r ( 1 + 1 ) ) = ( ( R ^r 1 ) o. R ) )
29 27 28 mpan2 
 |-  ( R e. V -> ( R ^r ( 1 + 1 ) ) = ( ( R ^r 1 ) o. R ) )
30 25 coeq2d 
 |-  ( R e. V -> ( R o. ( R ^r 1 ) ) = ( R o. R ) )
31 26 29 30 3eqtr4d 
 |-  ( R e. V -> ( R ^r ( 1 + 1 ) ) = ( R o. ( R ^r 1 ) ) )
32 coeq1 
 |-  ( ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) -> ( ( R ^r ( m + 1 ) ) o. R ) = ( ( R o. ( R ^r m ) ) o. R ) )
33 coass 
 |-  ( ( R o. ( R ^r m ) ) o. R ) = ( R o. ( ( R ^r m ) o. R ) )
34 32 33 eqtrdi 
 |-  ( ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) -> ( ( R ^r ( m + 1 ) ) o. R ) = ( R o. ( ( R ^r m ) o. R ) ) )
35 34 adantl 
 |-  ( ( ( R e. V /\ m e. NN ) /\ ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) ) -> ( ( R ^r ( m + 1 ) ) o. R ) = ( R o. ( ( R ^r m ) o. R ) ) )
36 simpl 
 |-  ( ( ( R e. V /\ m e. NN ) /\ ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) ) -> ( R e. V /\ m e. NN ) )
37 peano2nn 
 |-  ( m e. NN -> ( m + 1 ) e. NN )
38 37 anim2i 
 |-  ( ( R e. V /\ m e. NN ) -> ( R e. V /\ ( m + 1 ) e. NN ) )
39 relexpsucnnr 
 |-  ( ( R e. V /\ ( m + 1 ) e. NN ) -> ( R ^r ( ( m + 1 ) + 1 ) ) = ( ( R ^r ( m + 1 ) ) o. R ) )
40 36 38 39 3syl 
 |-  ( ( ( R e. V /\ m e. NN ) /\ ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) ) -> ( R ^r ( ( m + 1 ) + 1 ) ) = ( ( R ^r ( m + 1 ) ) o. R ) )
41 relexpsucnnr 
 |-  ( ( R e. V /\ m e. NN ) -> ( R ^r ( m + 1 ) ) = ( ( R ^r m ) o. R ) )
42 41 adantr 
 |-  ( ( ( R e. V /\ m e. NN ) /\ ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) ) -> ( R ^r ( m + 1 ) ) = ( ( R ^r m ) o. R ) )
43 42 coeq2d 
 |-  ( ( ( R e. V /\ m e. NN ) /\ ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) ) -> ( R o. ( R ^r ( m + 1 ) ) ) = ( R o. ( ( R ^r m ) o. R ) ) )
44 35 40 43 3eqtr4d 
 |-  ( ( ( R e. V /\ m e. NN ) /\ ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) ) -> ( R ^r ( ( m + 1 ) + 1 ) ) = ( R o. ( R ^r ( m + 1 ) ) ) )
45 44 ex 
 |-  ( ( R e. V /\ m e. NN ) -> ( ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) -> ( R ^r ( ( m + 1 ) + 1 ) ) = ( R o. ( R ^r ( m + 1 ) ) ) ) )
46 45 expcom 
 |-  ( m e. NN -> ( R e. V -> ( ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) -> ( R ^r ( ( m + 1 ) + 1 ) ) = ( R o. ( R ^r ( m + 1 ) ) ) ) ) )
47 46 a2d 
 |-  ( m e. NN -> ( ( R e. V -> ( R ^r ( m + 1 ) ) = ( R o. ( R ^r m ) ) ) -> ( R e. V -> ( R ^r ( ( m + 1 ) + 1 ) ) = ( R o. ( R ^r ( m + 1 ) ) ) ) ) )
48 6 12 18 24 31 47 nnind 
 |-  ( N e. NN -> ( R e. V -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) ) )
49 48 impcom 
 |-  ( ( R e. V /\ N e. NN ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )