Metamath Proof Explorer

Theorem relexpmulg

Description: With ordered exponents, 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 relexpmulg 
|- ( ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) /\ ( J e. NN0 /\ K e. NN0 ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( J e. NN0 <-> ( J e. NN \/ J = 0 ) )
2 elnn0 
 |-  ( K e. NN0 <-> ( K e. NN \/ K = 0 ) )
3 relexpmulnn 
 |-  ( ( ( R e. V /\ I = ( J x. K ) ) /\ ( J e. NN /\ K e. NN ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
4 3 3adantl3 
 |-  ( ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) /\ ( J e. NN /\ K e. NN ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
5 4 expcom 
 |-  ( ( J e. NN /\ K e. NN ) -> ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) )
6 5 expcom 
 |-  ( K e. NN -> ( J e. NN -> ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
7 simprr 
 |-  ( ( ( K = 0 /\ J e. NN ) /\ ( R e. V /\ I = ( J x. K ) ) ) -> I = ( J x. K ) )
8 simpll 
 |-  ( ( ( K = 0 /\ J e. NN ) /\ ( R e. V /\ I = ( J x. K ) ) ) -> K = 0 )
9 8 oveq2d 
 |-  ( ( ( K = 0 /\ J e. NN ) /\ ( R e. V /\ I = ( J x. K ) ) ) -> ( J x. K ) = ( J x. 0 ) )
10 simplr 
 |-  ( ( ( K = 0 /\ J e. NN ) /\ ( R e. V /\ I = ( J x. K ) ) ) -> J e. NN )
11 10 nncnd 
 |-  ( ( ( K = 0 /\ J e. NN ) /\ ( R e. V /\ I = ( J x. K ) ) ) -> J e. CC )
12 11 mul01d 
 |-  ( ( ( K = 0 /\ J e. NN ) /\ ( R e. V /\ I = ( J x. K ) ) ) -> ( J x. 0 ) = 0 )
13 7 9 12 3eqtrd 
 |-  ( ( ( K = 0 /\ J e. NN ) /\ ( R e. V /\ I = ( J x. K ) ) ) -> I = 0 )
14 simpl 
 |-  ( ( ( K = 0 /\ J e. NN ) /\ ( R e. V /\ I = ( J x. K ) ) ) -> ( K = 0 /\ J e. NN ) )
15 nnnle0 
 |-  ( J e. NN -> -. J <_ 0 )
16 15 adantl 
 |-  ( ( K = 0 /\ J e. NN ) -> -. J <_ 0 )
17 simpl 
 |-  ( ( K = 0 /\ J e. NN ) -> K = 0 )
18 17 breq2d 
 |-  ( ( K = 0 /\ J e. NN ) -> ( J <_ K <-> J <_ 0 ) )
19 16 18 mtbird 
 |-  ( ( K = 0 /\ J e. NN ) -> -. J <_ K )
20 14 19 syl 
 |-  ( ( ( K = 0 /\ J e. NN ) /\ ( R e. V /\ I = ( J x. K ) ) ) -> -. J <_ K )
21 13 20 jcnd 
 |-  ( ( ( K = 0 /\ J e. NN ) /\ ( R e. V /\ I = ( J x. K ) ) ) -> -. ( I = 0 -> J <_ K ) )
22 21 pm2.21d 
 |-  ( ( ( K = 0 /\ J e. NN ) /\ ( R e. V /\ I = ( J x. K ) ) ) -> ( ( I = 0 -> J <_ K ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) )
23 22 exp32 
 |-  ( ( K = 0 /\ J e. NN ) -> ( R e. V -> ( I = ( J x. K ) -> ( ( I = 0 -> J <_ K ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) ) )
24 23 3impd 
 |-  ( ( K = 0 /\ J e. NN ) -> ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) )
25 24 ex 
 |-  ( K = 0 -> ( J e. NN -> ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
26 6 25 jaoi 
 |-  ( ( K e. NN \/ K = 0 ) -> ( J e. NN -> ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
27 2 26 sylbi 
 |-  ( K e. NN0 -> ( J e. NN -> ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
28 simplr 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> J = 0 )
29 28 oveq2d 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> ( R ^r J ) = ( R ^r 0 ) )
30 simpr1 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> R e. V )
31 relexp0g 
 |-  ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
32 30 31 syl 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
33 29 32 eqtrd 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> ( R ^r J ) = ( _I |` ( dom R u. ran R ) ) )
34 33 oveq1d 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> ( ( R ^r J ) ^r K ) = ( ( _I |` ( dom R u. ran R ) ) ^r K ) )
35 dmexg 
 |-  ( R e. V -> dom R e. _V )
36 rnexg 
 |-  ( R e. V -> ran R e. _V )
37 unexg 
 |-  ( ( dom R e. _V /\ ran R e. _V ) -> ( dom R u. ran R ) e. _V )
38 35 36 37 syl2anc 
 |-  ( R e. V -> ( dom R u. ran R ) e. _V )
39 30 38 syl 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> ( dom R u. ran R ) e. _V )
40 simpll 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> K e. NN0 )
41 relexpiidm 
 |-  ( ( ( dom R u. ran R ) e. _V /\ K e. NN0 ) -> ( ( _I |` ( dom R u. ran R ) ) ^r K ) = ( _I |` ( dom R u. ran R ) ) )
42 39 40 41 syl2anc 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> ( ( _I |` ( dom R u. ran R ) ) ^r K ) = ( _I |` ( dom R u. ran R ) ) )
43 simpr2 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> I = ( J x. K ) )
44 28 oveq1d 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> ( J x. K ) = ( 0 x. K ) )
45 40 nn0cnd 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> K e. CC )
46 45 mul02d 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> ( 0 x. K ) = 0 )
47 43 44 46 3eqtrd 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> I = 0 )
48 47 oveq2d 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> ( R ^r I ) = ( R ^r 0 ) )
49 48 32 eqtr2d 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> ( _I |` ( dom R u. ran R ) ) = ( R ^r I ) )
50 34 42 49 3eqtrd 
 |-  ( ( ( K e. NN0 /\ J = 0 ) /\ ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
51 50 ex 
 |-  ( ( K e. NN0 /\ J = 0 ) -> ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) )
52 51 ex 
 |-  ( K e. NN0 -> ( J = 0 -> ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
53 27 52 jaod 
 |-  ( K e. NN0 -> ( ( J e. NN \/ J = 0 ) -> ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
54 1 53 syl5bi 
 |-  ( K e. NN0 -> ( J e. NN0 -> ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
55 54 impcom 
 |-  ( ( J e. NN0 /\ K e. NN0 ) -> ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) )
56 55 impcom 
 |-  ( ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) /\ ( J e. NN0 /\ K e. NN0 ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )