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 \in ℕ_{0} \land M \in ℕ_{0} \land R \in V) \to (R ↑_{r} N) \circ (R ↑_{r} M) \subseteq R ↑_{r} (N + M)$

Proof

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

Metamath Proof Explorer

Theorem relexpaddss

Proof