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 addid1d
 |-  ( ( ( 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 addid1d
 |-  ( ( 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 addid2d
 |-  ( ( 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 ) ) )