Metamath Proof Explorer

Theorem relexpaddss

Description: The composition of two powers of a relation is a subset of the relation raised to the sum of those exponents. This is equality where R is a relation as shown by relexpaddd or when the sum of the powers isn't 1 as shown by relexpaddg . (Contributed by RP, 3-Jun-2020)

Ref Expression
Assertion relexpaddss 
|- ( ( N e. NN0 /\ M e. NN0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
2 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
3 2 biimpi 
 |-  ( N e. NN0 -> ( N e. NN \/ N = 0 ) )
4 relexpaddnn 
 |-  ( ( N e. NN /\ M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
5 eqimss 
 |-  ( ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
6 4 5 syl 
 |-  ( ( N e. NN /\ M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
7 6 3exp 
 |-  ( N e. NN -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
8 elnn1uz2 
 |-  ( M e. NN <-> ( M = 1 \/ M e. ( ZZ>= ` 2 ) ) )
9 relco 
 |-  Rel ( ( _I |` ( dom R u. ran R ) ) o. R )
10 dfrel2 
 |-  ( Rel ( ( _I |` ( dom R u. ran R ) ) o. R ) <-> `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( ( _I |` ( dom R u. ran R ) ) o. R ) )
11 10 biimpi 
 |-  ( Rel ( ( _I |` ( dom R u. ran R ) ) o. R ) -> `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( ( _I |` ( dom R u. ran R ) ) o. R ) )
12 9 11 ax-mp 
 |-  `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( ( _I |` ( dom R u. ran R ) ) o. R )
13 cnvco 
 |-  `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( `' R o. `' ( _I |` ( dom R u. ran R ) ) )
14 cnvresid 
 |-  `' ( _I |` ( dom R u. ran R ) ) = ( _I |` ( dom R u. ran R ) )
15 14 coeq2i 
 |-  ( `' R o. `' ( _I |` ( dom R u. ran R ) ) ) = ( `' R o. ( _I |` ( dom R u. ran R ) ) )
16 coires1 
 |-  ( `' R o. ( _I |` ( dom R u. ran R ) ) ) = ( `' R |` ( dom R u. ran R ) )
17 13 15 16 3eqtri 
 |-  `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( `' R |` ( dom R u. ran R ) )
18 eqimss 
 |-  ( `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( `' R |` ( dom R u. ran R ) ) -> `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ ( `' R |` ( dom R u. ran R ) ) )
19 17 18 ax-mp 
 |-  `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ ( `' R |` ( dom R u. ran R ) )
20 cnvss 
 |-  ( `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ ( `' R |` ( dom R u. ran R ) ) -> `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' ( `' R |` ( dom R u. ran R ) ) )
21 19 20 ax-mp 
 |-  `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' ( `' R |` ( dom R u. ran R ) )
22 resss 
 |-  ( `' R |` ( dom R u. ran R ) ) C_ `' R
23 cnvss 
 |-  ( ( `' R |` ( dom R u. ran R ) ) C_ `' R -> `' ( `' R |` ( dom R u. ran R ) ) C_ `' `' R )
24 22 23 ax-mp 
 |-  `' ( `' R |` ( dom R u. ran R ) ) C_ `' `' R
25 21 24 sstri 
 |-  `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' `' R
26 12 25 eqsstrri 
 |-  ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' `' R
27 cnvcnvss 
 |-  `' `' R C_ R
28 26 27 sstri 
 |-  ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ R
29 28 a1i 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ R )
30 simp1 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> N = 0 )
31 30 oveq2d 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
32 relexp0g 
 |-  ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
33 32 3ad2ant3 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
34 31 33 eqtrd 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
35 simp2 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> M = 1 )
36 35 oveq2d 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r M ) = ( R ^r 1 ) )
37 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
38 37 3ad2ant3 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r 1 ) = R )
39 36 38 eqtrd 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r M ) = R )
40 34 39 coeq12d 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( ( _I |` ( dom R u. ran R ) ) o. R ) )
41 30 35 oveq12d 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( N + M ) = ( 0 + 1 ) )
42 1cnd 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> 1 e. CC )
43 42 addlidd 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( 0 + 1 ) = 1 )
44 41 43 eqtrd 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( N + M ) = 1 )
45 44 oveq2d 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 1 ) )
46 45 38 eqtrd 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r ( N + M ) ) = R )
47 29 40 46 3sstr4d 
 |-  ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
48 47 3exp 
 |-  ( N = 0 -> ( M = 1 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
49 coires1 
 |-  ( ( `' R ^r M ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( `' R ^r M ) |` ( dom R u. ran R ) )
50 simp2 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. ( ZZ>= ` 2 ) )
51 cnvexg 
 |-  ( R e. V -> `' R e. _V )
52 51 3ad2ant3 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' R e. _V )
53 relexpuzrel 
 |-  ( ( M e. ( ZZ>= ` 2 ) /\ `' R e. _V ) -> Rel ( `' R ^r M ) )
54 50 52 53 syl2anc 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( `' R ^r M ) )
55 eluz2nn 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. NN )
56 50 55 syl 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. NN )
57 relexpnndm 
 |-  ( ( M e. NN /\ `' R e. _V ) -> dom ( `' R ^r M ) C_ dom `' R )
58 56 52 57 syl2anc 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> dom ( `' R ^r M ) C_ dom `' R )
59 df-rn 
 |-  ran R = dom `' R
60 ssun2 
 |-  ran R C_ ( dom R u. ran R )
61 59 60 eqsstrri 
 |-  dom `' R C_ ( dom R u. ran R )
62 58 61 sstrdi 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> dom ( `' R ^r M ) C_ ( dom R u. ran R ) )
63 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 ) )
64 54 62 63 syl2anc 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) |` ( dom R u. ran R ) ) = ( `' R ^r M ) )
65 49 64 eqtrid 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) o. ( _I |` ( dom R u. ran R ) ) ) = ( `' R ^r M ) )
66 cnvco 
 |-  `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( `' ( R ^r M ) o. `' ( _I |` ( dom R u. ran R ) ) )
67 simp3 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> R e. V )
68 eluzge2nn0 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. NN0 )
69 50 68 syl 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. NN0 )
70 67 69 relexpcnvd 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( R ^r M ) = ( `' R ^r M ) )
71 14 a1i 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( _I |` ( dom R u. ran R ) ) = ( _I |` ( dom R u. ran R ) ) )
72 70 71 coeq12d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( `' ( R ^r M ) o. `' ( _I |` ( dom R u. ran R ) ) ) = ( ( `' R ^r M ) o. ( _I |` ( dom R u. ran R ) ) ) )
73 66 72 eqtrid 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( ( `' R ^r M ) o. ( _I |` ( dom R u. ran R ) ) ) )
74 65 73 70 3eqtr4d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = `' ( R ^r M ) )
75 relco 
 |-  Rel ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) )
76 relexpuzrel 
 |-  ( ( M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r M ) )
77 76 3adant1 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r M ) )
78 cnveqb 
 |-  ( ( Rel ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) /\ Rel ( R ^r M ) ) -> ( ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( R ^r M ) <-> `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = `' ( R ^r M ) ) )
79 75 77 78 sylancr 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( R ^r M ) <-> `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = `' ( R ^r M ) ) )
80 74 79 mpbird 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( R ^r M ) )
81 simp1 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> N = 0 )
82 81 oveq2d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
83 32 3ad2ant3 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
84 82 83 eqtrd 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
85 84 coeq1d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) )
86 81 oveq1d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = ( 0 + M ) )
87 eluzelcn 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. CC )
88 50 87 syl 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. CC )
89 88 addlidd 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( 0 + M ) = M )
90 86 89 eqtrd 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = M )
91 90 oveq2d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r M ) )
92 80 85 91 3eqtr4d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
93 92 5 syl 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
94 93 3exp 
 |-  ( N = 0 -> ( M e. ( ZZ>= ` 2 ) -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
95 48 94 jaod 
 |-  ( N = 0 -> ( ( M = 1 \/ M e. ( ZZ>= ` 2 ) ) -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
96 8 95 biimtrid 
 |-  ( N = 0 -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
97 7 96 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
98 3 97 syl 
 |-  ( N e. NN0 -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
99 elnn1uz2 
 |-  ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
100 99 biimpi 
 |-  ( N e. NN -> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
101 coires1 
 |-  ( R o. ( _I |` ( dom R u. ran R ) ) ) = ( R |` ( dom R u. ran R ) )
102 resss 
 |-  ( R |` ( dom R u. ran R ) ) C_ R
103 101 102 eqsstri 
 |-  ( R o. ( _I |` ( dom R u. ran R ) ) ) C_ R
104 103 a1i 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R o. ( _I |` ( dom R u. ran R ) ) ) C_ R )
105 simp1 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> N = 1 )
106 105 oveq2d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 1 ) )
107 37 3ad2ant3 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r 1 ) = R )
108 106 107 eqtrd 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = R )
109 simp2 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> M = 0 )
110 109 oveq2d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
111 32 3ad2ant3 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
112 110 111 eqtrd 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
113 108 112 coeq12d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R o. ( _I |` ( dom R u. ran R ) ) ) )
114 105 109 oveq12d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( N + M ) = ( 1 + 0 ) )
115 1cnd 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> 1 e. CC )
116 115 addridd 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( 1 + 0 ) = 1 )
117 114 116 eqtrd 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( N + M ) = 1 )
118 117 oveq2d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 1 ) )
119 118 107 eqtrd 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = R )
120 104 113 119 3sstr4d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
121 120 3exp 
 |-  ( N = 1 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
122 coires1 
 |-  ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( R ^r N ) |` ( dom R u. ran R ) )
123 relexpuzrel 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r N ) )
124 123 3adant2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> Rel ( R ^r N ) )
125 simp1 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. ( ZZ>= ` 2 ) )
126 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
127 125 126 syl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. NN )
128 simp3 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> R e. V )
129 relexpnndm 
 |-  ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
130 127 128 129 syl2anc 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
131 ssun1 
 |-  dom R C_ ( dom R u. ran R )
132 130 131 sstrdi 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
133 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 ) )
134 124 132 133 syl2anc 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) |` ( dom R u. ran R ) ) = ( R ^r N ) )
135 122 134 eqtrid 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( R ^r N ) )
136 simp2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> M = 0 )
137 136 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
138 32 3ad2ant3 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
139 137 138 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
140 139 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 ) ) ) )
141 136 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = ( N + 0 ) )
142 eluzelcn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. CC )
143 125 142 syl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. CC )
144 143 addridd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + 0 ) = N )
145 141 144 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = N )
146 145 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r N ) )
147 135 140 146 3eqtr4d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
148 147 5 syl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
149 148 3exp 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
150 121 149 jaoi 
 |-  ( ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
151 100 150 syl 
 |-  ( N e. NN -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
152 coires1 
 |-  ( ( _I |` ( dom R u. ran R ) ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( _I |` ( dom R u. ran R ) ) |` ( dom R u. ran R ) )
153 resres 
 |-  ( ( _I |` ( dom R u. ran R ) ) |` ( dom R u. ran R ) ) = ( _I |` ( ( dom R u. ran R ) i^i ( dom R u. ran R ) ) )
154 inidm 
 |-  ( ( dom R u. ran R ) i^i ( dom R u. ran R ) ) = ( dom R u. ran R )
155 154 reseq2i 
 |-  ( _I |` ( ( dom R u. ran R ) i^i ( dom R u. ran R ) ) ) = ( _I |` ( dom R u. ran R ) )
156 152 153 155 3eqtri 
 |-  ( ( _I |` ( dom R u. ran R ) ) o. ( _I |` ( dom R u. ran R ) ) ) = ( _I |` ( dom R u. ran R ) )
157 simp1 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> N = 0 )
158 157 oveq2d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
159 32 3ad2ant3 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
160 158 159 eqtrd 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
161 simp2 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> M = 0 )
162 161 oveq2d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
163 162 159 eqtrd 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
164 160 163 coeq12d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( ( _I |` ( dom R u. ran R ) ) o. ( _I |` ( dom R u. ran R ) ) ) )
165 157 161 oveq12d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = ( 0 + 0 ) )
166 00id 
 |-  ( 0 + 0 ) = 0
167 166 a1i 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( 0 + 0 ) = 0 )
168 165 167 eqtrd 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = 0 )
169 168 oveq2d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 0 ) )
170 169 159 eqtrd 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( _I |` ( dom R u. ran R ) ) )
171 156 164 170 3eqtr4a 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
172 171 5 syl 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
173 172 3exp 
 |-  ( N = 0 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
174 151 173 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
175 3 174 syl 
 |-  ( N e. NN0 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
176 98 175 jaod 
 |-  ( N e. NN0 -> ( ( M e. NN \/ M = 0 ) -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
177 1 176 biimtrid 
 |-  ( N e. NN0 -> ( M e. NN0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
178 177 3imp 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )