Metamath Proof Explorer

Theorem relexpmulnn

Description: With exponents limited to the counting numbers, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020)

Ref Expression
Assertion relexpmulnn 
|- ( ( ( R e. V /\ I = ( J x. K ) ) /\ ( J e. NN /\ K e. NN ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = 1 -> ( ( R ^r J ) ^r x ) = ( ( R ^r J ) ^r 1 ) )
2 oveq2 
 |-  ( x = 1 -> ( J x. x ) = ( J x. 1 ) )
3 2 oveq2d 
 |-  ( x = 1 -> ( R ^r ( J x. x ) ) = ( R ^r ( J x. 1 ) ) )
4 1 3 eqeq12d 
 |-  ( x = 1 -> ( ( ( R ^r J ) ^r x ) = ( R ^r ( J x. x ) ) <-> ( ( R ^r J ) ^r 1 ) = ( R ^r ( J x. 1 ) ) ) )
5 4 imbi2d 
 |-  ( x = 1 -> ( ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r x ) = ( R ^r ( J x. x ) ) ) <-> ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r 1 ) = ( R ^r ( J x. 1 ) ) ) ) )
6 oveq2 
 |-  ( x = y -> ( ( R ^r J ) ^r x ) = ( ( R ^r J ) ^r y ) )
7 oveq2 
 |-  ( x = y -> ( J x. x ) = ( J x. y ) )
8 7 oveq2d 
 |-  ( x = y -> ( R ^r ( J x. x ) ) = ( R ^r ( J x. y ) ) )
9 6 8 eqeq12d 
 |-  ( x = y -> ( ( ( R ^r J ) ^r x ) = ( R ^r ( J x. x ) ) <-> ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) )
10 9 imbi2d 
 |-  ( x = y -> ( ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r x ) = ( R ^r ( J x. x ) ) ) <-> ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) ) )
11 oveq2 
 |-  ( x = ( y + 1 ) -> ( ( R ^r J ) ^r x ) = ( ( R ^r J ) ^r ( y + 1 ) ) )
12 oveq2 
 |-  ( x = ( y + 1 ) -> ( J x. x ) = ( J x. ( y + 1 ) ) )
13 12 oveq2d 
 |-  ( x = ( y + 1 ) -> ( R ^r ( J x. x ) ) = ( R ^r ( J x. ( y + 1 ) ) ) )
14 11 13 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( ( R ^r J ) ^r x ) = ( R ^r ( J x. x ) ) <-> ( ( R ^r J ) ^r ( y + 1 ) ) = ( R ^r ( J x. ( y + 1 ) ) ) ) )
15 14 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r x ) = ( R ^r ( J x. x ) ) ) <-> ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r ( y + 1 ) ) = ( R ^r ( J x. ( y + 1 ) ) ) ) ) )
16 oveq2 
 |-  ( x = K -> ( ( R ^r J ) ^r x ) = ( ( R ^r J ) ^r K ) )
17 oveq2 
 |-  ( x = K -> ( J x. x ) = ( J x. K ) )
18 17 oveq2d 
 |-  ( x = K -> ( R ^r ( J x. x ) ) = ( R ^r ( J x. K ) ) )
19 16 18 eqeq12d 
 |-  ( x = K -> ( ( ( R ^r J ) ^r x ) = ( R ^r ( J x. x ) ) <-> ( ( R ^r J ) ^r K ) = ( R ^r ( J x. K ) ) ) )
20 19 imbi2d 
 |-  ( x = K -> ( ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r x ) = ( R ^r ( J x. x ) ) ) <-> ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r ( J x. K ) ) ) ) )
21 ovexd 
 |-  ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( R ^r J ) e. _V )
22 21 relexp1d 
 |-  ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r 1 ) = ( R ^r J ) )
23 simp1 
 |-  ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> J e. NN )
24 nnre 
 |-  ( J e. NN -> J e. RR )
25 ax-1rid 
 |-  ( J e. RR -> ( J x. 1 ) = J )
26 23 24 25 3syl 
 |-  ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( J x. 1 ) = J )
27 26 eqcomd 
 |-  ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> J = ( J x. 1 ) )
28 27 oveq2d 
 |-  ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( R ^r J ) = ( R ^r ( J x. 1 ) ) )
29 22 28 eqtrd 
 |-  ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r 1 ) = ( R ^r ( J x. 1 ) ) )
30 ovex 
 |-  ( R ^r J ) e. _V
31 simp1 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> y e. NN )
32 relexpsucnnr 
 |-  ( ( ( R ^r J ) e. _V /\ y e. NN ) -> ( ( R ^r J ) ^r ( y + 1 ) ) = ( ( ( R ^r J ) ^r y ) o. ( R ^r J ) ) )
33 30 31 32 sylancr 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( ( R ^r J ) ^r ( y + 1 ) ) = ( ( ( R ^r J ) ^r y ) o. ( R ^r J ) ) )
34 simp3 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) )
35 34 coeq1d 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( ( ( R ^r J ) ^r y ) o. ( R ^r J ) ) = ( ( R ^r ( J x. y ) ) o. ( R ^r J ) ) )
36 simp21 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> J e. NN )
37 36 31 nnmulcld 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( J x. y ) e. NN )
38 simp22 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> R e. V )
39 relexpaddnn 
 |-  ( ( ( J x. y ) e. NN /\ J e. NN /\ R e. V ) -> ( ( R ^r ( J x. y ) ) o. ( R ^r J ) ) = ( R ^r ( ( J x. y ) + J ) ) )
40 37 36 38 39 syl3anc 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( ( R ^r ( J x. y ) ) o. ( R ^r J ) ) = ( R ^r ( ( J x. y ) + J ) ) )
41 35 40 eqtrd 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( ( ( R ^r J ) ^r y ) o. ( R ^r J ) ) = ( R ^r ( ( J x. y ) + J ) ) )
42 36 nncnd 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> J e. CC )
43 31 nncnd 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> y e. CC )
44 1cnd 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> 1 e. CC )
45 42 43 44 adddid 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( J x. ( y + 1 ) ) = ( ( J x. y ) + ( J x. 1 ) ) )
46 42 mulid1d 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( J x. 1 ) = J )
47 46 oveq2d 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( ( J x. y ) + ( J x. 1 ) ) = ( ( J x. y ) + J ) )
48 45 47 eqtr2d 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( ( J x. y ) + J ) = ( J x. ( y + 1 ) ) )
49 48 oveq2d 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( R ^r ( ( J x. y ) + J ) ) = ( R ^r ( J x. ( y + 1 ) ) ) )
50 41 49 eqtrd 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( ( ( R ^r J ) ^r y ) o. ( R ^r J ) ) = ( R ^r ( J x. ( y + 1 ) ) ) )
51 33 50 eqtrd 
 |-  ( ( y e. NN /\ ( J e. NN /\ R e. V /\ I = ( J x. K ) ) /\ ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( ( R ^r J ) ^r ( y + 1 ) ) = ( R ^r ( J x. ( y + 1 ) ) ) )
52 51 3exp 
 |-  ( y e. NN -> ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) -> ( ( R ^r J ) ^r ( y + 1 ) ) = ( R ^r ( J x. ( y + 1 ) ) ) ) ) )
53 52 a2d 
 |-  ( y e. NN -> ( ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r y ) = ( R ^r ( J x. y ) ) ) -> ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r ( y + 1 ) ) = ( R ^r ( J x. ( y + 1 ) ) ) ) ) )
54 5 10 15 20 29 53 nnind 
 |-  ( K e. NN -> ( ( J e. NN /\ R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r ( J x. K ) ) ) )
55 54 3expd 
 |-  ( K e. NN -> ( J e. NN -> ( R e. V -> ( I = ( J x. K ) -> ( ( R ^r J ) ^r K ) = ( R ^r ( J x. K ) ) ) ) ) )
56 55 impcom 
 |-  ( ( J e. NN /\ K e. NN ) -> ( R e. V -> ( I = ( J x. K ) -> ( ( R ^r J ) ^r K ) = ( R ^r ( J x. K ) ) ) ) )
57 56 impd 
 |-  ( ( J e. NN /\ K e. NN ) -> ( ( R e. V /\ I = ( J x. K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r ( J x. K ) ) ) )
58 57 impcom 
 |-  ( ( ( R e. V /\ I = ( J x. K ) ) /\ ( J e. NN /\ K e. NN ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r ( J x. K ) ) )
59 simplr 
 |-  ( ( ( R e. V /\ I = ( J x. K ) ) /\ ( J e. NN /\ K e. NN ) ) -> I = ( J x. K ) )
60 59 eqcomd 
 |-  ( ( ( R e. V /\ I = ( J x. K ) ) /\ ( J e. NN /\ K e. NN ) ) -> ( J x. K ) = I )
61 60 oveq2d 
 |-  ( ( ( R e. V /\ I = ( J x. K ) ) /\ ( J e. NN /\ K e. NN ) ) -> ( R ^r ( J x. K ) ) = ( R ^r I ) )
62 58 61 eqtrd 
 |-  ( ( ( R e. V /\ I = ( J x. K ) ) /\ ( J e. NN /\ K e. NN ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )