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