Metamath Proof Explorer

Theorem relexpcnv

Description: Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020)

Ref Expression
Assertion relexpcnv 
|- ( ( N e. NN0 /\ R e. V ) -> `' ( R ^r N ) = ( `' R ^r N ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 oveq2 
 |-  ( n = 1 -> ( R ^r n ) = ( R ^r 1 ) )
3 2 cnveqd 
 |-  ( n = 1 -> `' ( R ^r n ) = `' ( R ^r 1 ) )
4 oveq2 
 |-  ( n = 1 -> ( `' R ^r n ) = ( `' R ^r 1 ) )
5 3 4 eqeq12d 
 |-  ( n = 1 -> ( `' ( R ^r n ) = ( `' R ^r n ) <-> `' ( R ^r 1 ) = ( `' R ^r 1 ) ) )
6 5 imbi2d 
 |-  ( n = 1 -> ( ( R e. V -> `' ( R ^r n ) = ( `' R ^r n ) ) <-> ( R e. V -> `' ( R ^r 1 ) = ( `' R ^r 1 ) ) ) )
7 oveq2 
 |-  ( n = m -> ( R ^r n ) = ( R ^r m ) )
8 7 cnveqd 
 |-  ( n = m -> `' ( R ^r n ) = `' ( R ^r m ) )
9 oveq2 
 |-  ( n = m -> ( `' R ^r n ) = ( `' R ^r m ) )
10 8 9 eqeq12d 
 |-  ( n = m -> ( `' ( R ^r n ) = ( `' R ^r n ) <-> `' ( R ^r m ) = ( `' R ^r m ) ) )
11 10 imbi2d 
 |-  ( n = m -> ( ( R e. V -> `' ( R ^r n ) = ( `' R ^r n ) ) <-> ( R e. V -> `' ( R ^r m ) = ( `' R ^r m ) ) ) )
12 oveq2 
 |-  ( n = ( m + 1 ) -> ( R ^r n ) = ( R ^r ( m + 1 ) ) )
13 12 cnveqd 
 |-  ( n = ( m + 1 ) -> `' ( R ^r n ) = `' ( R ^r ( m + 1 ) ) )
14 oveq2 
 |-  ( n = ( m + 1 ) -> ( `' R ^r n ) = ( `' R ^r ( m + 1 ) ) )
15 13 14 eqeq12d 
 |-  ( n = ( m + 1 ) -> ( `' ( R ^r n ) = ( `' R ^r n ) <-> `' ( R ^r ( m + 1 ) ) = ( `' R ^r ( m + 1 ) ) ) )
16 15 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( R e. V -> `' ( R ^r n ) = ( `' R ^r n ) ) <-> ( R e. V -> `' ( R ^r ( m + 1 ) ) = ( `' R ^r ( m + 1 ) ) ) ) )
17 oveq2 
 |-  ( n = N -> ( R ^r n ) = ( R ^r N ) )
18 17 cnveqd 
 |-  ( n = N -> `' ( R ^r n ) = `' ( R ^r N ) )
19 oveq2 
 |-  ( n = N -> ( `' R ^r n ) = ( `' R ^r N ) )
20 18 19 eqeq12d 
 |-  ( n = N -> ( `' ( R ^r n ) = ( `' R ^r n ) <-> `' ( R ^r N ) = ( `' R ^r N ) ) )
21 20 imbi2d 
 |-  ( n = N -> ( ( R e. V -> `' ( R ^r n ) = ( `' R ^r n ) ) <-> ( R e. V -> `' ( R ^r N ) = ( `' R ^r N ) ) ) )
22 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
23 22 cnveqd 
 |-  ( R e. V -> `' ( R ^r 1 ) = `' R )
24 cnvexg 
 |-  ( R e. V -> `' R e. _V )
25 relexp1g 
 |-  ( `' R e. _V -> ( `' R ^r 1 ) = `' R )
26 24 25 syl 
 |-  ( R e. V -> ( `' R ^r 1 ) = `' R )
27 23 26 eqtr4d 
 |-  ( R e. V -> `' ( R ^r 1 ) = ( `' R ^r 1 ) )
28 cnvco 
 |-  `' ( ( R ^r m ) o. R ) = ( `' R o. `' ( R ^r m ) )
29 simp3 
 |-  ( ( m e. NN /\ R e. V /\ `' ( R ^r m ) = ( `' R ^r m ) ) -> `' ( R ^r m ) = ( `' R ^r m ) )
30 29 coeq2d 
 |-  ( ( m e. NN /\ R e. V /\ `' ( R ^r m ) = ( `' R ^r m ) ) -> ( `' R o. `' ( R ^r m ) ) = ( `' R o. ( `' R ^r m ) ) )
31 28 30 eqtrid 
 |-  ( ( m e. NN /\ R e. V /\ `' ( R ^r m ) = ( `' R ^r m ) ) -> `' ( ( R ^r m ) o. R ) = ( `' R o. ( `' R ^r m ) ) )
32 simp2 
 |-  ( ( m e. NN /\ R e. V /\ `' ( R ^r m ) = ( `' R ^r m ) ) -> R e. V )
33 simp1 
 |-  ( ( m e. NN /\ R e. V /\ `' ( R ^r m ) = ( `' R ^r m ) ) -> m e. NN )
34 relexpsucnnr 
 |-  ( ( R e. V /\ m e. NN ) -> ( R ^r ( m + 1 ) ) = ( ( R ^r m ) o. R ) )
35 32 33 34 syl2anc 
 |-  ( ( m e. NN /\ R e. V /\ `' ( R ^r m ) = ( `' R ^r m ) ) -> ( R ^r ( m + 1 ) ) = ( ( R ^r m ) o. R ) )
36 35 cnveqd 
 |-  ( ( m e. NN /\ R e. V /\ `' ( R ^r m ) = ( `' R ^r m ) ) -> `' ( R ^r ( m + 1 ) ) = `' ( ( R ^r m ) o. R ) )
37 32 24 syl 
 |-  ( ( m e. NN /\ R e. V /\ `' ( R ^r m ) = ( `' R ^r m ) ) -> `' R e. _V )
38 relexpsucnnl 
 |-  ( ( `' R e. _V /\ m e. NN ) -> ( `' R ^r ( m + 1 ) ) = ( `' R o. ( `' R ^r m ) ) )
39 37 33 38 syl2anc 
 |-  ( ( m e. NN /\ R e. V /\ `' ( R ^r m ) = ( `' R ^r m ) ) -> ( `' R ^r ( m + 1 ) ) = ( `' R o. ( `' R ^r m ) ) )
40 31 36 39 3eqtr4d 
 |-  ( ( m e. NN /\ R e. V /\ `' ( R ^r m ) = ( `' R ^r m ) ) -> `' ( R ^r ( m + 1 ) ) = ( `' R ^r ( m + 1 ) ) )
41 40 3exp 
 |-  ( m e. NN -> ( R e. V -> ( `' ( R ^r m ) = ( `' R ^r m ) -> `' ( R ^r ( m + 1 ) ) = ( `' R ^r ( m + 1 ) ) ) ) )
42 41 a2d 
 |-  ( m e. NN -> ( ( R e. V -> `' ( R ^r m ) = ( `' R ^r m ) ) -> ( R e. V -> `' ( R ^r ( m + 1 ) ) = ( `' R ^r ( m + 1 ) ) ) ) )
43 6 11 16 21 27 42 nnind 
 |-  ( N e. NN -> ( R e. V -> `' ( R ^r N ) = ( `' R ^r N ) ) )
44 cnvresid 
 |-  `' ( _I |` ( dom R u. ran R ) ) = ( _I |` ( dom R u. ran R ) )
45 uncom 
 |-  ( dom R u. ran R ) = ( ran R u. dom R )
46 df-rn 
 |-  ran R = dom `' R
47 dfdm4 
 |-  dom R = ran `' R
48 46 47 uneq12i 
 |-  ( ran R u. dom R ) = ( dom `' R u. ran `' R )
49 45 48 eqtri 
 |-  ( dom R u. ran R ) = ( dom `' R u. ran `' R )
50 49 reseq2i 
 |-  ( _I |` ( dom R u. ran R ) ) = ( _I |` ( dom `' R u. ran `' R ) )
51 44 50 eqtri 
 |-  `' ( _I |` ( dom R u. ran R ) ) = ( _I |` ( dom `' R u. ran `' R ) )
52 oveq2 
 |-  ( N = 0 -> ( R ^r N ) = ( R ^r 0 ) )
53 relexp0g 
 |-  ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
54 52 53 sylan9eq 
 |-  ( ( N = 0 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
55 54 cnveqd 
 |-  ( ( N = 0 /\ R e. V ) -> `' ( R ^r N ) = `' ( _I |` ( dom R u. ran R ) ) )
56 oveq2 
 |-  ( N = 0 -> ( `' R ^r N ) = ( `' R ^r 0 ) )
57 56 adantr 
 |-  ( ( N = 0 /\ R e. V ) -> ( `' R ^r N ) = ( `' R ^r 0 ) )
58 simpr 
 |-  ( ( N = 0 /\ R e. V ) -> R e. V )
59 relexp0g 
 |-  ( `' R e. _V -> ( `' R ^r 0 ) = ( _I |` ( dom `' R u. ran `' R ) ) )
60 58 24 59 3syl 
 |-  ( ( N = 0 /\ R e. V ) -> ( `' R ^r 0 ) = ( _I |` ( dom `' R u. ran `' R ) ) )
61 57 60 eqtrd 
 |-  ( ( N = 0 /\ R e. V ) -> ( `' R ^r N ) = ( _I |` ( dom `' R u. ran `' R ) ) )
62 51 55 61 3eqtr4a 
 |-  ( ( N = 0 /\ R e. V ) -> `' ( R ^r N ) = ( `' R ^r N ) )
63 62 ex 
 |-  ( N = 0 -> ( R e. V -> `' ( R ^r N ) = ( `' R ^r N ) ) )
64 43 63 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( R e. V -> `' ( R ^r N ) = ( `' R ^r N ) ) )
65 1 64 sylbi 
 |-  ( N e. NN0 -> ( R e. V -> `' ( R ^r N ) = ( `' R ^r N ) ) )
66 65 imp 
 |-  ( ( N e. NN0 /\ R e. V ) -> `' ( R ^r N ) = ( `' R ^r N ) )