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 addid2d 
 |-  ( ( 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 syl5eq 
 |-  ( ( 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 eluzge2nn0 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. NN0 )
68 50 67 syl 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. NN0 )
69 simp3 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> R e. V )
70 relexpcnv 
 |-  ( ( M e. NN0 /\ R e. V ) -> `' ( R ^r M ) = ( `' R ^r M ) )
71 68 69 70 syl2anc 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( R ^r M ) = ( `' R ^r M ) )
72 14 a1i 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( _I |` ( dom R u. ran R ) ) = ( _I |` ( dom R u. ran R ) ) )
73 71 72 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 ) ) ) )
74 66 73 syl5eq 
 |-  ( ( 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 ) ) ) )
75 65 74 71 3eqtr4d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = `' ( R ^r M ) )
76 relco 
 |-  Rel ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) )
77 relexpuzrel 
 |-  ( ( M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r M ) )
78 77 3adant1 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r M ) )
79 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 ) ) )
80 76 78 79 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 ) ) )
81 75 80 mpbird 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( R ^r M ) )
82 simp1 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> N = 0 )
83 82 oveq2d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
84 32 3ad2ant3 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
85 83 84 eqtrd 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
86 85 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 ) ) )
87 82 oveq1d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = ( 0 + M ) )
88 eluzelcn 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. CC )
89 50 88 syl 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. CC )
90 89 addid2d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( 0 + M ) = M )
91 87 90 eqtrd 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = M )
92 91 oveq2d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r M ) )
93 81 86 92 3eqtr4d 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
94 93 5 syl 
 |-  ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
95 94 3exp 
 |-  ( N = 0 -> ( M e. ( ZZ>= ` 2 ) -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
96 48 95 jaod 
 |-  ( N = 0 -> ( ( M = 1 \/ M e. ( ZZ>= ` 2 ) ) -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
97 8 96 syl5bi 
 |-  ( N = 0 -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
98 7 97 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
99 3 98 syl 
 |-  ( N e. NN0 -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
100 elnn1uz2 
 |-  ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
101 100 biimpi 
 |-  ( N e. NN -> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
102 coires1 
 |-  ( R o. ( _I |` ( dom R u. ran R ) ) ) = ( R |` ( dom R u. ran R ) )
103 resss 
 |-  ( R |` ( dom R u. ran R ) ) C_ R
104 102 103 eqsstri 
 |-  ( R o. ( _I |` ( dom R u. ran R ) ) ) C_ R
105 104 a1i 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R o. ( _I |` ( dom R u. ran R ) ) ) C_ R )
106 simp1 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> N = 1 )
107 106 oveq2d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 1 ) )
108 37 3ad2ant3 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r 1 ) = R )
109 107 108 eqtrd 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = R )
110 simp2 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> M = 0 )
111 110 oveq2d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
112 32 3ad2ant3 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
113 111 112 eqtrd 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
114 109 113 coeq12d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R o. ( _I |` ( dom R u. ran R ) ) ) )
115 106 110 oveq12d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( N + M ) = ( 1 + 0 ) )
116 1cnd 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> 1 e. CC )
117 116 addid1d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( 1 + 0 ) = 1 )
118 115 117 eqtrd 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( N + M ) = 1 )
119 118 oveq2d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 1 ) )
120 119 108 eqtrd 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = R )
121 105 114 120 3sstr4d 
 |-  ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
122 121 3exp 
 |-  ( N = 1 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
123 coires1 
 |-  ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( R ^r N ) |` ( dom R u. ran R ) )
124 relexpuzrel 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r N ) )
125 124 3adant2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> Rel ( R ^r N ) )
126 simp1 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. ( ZZ>= ` 2 ) )
127 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
128 126 127 syl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. NN )
129 simp3 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> R e. V )
130 relexpnndm 
 |-  ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
131 128 129 130 syl2anc 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
132 ssun1 
 |-  dom R C_ ( dom R u. ran R )
133 131 132 sstrdi 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
134 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 ) )
135 125 133 134 syl2anc 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) |` ( dom R u. ran R ) ) = ( R ^r N ) )
136 123 135 syl5eq 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( R ^r N ) )
137 simp2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> M = 0 )
138 137 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
139 32 3ad2ant3 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
140 138 139 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
141 140 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 ) ) ) )
142 137 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = ( N + 0 ) )
143 eluzelcn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. CC )
144 126 143 syl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. CC )
145 144 addid1d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + 0 ) = N )
146 142 145 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = N )
147 146 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r N ) )
148 136 141 147 3eqtr4d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
149 148 5 syl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
150 149 3exp 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
151 122 150 jaoi 
 |-  ( ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
152 101 151 syl 
 |-  ( N e. NN -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
153 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 ) )
154 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 ) ) )
155 inidm 
 |-  ( ( dom R u. ran R ) i^i ( dom R u. ran R ) ) = ( dom R u. ran R )
156 155 reseq2i 
 |-  ( _I |` ( ( dom R u. ran R ) i^i ( dom R u. ran R ) ) ) = ( _I |` ( dom R u. ran R ) )
157 153 154 156 3eqtri 
 |-  ( ( _I |` ( dom R u. ran R ) ) o. ( _I |` ( dom R u. ran R ) ) ) = ( _I |` ( dom R u. ran R ) )
158 simp1 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> N = 0 )
159 158 oveq2d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
160 32 3ad2ant3 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
161 159 160 eqtrd 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
162 simp2 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> M = 0 )
163 162 oveq2d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
164 163 160 eqtrd 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
165 161 164 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 ) ) ) )
166 158 162 oveq12d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = ( 0 + 0 ) )
167 00id 
 |-  ( 0 + 0 ) = 0
168 167 a1i 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( 0 + 0 ) = 0 )
169 166 168 eqtrd 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = 0 )
170 169 oveq2d 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 0 ) )
171 170 160 eqtrd 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( _I |` ( dom R u. ran R ) ) )
172 157 165 171 3eqtr4a 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
173 172 5 syl 
 |-  ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
174 173 3exp 
 |-  ( N = 0 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
175 152 174 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
176 3 175 syl 
 |-  ( N e. NN0 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
177 99 176 jaod 
 |-  ( N e. NN0 -> ( ( M e. NN \/ M = 0 ) -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
178 1 177 syl5bi 
 |-  ( N e. NN0 -> ( M e. NN0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
179 178 3imp 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )