Theorem relexpaddg 13116

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.)

Assertion

Ref	Expression
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 of Theorem relexpaddg

Step	Hyp	Ref	Expression
1		elnn0 10878	. . 3 |- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2		elnn0 10878	. . . . . . 7 |- ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
3		relexpaddnn 13114	. . . . . . . . . . 11 |- ( ( N e. NN /\ M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
4	3	a1d 26	. . . . . . . . . 10 |- ( ( 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 1204	. . . . . . . . 9 |- ( 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 32	. . . . . . . 8 |- ( 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 11242	. . . . . . . . . 10 |- ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
8		coires1 5372	. . . . . . . . . . . . . 14 |- ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( R ^r N ) |` ( dom R u. ran R ) )
9		simpll 758	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> N = 1 )
10		simplr 760	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> M = 0 )
11	9, 10	oveq12d 6323	. . . . . . . . . . . . . . . . . 18 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) = ( 1 + 0 ) )
12		1p0e1 10729	. . . . . . . . . . . . . . . . . 18 |- ( 1 + 0 ) = 1
13	11, 12	syl6eq 2479	. . . . . . . . . . . . . . . . 17 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) = 1 )
14		simprr 764	. . . . . . . . . . . . . . . . 17 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( N + M ) = 1 -> Rel R ) )
15	13, 14	mpd 15	. . . . . . . . . . . . . . . 16 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> Rel R )
16	9	oveq2d 6321	. . . . . . . . . . . . . . . . . 18 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r N ) = ( R ^r 1 ) )
17		simprl 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> R e. V )
18		relexp1g 13089	. . . . . . . . . . . . . . . . . . 19 |- ( R e. V -> ( R ^r 1 ) = R )
19	17, 18	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r 1 ) = R )
20	16, 19	eqtrd 2463	. . . . . . . . . . . . . . . . 17 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r N ) = R )
21	20	releqd 4938	. . . . . . . . . . . . . . . 16 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( Rel ( R ^r N ) <-> Rel R ) )
22	15, 21	mpbird 235	. . . . . . . . . . . . . . 15 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> Rel ( R ^r N ) )
23		1nn 10627	. . . . . . . . . . . . . . . . . 18 |- 1 e. NN
24	9, 23	syl6eqel 2515	. . . . . . . . . . . . . . . . 17 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> N e. NN )
25		relexpnndm 13104	. . . . . . . . . . . . . . . . 17 |- ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
26	24, 17, 25	syl2anc 665	. . . . . . . . . . . . . . . 16 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> dom ( R ^r N ) C_ dom R )
27		ssun1 3629	. . . . . . . . . . . . . . . 16 |- dom R C_ ( dom R u. ran R )
28	26, 27	syl6ss 3476	. . . . . . . . . . . . . . 15 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
29		relssres 5161	. . . . . . . . . . . . . . 15 |- ( ( 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 665	. . . . . . . . . . . . . 14 |- ( ( ( 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	syl5eq 2475	. . . . . . . . . . . . 13 |- ( ( ( 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 6321	. . . . . . . . . . . . . . 15 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r M ) = ( R ^r 0 ) )
33		relexp0g 13085	. . . . . . . . . . . . . . . 16 |- ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
34	17, 33	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( 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 2463	. . . . . . . . . . . . . 14 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
36	35	coeq2d 5016	. . . . . . . . . . . . 13 |- ( ( ( 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 6321	. . . . . . . . . . . . . . 15 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) = ( N + 0 ) )
38		ax-1cn 9604	. . . . . . . . . . . . . . . . 17 |- 1 e. CC
39	9, 38	syl6eqel 2515	. . . . . . . . . . . . . . . 16 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> N e. CC )
40	39	addid1d 9840	. . . . . . . . . . . . . . 15 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + 0 ) = N )
41	37, 40	eqtrd 2463	. . . . . . . . . . . . . 14 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) = N )
42	41	oveq2d 6321	. . . . . . . . . . . . 13 |- ( ( ( N = 1 /\ M = 0 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r ( N + M ) ) = ( R ^r N ) )
43	31, 36, 42	3eqtr4d 2473	. . . . . . . . . . . 12 |- ( ( ( 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 615	. . . . . . . . . . 11 |- ( 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 1005	. . . . . . . . . . . . . . . . 17 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. ( ZZ>= ` 2 ) )
46		simp3 1007	. . . . . . . . . . . . . . . . 17 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> R e. V )
47		relexpuzrel 13115	. . . . . . . . . . . . . . . . 17 |- ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r N ) )
48	45, 46, 47	syl2anc 665	. . . . . . . . . . . . . . . 16 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> Rel ( R ^r N ) )
49		eluz2nn 11204	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ( ZZ>= ` 2 ) -> N e. NN )
50	45, 49	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. NN )
51	50, 46, 25	syl2anc 665	. . . . . . . . . . . . . . . . 17 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
52	51, 27	syl6ss 3476	. . . . . . . . . . . . . . . 16 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
53	48, 52, 29	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) |` ( dom R u. ran R ) ) = ( R ^r N ) )
54	8, 53	syl5eq 2475	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( R ^r N ) )
55		simp2 1006	. . . . . . . . . . . . . . . . 17 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> M = 0 )
56	55	oveq2d 6321	. . . . . . . . . . . . . . . 16 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
57	46, 33	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
58	56, 57	eqtrd 2463	. . . . . . . . . . . . . . 15 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
59	58	coeq2d 5016	. . . . . . . . . . . . . 14 |- ( ( 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 6321	. . . . . . . . . . . . . . . 16 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = ( N + 0 ) )
61		eluzelcn 11177	. . . . . . . . . . . . . . . . . 18 |- ( N e. ( ZZ>= ` 2 ) -> N e. CC )
62	45, 61	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. CC )
63	62	addid1d 9840	. . . . . . . . . . . . . . . 16 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + 0 ) = N )
64	60, 63	eqtrd 2463	. . . . . . . . . . . . . . 15 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = N )
65	64	oveq2d 6321	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r N ) )
66	54, 59, 65	3eqtr4d 2473	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
67	66	a1d 26	. . . . . . . . . . . 12 |- ( ( 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 1204	. . . . . . . . . . 11 |- ( 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 380	. . . . . . . . . 10 |- ( ( 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 198	. . . . . . . . 9 |- ( 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 32	. . . . . . . 8 |- ( 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 380	. . . . . . 7 |- ( ( 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 198	. . . . . 6 |- ( 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 32	. . . . 5 |- ( 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 1219	. . . 4 |- ( 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 11242	. . . . . . . . 9 |- ( M e. NN <-> ( M = 1 \/ M e. ( ZZ>= ` 2 ) ) )
77		coires1 5372	. . . . . . . . . . . . . . 15 |- ( `' R o. ( _I |` ( dom `' R u. ran `' R ) ) ) = ( `' R |` ( dom `' R u. ran `' R ) )
78		relcnv 5226	. . . . . . . . . . . . . . . . 17 |- Rel `' R
79		ssun1 3629	. . . . . . . . . . . . . . . . 17 |- dom `' R C_ ( dom `' R u. ran `' R )
80	78, 79	pm3.2i 456	. . . . . . . . . . . . . . . 16 |- ( Rel `' R /\ dom `' R C_ ( dom `' R u. ran `' R ) )
81		relssres 5161	. . . . . . . . . . . . . . . 16 |- ( ( Rel `' R /\ dom `' R C_ ( dom `' R u. ran `' R ) ) -> ( `' R |` ( dom `' R u. ran `' R ) ) = `' R )
82	80, 81	mp1i 13	. . . . . . . . . . . . . . 15 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R |` ( dom `' R u. ran `' R ) ) = `' R )
83	77, 82	syl5eq 2475	. . . . . . . . . . . . . 14 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R o. ( _I |` ( dom `' R u. ran `' R ) ) ) = `' R )
84		cnvco 5039	. . . . . . . . . . . . . . 15 |- `' ( ( R ^r N ) o. ( R ^r M ) ) = ( `' ( R ^r M ) o. `' ( R ^r N ) )
85		simplr 760	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> M = 1 )
86		1nn0 10892	. . . . . . . . . . . . . . . . . . 19 |- 1 e. NN0
87	85, 86	syl6eqel 2515	. . . . . . . . . . . . . . . . . 18 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> M e. NN0 )
88		simprl 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> R e. V )
89		relexpcnv 13098	. . . . . . . . . . . . . . . . . 18 |- ( ( M e. NN0 /\ R e. V ) -> `' ( R ^r M ) = ( `' R ^r M ) )
90	87, 88, 89	syl2anc 665	. . . . . . . . . . . . . . . . 17 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( R ^r M ) = ( `' R ^r M ) )
91	85	oveq2d 6321	. . . . . . . . . . . . . . . . 17 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R ^r M ) = ( `' R ^r 1 ) )
92		cnvexg 6753	. . . . . . . . . . . . . . . . . . 19 |- ( R e. V -> `' R e. _V )
93	88, 92	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' R e. _V )
94		relexp1g 13089	. . . . . . . . . . . . . . . . . 18 |- ( `' R e. _V -> ( `' R ^r 1 ) = `' R )
95	93, 94	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R ^r 1 ) = `' R )
96	90, 91, 95	3eqtrd 2467	. . . . . . . . . . . . . . . 16 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( R ^r M ) = `' R )
97		simpll 758	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> N = 0 )
98		0nn0 10891	. . . . . . . . . . . . . . . . . . 19 |- 0 e. NN0
99	97, 98	syl6eqel 2515	. . . . . . . . . . . . . . . . . 18 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> N e. NN0 )
100		relexpcnv 13098	. . . . . . . . . . . . . . . . . 18 |- ( ( N e. NN0 /\ R e. V ) -> `' ( R ^r N ) = ( `' R ^r N ) )
101	99, 88, 100	syl2anc 665	. . . . . . . . . . . . . . . . 17 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( R ^r N ) = ( `' R ^r N ) )
102	97	oveq2d 6321	. . . . . . . . . . . . . . . . 17 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R ^r N ) = ( `' R ^r 0 ) )
103		relexp0g 13085	. . . . . . . . . . . . . . . . . 18 |- ( `' R e. _V -> ( `' R ^r 0 ) = ( _I |` ( dom `' R u. ran `' R ) ) )
104	93, 103	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 2467	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 5018	. . . . . . . . . . . . . . 15 |- ( ( ( 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	syl5eq 2475	. . . . . . . . . . . . . 14 |- ( ( ( 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 10936	. . . . . . . . . . . . . . . 16 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) e. NN0 )
109		relexpcnv 13098	. . . . . . . . . . . . . . . 16 |- ( ( ( N + M ) e. NN0 /\ R e. V ) -> `' ( R ^r ( N + M ) ) = ( `' R ^r ( N + M ) ) )
110	108, 88, 109	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( R ^r ( N + M ) ) = ( `' R ^r ( N + M ) ) )
111	97, 85	oveq12d 6323	. . . . . . . . . . . . . . . . 17 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) = ( 0 + 1 ) )
112		0p1e1 10728	. . . . . . . . . . . . . . . . 17 |- ( 0 + 1 ) = 1
113	111, 112	syl6eq 2479	. . . . . . . . . . . . . . . 16 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( N + M ) = 1 )
114	113	oveq2d 6321	. . . . . . . . . . . . . . 15 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( `' R ^r ( N + M ) ) = ( `' R ^r 1 ) )
115	110, 114, 95	3eqtrd 2467	. . . . . . . . . . . . . 14 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> `' ( R ^r ( N + M ) ) = `' R )
116	83, 107, 115	3eqtr4d 2473	. . . . . . . . . . . . 13 |- ( ( ( 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 5352	. . . . . . . . . . . . . 14 |- Rel ( ( R ^r N ) o. ( R ^r M ) )
118		simprr 764	. . . . . . . . . . . . . . . 16 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( N + M ) = 1 -> Rel R ) )
119	113, 118	mpd 15	. . . . . . . . . . . . . . 15 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> Rel R )
120	113	oveq2d 6321	. . . . . . . . . . . . . . . . 17 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r ( N + M ) ) = ( R ^r 1 ) )
121	88, 18	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r 1 ) = R )
122	120, 121	eqtrd 2463	. . . . . . . . . . . . . . . 16 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( R ^r ( N + M ) ) = R )
123	122	releqd 4938	. . . . . . . . . . . . . . 15 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( Rel ( R ^r ( N + M ) ) <-> Rel R ) )
124	119, 123	mpbird 235	. . . . . . . . . . . . . 14 |- ( ( ( N = 0 /\ M = 1 ) /\ ( R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> Rel ( R ^r ( N + M ) ) )
125		cnveqb 5310	. . . . . . . . . . . . . 14 |- ( ( 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 667	. . . . . . . . . . . . 13 |- ( ( ( 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 235	. . . . . . . . . . . 12 |- ( ( ( 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 615	. . . . . . . . . . 11 |- ( 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 32	. . . . . . . . . 10 |- ( 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 5372	. . . . . . . . . . . . . . . . 17 |- ( ( `' R ^r M ) o. ( _I |` ( dom `' R u. ran `' R ) ) ) = ( ( `' R ^r M ) |` ( dom `' R u. ran `' R ) )
131		simp2 1006	. . . . . . . . . . . . . . . . . . 19 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. ( ZZ>= ` 2 ) )
132		simp3 1007	. . . . . . . . . . . . . . . . . . . 20 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> R e. V )
133	132, 92	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' R e. _V )
134		relexpuzrel 13115	. . . . . . . . . . . . . . . . . . 19 |- ( ( M e. ( ZZ>= ` 2 ) /\ `' R e. _V ) -> Rel ( `' R ^r M ) )
135	131, 133, 134	syl2anc 665	. . . . . . . . . . . . . . . . . 18 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( `' R ^r M ) )
136		eluz2nn 11204	. . . . . . . . . . . . . . . . . . . . 21 |- ( M e. ( ZZ>= ` 2 ) -> M e. NN )
137	131, 136	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. NN )
138		relexpnndm 13104	. . . . . . . . . . . . . . . . . . . 20 |- ( ( M e. NN /\ `' R e. _V ) -> dom ( `' R ^r M ) C_ dom `' R )
139	137, 133, 138	syl2anc 665	. . . . . . . . . . . . . . . . . . 19 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> dom ( `' R ^r M ) C_ dom `' R )
140	139, 79	syl6ss 3476	. . . . . . . . . . . . . . . . . 18 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> dom ( `' R ^r M ) C_ ( dom `' R u. ran `' R ) )
141		relssres 5161	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 665	. . . . . . . . . . . . . . . . 17 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) |` ( dom `' R u. ran `' R ) ) = ( `' R ^r M ) )
143	130, 142	syl5eq 2475	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) o. ( _I |` ( dom `' R u. ran `' R ) ) ) = ( `' R ^r M ) )
144		simp1 1005	. . . . . . . . . . . . . . . . . . 19 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> N = 0 )
145	144	oveq2d 6321	. . . . . . . . . . . . . . . . . 18 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( `' R ^r N ) = ( `' R ^r 0 ) )
146	133, 103	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( `' R ^r 0 ) = ( _I |` ( dom `' R u. ran `' R ) ) )
147	145, 146	eqtrd 2463	. . . . . . . . . . . . . . . . 17 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( `' R ^r N ) = ( _I |` ( dom `' R u. ran `' R ) ) )
148	147	coeq2d 5016	. . . . . . . . . . . . . . . 16 |- ( ( 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 6320	. . . . . . . . . . . . . . . . . 18 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = ( 0 + M ) )
150		eluzelcn 11177	. . . . . . . . . . . . . . . . . . . 20 |- ( M e. ( ZZ>= ` 2 ) -> M e. CC )
151	131, 150	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. CC )
152	151	addid2d 9841	. . . . . . . . . . . . . . . . . 18 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( 0 + M ) = M )
153	149, 152	eqtrd 2463	. . . . . . . . . . . . . . . . 17 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = M )
154	153	oveq2d 6321	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( `' R ^r ( N + M ) ) = ( `' R ^r M ) )
155	143, 148, 154	3eqtr4d 2473	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) o. ( `' R ^r N ) ) = ( `' R ^r ( N + M ) ) )
156		nnnn0 10883	. . . . . . . . . . . . . . . . . . 19 |- ( M e. NN -> M e. NN0 )
157	131, 136, 156	3syl 18	. . . . . . . . . . . . . . . . . 18 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. NN0 )
158	157, 132, 89	syl2anc 665	. . . . . . . . . . . . . . . . 17 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( R ^r M ) = ( `' R ^r M ) )
159	144, 98	syl6eqel 2515	. . . . . . . . . . . . . . . . . 18 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> N e. NN0 )
160	159, 132, 100	syl2anc 665	. . . . . . . . . . . . . . . . 17 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( R ^r N ) = ( `' R ^r N ) )
161	158, 160	coeq12d 5018	. . . . . . . . . . . . . . . 16 |- ( ( 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	syl5eq 2475	. . . . . . . . . . . . . . 15 |- ( ( 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 10936	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) e. NN0 )
164	163, 132, 109	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( R ^r ( N + M ) ) = ( `' R ^r ( N + M ) ) )
165	155, 162, 164	3eqtr4d 2473	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( ( R ^r N ) o. ( R ^r M ) ) = `' ( R ^r ( N + M ) ) )
166	159	nn0cnd 10934	. . . . . . . . . . . . . . . . . 18 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> N e. CC )
167	151, 166	addcomd 9842	. . . . . . . . . . . . . . . . 17 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( M + N ) = ( N + M ) )
168		uzaddcl 11222	. . . . . . . . . . . . . . . . . 18 |- ( ( M e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( M + N ) e. ( ZZ>= ` 2 ) )
169	131, 159, 168	syl2anc 665	. . . . . . . . . . . . . . . . 17 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( M + N ) e. ( ZZ>= ` 2 ) )
170	167, 169	eqeltrrd 2508	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) e. ( ZZ>= ` 2 ) )
171		relexpuzrel 13115	. . . . . . . . . . . . . . . 16 |- ( ( ( N + M ) e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r ( N + M ) ) )
172	170, 132, 171	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r ( N + M ) ) )
173	117, 172, 125	sylancr 667	. . . . . . . . . . . . . 14 |- ( ( 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 235	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
175	174	a1d 26	. . . . . . . . . . . 12 |- ( ( 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 1204	. . . . . . . . . . 11 |- ( 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 32	. . . . . . . . . 10 |- ( 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 380	. . . . . . . . 9 |- ( ( 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 198	. . . . . . . 8 |- ( 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 5372	. . . . . . . . . . . . 13 |- ( ( R ^r 0 ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( R ^r 0 ) |` ( dom R u. ran R ) )
181		simp3 1007	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> R e. V )
182		relexp0rel 13100	. . . . . . . . . . . . . . 15 |- ( R e. V -> Rel ( R ^r 0 ) )
183	181, 182	syl 17	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> Rel ( R ^r 0 ) )
184	181, 33	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
185	184	dmeqd 5056	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> dom ( R ^r 0 ) = dom ( _I |` ( dom R u. ran R ) ) )
186		dmresi 5179	. . . . . . . . . . . . . . . 16 |- dom ( _I |` ( dom R u. ran R ) ) = ( dom R u. ran R )
187	185, 186	syl6eq 2479	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> dom ( R ^r 0 ) = ( dom R u. ran R ) )
188		eqimss 3516	. . . . . . . . . . . . . . 15 |- ( dom ( R ^r 0 ) = ( dom R u. ran R ) -> dom ( R ^r 0 ) C_ ( dom R u. ran R ) )
189	187, 188	syl 17	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> dom ( R ^r 0 ) C_ ( dom R u. ran R ) )
190		relssres 5161	. . . . . . . . . . . . . 14 |- ( ( 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 665	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r 0 ) |` ( dom R u. ran R ) ) = ( R ^r 0 ) )
192	180, 191	syl5eq 2475	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r 0 ) o. ( _I |` ( dom R u. ran R ) ) ) = ( R ^r 0 ) )
193		simp1 1005	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> N = 0 )
194	193	oveq2d 6321	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
195		simp2 1006	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> M = 0 )
196	195	oveq2d 6321	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
197	196, 184	eqtrd 2463	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
198	194, 197	coeq12d 5018	. . . . . . . . . . . 12 |- ( ( 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 6323	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = ( 0 + 0 ) )
200		00id 9815	. . . . . . . . . . . . . 14 |- ( 0 + 0 ) = 0
201	199, 200	syl6eq 2479	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = 0 )
202	201	oveq2d 6321	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 0 ) )
203	192, 198, 202	3eqtr4d 2473	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
204	203	a1d 26	. . . . . . . . . 10 |- ( ( 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 1204	. . . . . . . . 9 |- ( 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 32	. . . . . . . 8 |- ( 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 380	. . . . . . 7 |- ( ( 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 198	. . . . . 6 |- ( 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 32	. . . . 5 |- ( 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 1219	. . . 4 |- ( 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 380	. . 3 |- ( ( 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 198	. 2 |- ( 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 430	1 |- ( ( 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 ) ) )

Syntax hints:   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1872   _Vcvv 3080   u. cun 3434   C_ wss 3436   _I cid 4763   `'ccnv 4852   dom cdm 4853   ran crn 4854   |` cres 4855   o. ccom 4857   Rel wrel 4858   ` cfv 5601  (class class class)co 6305   CCcc 9544   0cc0 9546   1c1 9547   + caddc 9549   NNcn 10616   2c2 10666   NN0cn0 10876   ZZ>=cuz 11166   ^r crelexp 13083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-2nd 6808  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-er 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-nn 10617  df-2 10675  df-n0 10877  df-z 10945  df-uz 11167  df-seq 12220  df-relexp 13084

This theorem is referenced by:  relexpaddd  13117  relexpnul  36240