Metamath Proof Explorer

Theorem relexpaddg

Description: Relation composition becomes addition under exponentiation except when the exponents total to one and the class isn't a relation. (Contributed by RP, 30-May-2020)

Ref Expression
Assertion relexpaddg 
|- ( ( N e. NN0 /\ ( M e. NN0 /\ R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 elnn0 
 |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
3 relexpaddnn 
 |-  ( ( N e. NN /\ M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
4 3 a1d 
 |-  ( ( N e. NN /\ M e. NN /\ R e. V ) -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) )
5 4 3exp 
 |-  ( N e. NN -> ( M e. NN -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
6 5 com12 
 |-  ( M e. NN -> ( N e. NN -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
7 elnn1uz2 
 |-  ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
8 coires1 
 |-  ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( R ^r N ) |` ( dom R u. ran R ) )
9 simpll 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> N = 1 )
10 simplr 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> M = 0 )
11 9 10 oveq12d 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) = ( 1 + 0 ) )
12 1p0e1 
 |-  ( 1 + 0 ) = 1
13 11 12 eqtrdi 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) = 1 )
14 simprr 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( N + M ) = 1 -> Rel R ) )
15 13 14 mpd 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> Rel R )
16 9 oveq2d 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r N ) = ( R ^r 1 ) )
17 simprl 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> R e. V )
18 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
19 17 18 syl 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r 1 ) = R )
20 16 19 eqtrd 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r N ) = R )
21 20 releqd 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( Rel ( R ^r N ) <-> Rel R ) )
22 15 21 mpbird 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> Rel ( R ^r N ) )
23 1nn 
 |-  1 e. NN
24 9 23 eqeltrdi 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> N e. NN )
25 relexpnndm 
 |-  ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
26 24 17 25 syl2anc 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> dom ( R ^r N ) C_ dom R )
27 ssun1 
 |-  dom R C_ ( dom R u. ran R )
28 26 27 sstrdi 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
29 relssres 
 |-  ( ( Rel ( R ^r N ) /\ dom ( R ^r N ) C_ ( dom R u. ran R ) ) -> ( ( R ^r N ) |` ( dom R u. ran R ) ) = ( R ^r N ) )
30 22 28 29 syl2anc 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( R ^r N ) |` ( dom R u. ran R ) ) = ( R ^r N ) )
31 8 30 eqtrid 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( R ^r N ) )
32 10 oveq2d 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r M ) = ( R ^r 0 ) )
33 relexp0g 
 |-  ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
34 17 33 syl 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
35 32 34 eqtrd 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
36 35 coeq2d 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) )
37 10 oveq2d 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) = ( N + 0 ) )
38 ax-1cn 
 |-  1 e. CC
39 9 38 eqeltrdi 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> N e. CC )
40 39 addridd 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + 0 ) = N )
41 37 40 eqtrd 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) = N )
42 41 oveq2d 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r ( N + M ) ) = ( R ^r N ) )
43 31 36 42 3eqtr4d 
 |-  ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
44 43 exp43 
 |-  ( N = 1 -> ( M = 0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
45 simp1 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. ( ZZ>= ` 2 ) )
46 simp3 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> R e. V )
47 relexpuzrel 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r N ) )
48 45 46 47 syl2anc 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> Rel ( R ^r N ) )
49 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
50 45 49 syl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. NN )
51 50 46 25 syl2anc 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
52 51 27 sstrdi 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
53 48 52 29 syl2anc 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) |` ( dom R u. ran R ) ) = ( R ^r N ) )
54 8 53 eqtrid 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( R ^r N ) )
55 simp2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> M = 0 )
56 55 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
57 46 33 syl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
58 56 57 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
59 58 coeq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) )
60 55 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = ( N + 0 ) )
61 eluzelcn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. CC )
62 45 61 syl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. CC )
63 62 addridd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + 0 ) = N )
64 60 63 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = N )
65 64 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r N ) )
66 54 59 65 3eqtr4d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
67 66 a1d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) )
68 67 3exp 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( M = 0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
69 44 68 jaoi 
 |-  ( ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) -> ( M = 0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
70 7 69 sylbi 
 |-  ( N e. NN -> ( M = 0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
71 70 com12 
 |-  ( M = 0 -> ( N e. NN -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
72 6 71 jaoi 
 |-  ( ( M e. NN \/ M = 0 ) -> ( N e. NN -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
73 2 72 sylbi 
 |-  ( M e. NN0 -> ( N e. NN -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
74 73 com12 
 |-  ( N e. NN -> ( M e. NN0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
75 74 3impd 
 |-  ( N e. NN -> ( ( M e. NN0 /\ R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) )
76 elnn1uz2 
 |-  ( M e. NN <-> ( M = 1 \/ M e. ( ZZ>= ` 2 ) ) )
77 coires1 
 |-  ( `' R o. ( _I |` ( dom `' R u. ran `' R ) ) ) = ( `' R |` ( dom `' R u. ran `' R ) )
78 relcnv 
 |-  Rel `' R
79 ssun1 
 |-  dom `' R C_ ( dom `' R u. ran `' R )
80 78 79 pm3.2i 
 |-  ( Rel `' R /\ dom `' R C_ ( dom `' R u. ran `' R ) )
81 relssres 
 |-  ( ( Rel `' R /\ dom `' R C_ ( dom `' R u. ran `' R ) ) -> ( `' R |` ( dom `' R u. ran `' R ) ) = `' R )
82 80 81 mp1i 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R |` ( dom `' R u. ran `' R ) ) = `' R )
83 77 82 eqtrid 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R o. ( _I |` ( dom `' R u. ran `' R ) ) ) = `' R )
84 cnvco 
 |-  `' ( ( R ^r N ) o. ( R ^r M ) ) = ( `' ( R ^r M ) o. `' ( R ^r N ) )
85 simplr 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> M = 1 )
86 1nn0 
 |-  1 e. NN0
87 85 86 eqeltrdi 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> M e. NN0 )
88 simprl 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> R e. V )
89 relexpcnv 
 |-  ( ( M e. NN0 /\ R e. V ) -> `' ( R ^r M ) = ( `' R ^r M ) )
90 87 88 89 syl2anc 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( R ^r M ) = ( `' R ^r M ) )
91 85 oveq2d 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R ^r M ) = ( `' R ^r 1 ) )
92 cnvexg 
 |-  ( R e. V -> `' R e. _V )
93 88 92 syl 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' R e. _V )
94 relexp1g 
 |-  ( `' R e. _V -> ( `' R ^r 1 ) = `' R )
95 93 94 syl 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R ^r 1 ) = `' R )
96 90 91 95 3eqtrd 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( R ^r M ) = `' R )
97 simpll 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> N = 0 )
98 0nn0 
 |-  0 e. NN0
99 97 98 eqeltrdi 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> N e. NN0 )
100 relexpcnv 
 |-  ( ( N e. NN0 /\ R e. V ) -> `' ( R ^r N ) = ( `' R ^r N ) )
101 99 88 100 syl2anc 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( R ^r N ) = ( `' R ^r N ) )
102 97 oveq2d 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R ^r N ) = ( `' R ^r 0 ) )
103 relexp0g 
 |-  ( `' R e. _V -> ( `' R ^r 0 ) = ( _I |` ( dom `' R u. ran `' R ) ) )
104 93 103 syl 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R ^r 0 ) = ( _I |` ( dom `' R u. ran `' R ) ) )
105 101 102 104 3eqtrd 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( R ^r N ) = ( _I |` ( dom `' R u. ran `' R ) ) )
106 96 105 coeq12d 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' ( R ^r M ) o. `' ( R ^r N ) ) = ( `' R o. ( _I |` ( dom `' R u. ran `' R ) ) ) )
107 84 106 eqtrid 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( ( R ^r N ) o. ( R ^r M ) ) = ( `' R o. ( _I |` ( dom `' R u. ran `' R ) ) ) )
108 99 87 nn0addcld 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) e. NN0 )
109 relexpcnv 
 |-  ( ( ( N + M ) e. NN0 /\ R e. V ) -> `' ( R ^r ( N + M ) ) = ( `' R ^r ( N + M ) ) )
110 108 88 109 syl2anc 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( R ^r ( N + M ) ) = ( `' R ^r ( N + M ) ) )
111 97 85 oveq12d 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) = ( 0 + 1 ) )
112 0p1e1 
 |-  ( 0 + 1 ) = 1
113 111 112 eqtrdi 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) = 1 )
114 113 oveq2d 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R ^r ( N + M ) ) = ( `' R ^r 1 ) )
115 110 114 95 3eqtrd 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( R ^r ( N + M ) ) = `' R )
116 83 107 115 3eqtr4d 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( ( R ^r N ) o. ( R ^r M ) ) = `' ( R ^r ( N + M ) ) )
117 relco 
 |-  Rel ( ( R ^r N ) o. ( R ^r M ) )
118 simprr 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( N + M ) = 1 -> Rel R ) )
119 113 118 mpd 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> Rel R )
120 113 oveq2d 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r ( N + M ) ) = ( R ^r 1 ) )
121 88 18 syl 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r 1 ) = R )
122 120 121 eqtrd 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r ( N + M ) ) = R )
123 122 releqd 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( Rel ( R ^r ( N + M ) ) <-> Rel R ) )
124 119 123 mpbird 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> Rel ( R ^r ( N + M ) ) )
125 cnveqb 
 |-  ( ( Rel ( ( R ^r N ) o. ( R ^r M ) ) /\ Rel ( R ^r ( N + M ) ) ) -> ( ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) <-> `' ( ( R ^r N ) o. ( R ^r M ) ) = `' ( R ^r ( N + M ) ) ) )
126 117 124 125 sylancr 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) <-> `' ( ( R ^r N ) o. ( R ^r M ) ) = `' ( R ^r ( N + M ) ) ) )
127 116 126 mpbird 
 |-  ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
128 127 exp43 
 |-  ( N = 0 -> ( M = 1 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
129 128 com12 
 |-  ( M = 1 -> ( N = 0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
130 coires1 
 |-  ( ( `' R ^r M ) o. ( _I |` ( dom `' R u. ran `' R ) ) ) = ( ( `' R ^r M ) |` ( dom `' R u. ran `' R ) )
131 simp2 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. ( ZZ>= ` 2 ) )
132 simp3 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> R e. V )
133 132 92 syl 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' R e. _V )
134 relexpuzrel 
 |-  ( ( M e. ( ZZ>= ` 2 ) /\ `' R e. _V ) -> Rel ( `' R ^r M ) )
135 131 133 134 syl2anc 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( `' R ^r M ) )
136 eluz2nn 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. NN )
137 131 136 syl 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. NN )
138 relexpnndm 
 |-  ( ( M e. NN /\ `' R e. _V ) -> dom ( `' R ^r M ) C_ dom `' R )
139 137 133 138 syl2anc 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> dom ( `' R ^r M ) C_ dom `' R )
140 139 79 sstrdi 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> dom ( `' R ^r M ) C_ ( dom `' R u. ran `' R ) )
141 relssres 
 |-  ( ( Rel ( `' R ^r M ) /\ dom ( `' R ^r M ) C_ ( dom `' R u. ran `' R ) ) -> ( ( `' R ^r M ) |` ( dom `' R u. ran `' R ) ) = ( `' R ^r M ) )
142 135 140 141 syl2anc 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) |` ( dom `' R u. ran `' R ) ) = ( `' R ^r M ) )
143 130 142 eqtrid 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) o. ( _I |` ( dom `' R u. ran `' R ) ) ) = ( `' R ^r M ) )
144 simp1 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> N = 0 )
145 144 oveq2d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( `' R ^r N ) = ( `' R ^r 0 ) )
146 133 103 syl 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( `' R ^r 0 ) = ( _I |` ( dom `' R u. ran `' R ) ) )
147 145 146 eqtrd 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( `' R ^r N ) = ( _I |` ( dom `' R u. ran `' R ) ) )
148 147 coeq2d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) o. ( `' R ^r N ) ) = ( ( `' R ^r M ) o. ( _I |` ( dom `' R u. ran `' R ) ) ) )
149 144 oveq1d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = ( 0 + M ) )
150 eluzelcn 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. CC )
151 131 150 syl 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. CC )
152 151 addlidd 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( 0 + M ) = M )
153 149 152 eqtrd 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = M )
154 153 oveq2d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( `' R ^r ( N + M ) ) = ( `' R ^r M ) )
155 143 148 154 3eqtr4d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) o. ( `' R ^r N ) ) = ( `' R ^r ( N + M ) ) )
156 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
157 131 136 156 3syl 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. NN0 )
158 157 132 89 syl2anc 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( R ^r M ) = ( `' R ^r M ) )
159 144 98 eqeltrdi 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> N e. NN0 )
160 159 132 100 syl2anc 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( R ^r N ) = ( `' R ^r N ) )
161 158 160 coeq12d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( `' ( R ^r M ) o. `' ( R ^r N ) ) = ( ( `' R ^r M ) o. ( `' R ^r N ) ) )
162 84 161 eqtrid 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( ( R ^r N ) o. ( R ^r M ) ) = ( ( `' R ^r M ) o. ( `' R ^r N ) ) )
163 159 157 nn0addcld 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) e. NN0 )
164 163 132 109 syl2anc 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( R ^r ( N + M ) ) = ( `' R ^r ( N + M ) ) )
165 155 162 164 3eqtr4d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( ( R ^r N ) o. ( R ^r M ) ) = `' ( R ^r ( N + M ) ) )
166 159 nn0cnd 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> N e. CC )
167 151 166 addcomd 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( M + N ) = ( N + M ) )
168 uzaddcl 
 |-  ( ( M e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( M + N ) e. ( ZZ>= ` 2 ) )
169 131 159 168 syl2anc 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( M + N ) e. ( ZZ>= ` 2 ) )
170 167 169 eqeltrrd 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) e. ( ZZ>= ` 2 ) )
171 relexpuzrel 
 |-  ( ( ( N + M ) e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r ( N + M ) ) )
172 170 132 171 syl2anc 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r ( N + M ) ) )
173 117 172 125 sylancr 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) <-> `' ( ( R ^r N ) o. ( R ^r M ) ) = `' ( R ^r ( N + M ) ) ) )
174 165 173 mpbird 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
175 174 a1d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) )
176 175 3exp 
 |-  ( N = 0 -> ( M e. ( ZZ>= ` 2 ) -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
177 176 com12 
 |-  ( M e. ( ZZ>= ` 2 ) -> ( N = 0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
178 129 177 jaoi 
 |-  ( ( M = 1 \/ M e. ( ZZ>= ` 2 ) ) -> ( N = 0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
179 76 178 sylbi 
 |-  ( M e. NN -> ( N = 0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
180 coires1 
 |-  ( ( R ^r 0 ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( R ^r 0 ) |` ( dom R u. ran R ) )
181 simp3 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> R e. V )
182 relexp0rel 
 |-  ( R e. V -> Rel ( R ^r 0 ) )
183 181 182 syl 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> Rel ( R ^r 0 ) )
184 181 33 syl 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
185 184 dmeqd 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> dom ( R ^r 0 ) = dom ( _I |` ( dom R u. ran R ) ) )
186 dmresi 
 |-  dom ( _I |` ( dom R u. ran R ) ) = ( dom R u. ran R )
187 185 186 eqtrdi 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> dom ( R ^r 0 ) = ( dom R u. ran R ) )
188 eqimss 
 |-  ( dom ( R ^r 0 ) = ( dom R u. ran R ) -> dom ( R ^r 0 ) C_ ( dom R u. ran R ) )
189 187 188 syl 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> dom ( R ^r 0 ) C_ ( dom R u. ran R ) )
190 relssres 
 |-  ( ( Rel ( R ^r 0 ) /\ dom ( R ^r 0 ) C_ ( dom R u. ran R ) ) -> ( ( R ^r 0 ) |` ( dom R u. ran R ) ) = ( R ^r 0 ) )
191 183 189 190 syl2anc 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r 0 ) |` ( dom R u. ran R ) ) = ( R ^r 0 ) )
192 180 191 eqtrid 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r 0 ) o. ( _I |` ( dom R u. ran R ) ) ) = ( R ^r 0 ) )
193 simp1 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> N = 0 )
194 193 oveq2d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
195 simp2 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> M = 0 )
196 195 oveq2d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
197 196 184 eqtrd 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
198 194 197 coeq12d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( ( R ^r 0 ) o. ( _I |` ( dom R u. ran R ) ) ) )
199 193 195 oveq12d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = ( 0 + 0 ) )
200 00id 
 |-  ( 0 + 0 ) = 0
201 199 200 eqtrdi 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = 0 )
202 201 oveq2d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 0 ) )
203 192 198 202 3eqtr4d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
204 203 a1d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) )
205 204 3exp 
 |-  ( N = 0 -> ( M = 0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
206 205 com12 
 |-  ( M = 0 -> ( N = 0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
207 179 206 jaoi 
 |-  ( ( M e. NN \/ M = 0 ) -> ( N = 0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
208 2 207 sylbi 
 |-  ( M e. NN0 -> ( N = 0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
209 208 com12 
 |-  ( N = 0 -> ( M e. NN0 -> ( R e. V -> ( ( ( N + M ) = 1 -> Rel R ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) ) ) )
210 209 3impd 
 |-  ( N = 0 -> ( ( M e. NN0 /\ R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) )
211 75 210 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( ( M e. NN0 /\ R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) )
212 1 211 sylbi 
 |-  ( N e. NN0 -> ( ( M e. NN0 /\ R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) )
213 212 imp 
 |-  ( ( N e. NN0 /\ ( M e. NN0 /\ R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )