Theorem relexpaddss 35949

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 13096 or when the sum of the powers isn't 1 as shown by relexpaddg 13095. (Contributed by RP, 3-Jun-2020.)

Assertion

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

Proof of Theorem relexpaddss

Step	Hyp	Ref	Expression
1		elnn0 10871	. . 3 |- ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
2		elnn0 10871	. . . . . 6 |- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
3	2	biimpi 197	. . . . 5 |- ( N e. NN0 -> ( N e. NN \/ N = 0 ) )
4		relexpaddnn 13093	. . . . . . . 8 |- ( ( N e. NN /\ M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
5		eqimss 3522	. . . . . . . 8 |- ( ( ( 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 17	. . . . . . 7 |- ( ( N e. NN /\ M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
7	6	3exp 1204	. . . . . 6 |- ( N e. NN -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
8		elnn1uz2 11235	. . . . . . 7 |- ( M e. NN <-> ( M = 1 \/ M e. ( ZZ>= ` 2 ) ) )
9		relco 5353	. . . . . . . . . . . . . 14 |- Rel ( ( _I |` ( dom R u. ran R ) ) o. R )
10		dfrel2 5306	. . . . . . . . . . . . . . 15 |- ( 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 197	. . . . . . . . . . . . . 14 |- ( 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 5	. . . . . . . . . . . . 13 |- `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( ( _I |` ( dom R u. ran R ) ) o. R )
13		cnvco 5040	. . . . . . . . . . . . . . . . 17 |- `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( `' R o. `' ( _I |` ( dom R u. ran R ) ) )
14		cnvresid 5671	. . . . . . . . . . . . . . . . . 18 |- `' ( _I |` ( dom R u. ran R ) ) = ( _I |` ( dom R u. ran R ) )
15	14	coeq2i 5015	. . . . . . . . . . . . . . . . 17 |- ( `' R o. `' ( _I |` ( dom R u. ran R ) ) ) = ( `' R o. ( _I |` ( dom R u. ran R ) ) )
16		coires1 5373	. . . . . . . . . . . . . . . . 17 |- ( `' R o. ( _I |` ( dom R u. ran R ) ) ) = ( `' R |` ( dom R u. ran R ) )
17	13, 15, 16	3eqtri 2462	. . . . . . . . . . . . . . . 16 |- `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( `' R |` ( dom R u. ran R ) )
18		eqimss 3522	. . . . . . . . . . . . . . . 16 |- ( `' ( ( _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 5	. . . . . . . . . . . . . . 15 |- `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ ( `' R |` ( dom R u. ran R ) )
20		cnvss 5027	. . . . . . . . . . . . . . 15 |- ( `' ( ( _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 5	. . . . . . . . . . . . . 14 |- `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' ( `' R |` ( dom R u. ran R ) )
22		resss 5148	. . . . . . . . . . . . . . 15 |- ( `' R |` ( dom R u. ran R ) ) C_ `' R
23		cnvss 5027	. . . . . . . . . . . . . . 15 |- ( ( `' R |` ( dom R u. ran R ) ) C_ `' R -> `' ( `' R |` ( dom R u. ran R ) ) C_ `' `' R )
24	22, 23	ax-mp 5	. . . . . . . . . . . . . 14 |- `' ( `' R |` ( dom R u. ran R ) ) C_ `' `' R
25	21, 24	sstri 3479	. . . . . . . . . . . . 13 |- `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' `' R
26	12, 25	eqsstr3i 3501	. . . . . . . . . . . 12 |- ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' `' R
27		cnvcnvss 5310	. . . . . . . . . . . 12 |- `' `' R C_ R
28	26, 27	sstri 3479	. . . . . . . . . . 11 |- ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ R
29	28	a1i 11	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ R )
30		simp1 1005	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> N = 0 )
31	30	oveq2d 6321	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
32		relexp0g 13064	. . . . . . . . . . . . 13 |- ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
33	32	3ad2ant3 1028	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
34	31, 33	eqtrd 2470	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
35		simp2 1006	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> M = 1 )
36	35	oveq2d 6321	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r M ) = ( R ^r 1 ) )
37		relexp1g 13068	. . . . . . . . . . . . 13 |- ( R e. V -> ( R ^r 1 ) = R )
38	37	3ad2ant3 1028	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r 1 ) = R )
39	36, 38	eqtrd 2470	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r M ) = R )
40	34, 39	coeq12d 5019	. . . . . . . . . 10 |- ( ( 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 6323	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( N + M ) = ( 0 + 1 ) )
42		1cnd 9658	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> 1 e. CC )
43	42	addid2d 9833	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( 0 + 1 ) = 1 )
44	41, 43	eqtrd 2470	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( N + M ) = 1 )
45	44	oveq2d 6321	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 1 ) )
46	45, 38	eqtrd 2470	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r ( N + M ) ) = R )
47	29, 40, 46	3sstr4d 3513	. . . . . . . . 9 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
48	47	3exp 1204	. . . . . . . 8 |- ( N = 0 -> ( M = 1 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
49		coires1 5373	. . . . . . . . . . . . . 14 |- ( ( `' R ^r M ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( `' R ^r M ) |` ( dom R u. ran R ) )
50		simp2 1006	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. ( ZZ>= ` 2 ) )
51		cnvexg 6753	. . . . . . . . . . . . . . . . 17 |- ( R e. V -> `' R e. _V )
52	51	3ad2ant3 1028	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' R e. _V )
53		relexpuzrel 13094	. . . . . . . . . . . . . . . 16 |- ( ( M e. ( ZZ>= ` 2 ) /\ `' R e. _V ) -> Rel ( `' R ^r M ) )
54	50, 52, 53	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( `' R ^r M ) )
55		eluz2nn 11197	. . . . . . . . . . . . . . . . . 18 |- ( M e. ( ZZ>= ` 2 ) -> M e. NN )
56	50, 55	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. NN )
57		relexpnndm 13083	. . . . . . . . . . . . . . . . 17 |- ( ( M e. NN /\ `' R e. _V ) -> dom ( `' R ^r M ) C_ dom `' R )
58	56, 52, 57	syl2anc 665	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> dom ( `' R ^r M ) C_ dom `' R )
59		df-rn 4865	. . . . . . . . . . . . . . . . 17 |- ran R = dom `' R
60		ssun2 3636	. . . . . . . . . . . . . . . . 17 |- ran R C_ ( dom R u. ran R )
61	59, 60	eqsstr3i 3501	. . . . . . . . . . . . . . . 16 |- dom `' R C_ ( dom R u. ran R )
62	58, 61	syl6ss 3482	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> dom ( `' R ^r M ) C_ ( dom R u. ran R ) )
63		relssres 5162	. . . . . . . . . . . . . . 15 |- ( ( 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 665	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) |` ( dom R u. ran R ) ) = ( `' R ^r M ) )
65	49, 64	syl5eq 2482	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) o. ( _I |` ( dom R u. ran R ) ) ) = ( `' R ^r M ) )
66		cnvco 5040	. . . . . . . . . . . . . 14 |- `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( `' ( R ^r M ) o. `' ( _I |` ( dom R u. ran R ) ) )
67		eluzge2nn0 11198	. . . . . . . . . . . . . . . . 17 |- ( M e. ( ZZ>= ` 2 ) -> M e. NN0 )
68	50, 67	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. NN0 )
69		simp3 1007	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> R e. V )
70		relexpcnv 13077	. . . . . . . . . . . . . . . 16 |- ( ( M e. NN0 /\ R e. V ) -> `' ( R ^r M ) = ( `' R ^r M ) )
71	68, 69, 70	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( R ^r M ) = ( `' R ^r M ) )
72	14	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( 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 5019	. . . . . . . . . . . . . 14 |- ( ( 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 2482	. . . . . . . . . . . . 13 |- ( ( 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 2480	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = `' ( R ^r M ) )
76		relco 5353	. . . . . . . . . . . . 13 |- Rel ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) )
77		relexpuzrel 13094	. . . . . . . . . . . . . 14 |- ( ( M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r M ) )
78	77	3adant1 1023	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r M ) )
79		cnveqb 5311	. . . . . . . . . . . . 13 |- ( ( 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 667	. . . . . . . . . . . 12 |- ( ( 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 235	. . . . . . . . . . 11 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( R ^r M ) )
82		simp1 1005	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> N = 0 )
83	82	oveq2d 6321	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
84	32	3ad2ant3 1028	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
85	83, 84	eqtrd 2470	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
86	85	coeq1d 5016	. . . . . . . . . . 11 |- ( ( 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 6320	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = ( 0 + M ) )
88		eluzelcn 11170	. . . . . . . . . . . . . . 15 |- ( M e. ( ZZ>= ` 2 ) -> M e. CC )
89	50, 88	syl 17	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. CC )
90	89	addid2d 9833	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( 0 + M ) = M )
91	87, 90	eqtrd 2470	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = M )
92	91	oveq2d 6321	. . . . . . . . . . 11 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r M ) )
93	81, 86, 92	3eqtr4d 2480	. . . . . . . . . 10 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
94	93, 5	syl 17	. . . . . . . . 9 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
95	94	3exp 1204	. . . . . . . 8 |- ( 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 381	. . . . . . 7 |- ( 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 220	. . . . . 6 |- ( N = 0 -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
98	7, 97	jaoi 380	. . . . 5 |- ( ( 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 17	. . . 4 |- ( N e. NN0 -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
100		elnn1uz2 11235	. . . . . . . 8 |- ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
101	100	biimpi 197	. . . . . . 7 |- ( N e. NN -> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
102		coires1 5373	. . . . . . . . . . . 12 |- ( R o. ( _I |` ( dom R u. ran R ) ) ) = ( R |` ( dom R u. ran R ) )
103		resss 5148	. . . . . . . . . . . 12 |- ( R |` ( dom R u. ran R ) ) C_ R
104	102, 103	eqsstri 3500	. . . . . . . . . . 11 |- ( R o. ( _I |` ( dom R u. ran R ) ) ) C_ R
105	104	a1i 11	. . . . . . . . . 10 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R o. ( _I |` ( dom R u. ran R ) ) ) C_ R )
106		simp1 1005	. . . . . . . . . . . . 13 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> N = 1 )
107	106	oveq2d 6321	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 1 ) )
108	37	3ad2ant3 1028	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r 1 ) = R )
109	107, 108	eqtrd 2470	. . . . . . . . . . 11 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = R )
110		simp2 1006	. . . . . . . . . . . . 13 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> M = 0 )
111	110	oveq2d 6321	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
112	32	3ad2ant3 1028	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
113	111, 112	eqtrd 2470	. . . . . . . . . . 11 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
114	109, 113	coeq12d 5019	. . . . . . . . . 10 |- ( ( 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 6323	. . . . . . . . . . . . 13 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( N + M ) = ( 1 + 0 ) )
116		1cnd 9658	. . . . . . . . . . . . . 14 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> 1 e. CC )
117	116	addid1d 9832	. . . . . . . . . . . . 13 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( 1 + 0 ) = 1 )
118	115, 117	eqtrd 2470	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( N + M ) = 1 )
119	118	oveq2d 6321	. . . . . . . . . . 11 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 1 ) )
120	119, 108	eqtrd 2470	. . . . . . . . . 10 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = R )
121	105, 114, 120	3sstr4d 3513	. . . . . . . . 9 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
122	121	3exp 1204	. . . . . . . 8 |- ( N = 1 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
123		coires1 5373	. . . . . . . . . . . 12 |- ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( R ^r N ) |` ( dom R u. ran R ) )
124		relexpuzrel 13094	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r N ) )
125	124	3adant2 1024	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> Rel ( R ^r N ) )
126		simp1 1005	. . . . . . . . . . . . . . . 16 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. ( ZZ>= ` 2 ) )
127		eluz2nn 11197	. . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` 2 ) -> N e. NN )
128	126, 127	syl 17	. . . . . . . . . . . . . . 15 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. NN )
129		simp3 1007	. . . . . . . . . . . . . . 15 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> R e. V )
130		relexpnndm 13083	. . . . . . . . . . . . . . 15 |- ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
131	128, 129, 130	syl2anc 665	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
132		ssun1 3635	. . . . . . . . . . . . . 14 |- dom R C_ ( dom R u. ran R )
133	131, 132	syl6ss 3482	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
134		relssres 5162	. . . . . . . . . . . . 13 |- ( ( 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 665	. . . . . . . . . . . 12 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) |` ( dom R u. ran R ) ) = ( R ^r N ) )
136	123, 135	syl5eq 2482	. . . . . . . . . . 11 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( R ^r N ) )
137		simp2 1006	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> M = 0 )
138	137	oveq2d 6321	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
139	32	3ad2ant3 1028	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
140	138, 139	eqtrd 2470	. . . . . . . . . . . 12 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
141	140	coeq2d 5017	. . . . . . . . . . 11 |- ( ( 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 6321	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = ( N + 0 ) )
143		eluzelcn 11170	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` 2 ) -> N e. CC )
144	126, 143	syl 17	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. CC )
145	144	addid1d 9832	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + 0 ) = N )
146	142, 145	eqtrd 2470	. . . . . . . . . . . 12 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = N )
147	146	oveq2d 6321	. . . . . . . . . . 11 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r N ) )
148	136, 141, 147	3eqtr4d 2480	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
149	148, 5	syl 17	. . . . . . . . 9 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
150	149	3exp 1204	. . . . . . . 8 |- ( 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 380	. . . . . . 7 |- ( ( 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 17	. . . . . 6 |- ( N e. NN -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
153		coires1 5373	. . . . . . . . . 10 |- ( ( _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 5137	. . . . . . . . . 10 |- ( ( _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 3677	. . . . . . . . . . 11 |- ( ( dom R u. ran R ) i^i ( dom R u. ran R ) ) = ( dom R u. ran R )
156	155	reseq2i 5122	. . . . . . . . . 10 |- ( _I |` ( ( dom R u. ran R ) i^i ( dom R u. ran R ) ) ) = ( _I |` ( dom R u. ran R ) )
157	153, 154, 156	3eqtri 2462	. . . . . . . . 9 |- ( ( _I |` ( dom R u. ran R ) ) o. ( _I |` ( dom R u. ran R ) ) ) = ( _I |` ( dom R u. ran R ) )
158		simp1 1005	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> N = 0 )
159	158	oveq2d 6321	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
160	32	3ad2ant3 1028	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
161	159, 160	eqtrd 2470	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
162		simp2 1006	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> M = 0 )
163	162	oveq2d 6321	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
164	163, 160	eqtrd 2470	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
165	161, 164	coeq12d 5019	. . . . . . . . 9 |- ( ( 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 6323	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = ( 0 + 0 ) )
167		00id 9807	. . . . . . . . . . . . 13 |- ( 0 + 0 ) = 0
168	167	a1i 11	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( 0 + 0 ) = 0 )
169	166, 168	eqtrd 2470	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = 0 )
170	169	oveq2d 6321	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 0 ) )
171	170, 160	eqtrd 2470	. . . . . . . . 9 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( _I |` ( dom R u. ran R ) ) )
172	157, 165, 171	3eqtr4a 2496	. . . . . . . 8 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
173	172, 5	syl 17	. . . . . . 7 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
174	173	3exp 1204	. . . . . 6 |- ( N = 0 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
175	152, 174	jaoi 380	. . . . 5 |- ( ( 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 17	. . . 4 |- ( N e. NN0 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
177	99, 176	jaod 381	. . 3 |- ( 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 220	. 2 |- ( N e. NN0 -> ( M e. NN0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
179	178	3imp 1199	1 |- ( ( N e. NN0 /\ M e. NN0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )

Syntax hints:   -> wi 4   <-> wb 187   \/ wo 369   /\ w3a 982   = wceq 1437   e. wcel 1870   _Vcvv 3087   u. cun 3440   i^i cin 3441   C_ wss 3442   _I cid 4764   `'ccnv 4853   dom cdm 4854   ran crn 4855   |` cres 4856   o. ccom 4858   Rel wrel 4859   ` cfv 5601  (class class class)co 6305   CCcc 9536   0cc0 9538   1c1 9539   + caddc 9541   NNcn 10609   2c2 10659   NN0cn0 10869   ZZ>=cuz 11159   ^r crelexp 13062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615

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 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  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 7036  df-recs 7098  df-rdg 7136  df-er 7371  df-en 7578  df-dom 7579  df-sdom 7580  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-nn 10610  df-2 10668  df-n0 10870  df-z 10938  df-uz 11160  df-seq 12211  df-relexp 13063

This theorem is referenced by:  iunrelexpuztr  35950  cotrclrcl  35973