Metamath Proof Explorer

Theorem relexpaddnn

Description: Relation composition becomes addition under exponentiation. (Contributed by RP, 23-May-2020)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( n = 1 -> ( R ^r n ) = ( R ^r 1 ) )
2 1 coeq1d 
 |-  ( n = 1 -> ( ( R ^r n ) o. ( R ^r M ) ) = ( ( R ^r 1 ) o. ( R ^r M ) ) )
3 oveq1 
 |-  ( n = 1 -> ( n + M ) = ( 1 + M ) )
4 3 oveq2d 
 |-  ( n = 1 -> ( R ^r ( n + M ) ) = ( R ^r ( 1 + M ) ) )
5 2 4 eqeq12d 
 |-  ( n = 1 -> ( ( ( R ^r n ) o. ( R ^r M ) ) = ( R ^r ( n + M ) ) <-> ( ( R ^r 1 ) o. ( R ^r M ) ) = ( R ^r ( 1 + M ) ) ) )
6 5 imbi2d 
 |-  ( n = 1 -> ( ( ( M e. NN /\ R e. V ) -> ( ( R ^r n ) o. ( R ^r M ) ) = ( R ^r ( n + M ) ) ) <-> ( ( M e. NN /\ R e. V ) -> ( ( R ^r 1 ) o. ( R ^r M ) ) = ( R ^r ( 1 + M ) ) ) ) )
7 oveq2 
 |-  ( n = k -> ( R ^r n ) = ( R ^r k ) )
8 7 coeq1d 
 |-  ( n = k -> ( ( R ^r n ) o. ( R ^r M ) ) = ( ( R ^r k ) o. ( R ^r M ) ) )
9 oveq1 
 |-  ( n = k -> ( n + M ) = ( k + M ) )
10 9 oveq2d 
 |-  ( n = k -> ( R ^r ( n + M ) ) = ( R ^r ( k + M ) ) )
11 8 10 eqeq12d 
 |-  ( n = k -> ( ( ( R ^r n ) o. ( R ^r M ) ) = ( R ^r ( n + M ) ) <-> ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) )
12 11 imbi2d 
 |-  ( n = k -> ( ( ( M e. NN /\ R e. V ) -> ( ( R ^r n ) o. ( R ^r M ) ) = ( R ^r ( n + M ) ) ) <-> ( ( M e. NN /\ R e. V ) -> ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) ) )
13 oveq2 
 |-  ( n = ( k + 1 ) -> ( R ^r n ) = ( R ^r ( k + 1 ) ) )
14 13 coeq1d 
 |-  ( n = ( k + 1 ) -> ( ( R ^r n ) o. ( R ^r M ) ) = ( ( R ^r ( k + 1 ) ) o. ( R ^r M ) ) )
15 oveq1 
 |-  ( n = ( k + 1 ) -> ( n + M ) = ( ( k + 1 ) + M ) )
16 15 oveq2d 
 |-  ( n = ( k + 1 ) -> ( R ^r ( n + M ) ) = ( R ^r ( ( k + 1 ) + M ) ) )
17 14 16 eqeq12d 
 |-  ( n = ( k + 1 ) -> ( ( ( R ^r n ) o. ( R ^r M ) ) = ( R ^r ( n + M ) ) <-> ( ( R ^r ( k + 1 ) ) o. ( R ^r M ) ) = ( R ^r ( ( k + 1 ) + M ) ) ) )
18 17 imbi2d 
 |-  ( n = ( k + 1 ) -> ( ( ( M e. NN /\ R e. V ) -> ( ( R ^r n ) o. ( R ^r M ) ) = ( R ^r ( n + M ) ) ) <-> ( ( M e. NN /\ R e. V ) -> ( ( R ^r ( k + 1 ) ) o. ( R ^r M ) ) = ( R ^r ( ( k + 1 ) + M ) ) ) ) )
19 oveq2 
 |-  ( n = N -> ( R ^r n ) = ( R ^r N ) )
20 19 coeq1d 
 |-  ( n = N -> ( ( R ^r n ) o. ( R ^r M ) ) = ( ( R ^r N ) o. ( R ^r M ) ) )
21 oveq1 
 |-  ( n = N -> ( n + M ) = ( N + M ) )
22 21 oveq2d 
 |-  ( n = N -> ( R ^r ( n + M ) ) = ( R ^r ( N + M ) ) )
23 20 22 eqeq12d 
 |-  ( n = N -> ( ( ( R ^r n ) o. ( R ^r M ) ) = ( R ^r ( n + M ) ) <-> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) )
24 23 imbi2d 
 |-  ( n = N -> ( ( ( M e. NN /\ R e. V ) -> ( ( R ^r n ) o. ( R ^r M ) ) = ( R ^r ( n + M ) ) ) <-> ( ( M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) )
25 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
26 25 adantl 
 |-  ( ( M e. NN /\ R e. V ) -> ( R ^r 1 ) = R )
27 26 coeq1d 
 |-  ( ( M e. NN /\ R e. V ) -> ( ( R ^r 1 ) o. ( R ^r M ) ) = ( R o. ( R ^r M ) ) )
28 relexpsucnnl 
 |-  ( ( R e. V /\ M e. NN ) -> ( R ^r ( M + 1 ) ) = ( R o. ( R ^r M ) ) )
29 28 ancoms 
 |-  ( ( M e. NN /\ R e. V ) -> ( R ^r ( M + 1 ) ) = ( R o. ( R ^r M ) ) )
30 simpl 
 |-  ( ( M e. NN /\ R e. V ) -> M e. NN )
31 30 nncnd 
 |-  ( ( M e. NN /\ R e. V ) -> M e. CC )
32 1cnd 
 |-  ( ( M e. NN /\ R e. V ) -> 1 e. CC )
33 31 32 addcomd 
 |-  ( ( M e. NN /\ R e. V ) -> ( M + 1 ) = ( 1 + M ) )
34 33 oveq2d 
 |-  ( ( M e. NN /\ R e. V ) -> ( R ^r ( M + 1 ) ) = ( R ^r ( 1 + M ) ) )
35 27 29 34 3eqtr2d 
 |-  ( ( M e. NN /\ R e. V ) -> ( ( R ^r 1 ) o. ( R ^r M ) ) = ( R ^r ( 1 + M ) ) )
36 simp2r 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> R e. V )
37 simp1 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> k e. NN )
38 relexpsucnnl 
 |-  ( ( R e. V /\ k e. NN ) -> ( R ^r ( k + 1 ) ) = ( R o. ( R ^r k ) ) )
39 36 37 38 syl2anc 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> ( R ^r ( k + 1 ) ) = ( R o. ( R ^r k ) ) )
40 39 coeq1d 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> ( ( R ^r ( k + 1 ) ) o. ( R ^r M ) ) = ( ( R o. ( R ^r k ) ) o. ( R ^r M ) ) )
41 coass 
 |-  ( ( R o. ( R ^r k ) ) o. ( R ^r M ) ) = ( R o. ( ( R ^r k ) o. ( R ^r M ) ) )
42 40 41 eqtrdi 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> ( ( R ^r ( k + 1 ) ) o. ( R ^r M ) ) = ( R o. ( ( R ^r k ) o. ( R ^r M ) ) ) )
43 simp3 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) )
44 43 coeq2d 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> ( R o. ( ( R ^r k ) o. ( R ^r M ) ) ) = ( R o. ( R ^r ( k + M ) ) ) )
45 37 nncnd 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> k e. CC )
46 1cnd 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> 1 e. CC )
47 31 3ad2ant2 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> M e. CC )
48 45 46 47 add32d 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> ( ( k + 1 ) + M ) = ( ( k + M ) + 1 ) )
49 48 oveq2d 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> ( R ^r ( ( k + 1 ) + M ) ) = ( R ^r ( ( k + M ) + 1 ) ) )
50 30 3ad2ant2 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> M e. NN )
51 37 50 nnaddcld 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> ( k + M ) e. NN )
52 relexpsucnnl 
 |-  ( ( R e. V /\ ( k + M ) e. NN ) -> ( R ^r ( ( k + M ) + 1 ) ) = ( R o. ( R ^r ( k + M ) ) ) )
53 36 51 52 syl2anc 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> ( R ^r ( ( k + M ) + 1 ) ) = ( R o. ( R ^r ( k + M ) ) ) )
54 49 53 eqtr2d 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> ( R o. ( R ^r ( k + M ) ) ) = ( R ^r ( ( k + 1 ) + M ) ) )
55 42 44 54 3eqtrd 
 |-  ( ( k e. NN /\ ( M e. NN /\ R e. V ) /\ ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> ( ( R ^r ( k + 1 ) ) o. ( R ^r M ) ) = ( R ^r ( ( k + 1 ) + M ) ) )
56 55 3exp 
 |-  ( k e. NN -> ( ( M e. NN /\ R e. V ) -> ( ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) -> ( ( R ^r ( k + 1 ) ) o. ( R ^r M ) ) = ( R ^r ( ( k + 1 ) + M ) ) ) ) )
57 56 a2d 
 |-  ( k e. NN -> ( ( ( M e. NN /\ R e. V ) -> ( ( R ^r k ) o. ( R ^r M ) ) = ( R ^r ( k + M ) ) ) -> ( ( M e. NN /\ R e. V ) -> ( ( R ^r ( k + 1 ) ) o. ( R ^r M ) ) = ( R ^r ( ( k + 1 ) + M ) ) ) ) )
58 6 12 18 24 35 57 nnind 
 |-  ( N e. NN -> ( ( M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) )
59 58 3impib 
 |-  ( ( N e. NN /\ M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )