relexpaddg

Description: Relation composition becomes addition under exponentiation except when the exponents total to one and the class isn't a relation. (Contributed by RP, 30-May-2020)

		Ref	Expression
	Assertion	relexpaddg	$⊢ (N \in ℕ_{0} \land (M \in ℕ_{0} \land R \in V \land (N + M = 1 \to Rel R))) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		elnn0	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℕ \lor M = 0)$
3		relexpaddnn	$⊢ (N \in ℕ \land M \in ℕ \land R \in V) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$
4	3	a1d	$⊢ (N \in ℕ \land M \in ℕ \land R \in V) \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))$
5	4	3exp	$⊢ N \in ℕ \to (M \in ℕ \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
6	5	com12	$⊢ M \in ℕ \to (N \in ℕ \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
7		elnn1uz2	$⊢ N \in ℕ \leftrightarrow (N = 1 \lor N \in ℤ_{\geq 2})$
8		coires1	$⊢ (R ↑_{r} N) \circ ({I ↾}_{(dom R \cup ran R)}) = {(R ↑_{r} N) ↾}_{(dom R \cup ran R)}$
9		simpll	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to N = 1$
10		simplr	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to M = 0$
11	9 10	oveq12d	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to N + M = 1 + 0$
12		1p0e1	$⊢ 1 + 0 = 1$
13	11 12	syl6eq	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to N + M = 1$
14		simprr	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to (N + M = 1 \to Rel R)$
15	13 14	mpd	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to Rel R$
16	9	oveq2d	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to R ↑_{r} N = R ↑_{r} 1$
17		simprl	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to R \in V$
18		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
19	17 18	syl	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to R ↑_{r} 1 = R$
20	16 19	eqtrd	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to R ↑_{r} N = R$
21	20	releqd	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to (Rel (R ↑_{r} N) \leftrightarrow Rel R)$
22	15 21	mpbird	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to Rel (R ↑_{r} N)$
23		1nn	$⊢ 1 \in ℕ$
24	9 23	eqeltrdi	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to N \in ℕ$
25		relexpnndm	$⊢ (N \in ℕ \land R \in V) \to dom (R ↑_{r} N) \subseteq dom R$
26	24 17 25	syl2anc	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to dom (R ↑_{r} N) \subseteq dom R$
27		ssun1	$⊢ dom R \subseteq dom R \cup ran R$
28	26 27	sstrdi	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to dom (R ↑_{r} N) \subseteq dom R \cup ran R$
29		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$
30	22 28 29	syl2anc	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to {(R ↑_{r} N) ↾}_{(dom R \cup ran R)} = R ↑_{r} N$
31	8 30	syl5eq	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to (R ↑_{r} N) \circ ({I ↾}_{(dom R \cup ran R)}) = R ↑_{r} N$
32	10	oveq2d	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to R ↑_{r} M = R ↑_{r} 0$
33		relexp0g	$⊢ R \in V \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
34	17 33	syl	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
35	32 34	eqtrd	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to R ↑_{r} M = {I ↾}_{(dom R \cup ran R)}$
36	35	coeq2d	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to (R ↑_{r} N) \circ (R ↑_{r} M) = (R ↑_{r} N) \circ ({I ↾}_{(dom R \cup ran R)})$
37	10	oveq2d	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to N + M = N + 0$
38		ax-1cn	$⊢ 1 \in ℂ$
39	9 38	eqeltrdi	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to N \in ℂ$
40	39	addid1d	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to N + 0 = N$
41	37 40	eqtrd	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to N + M = N$
42	41	oveq2d	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to R ↑_{r} (N + M) = R ↑_{r} N$
43	31 36 42	3eqtr4d	$⊢ ((N = 1 \land M = 0) \land (R \in V \land (N + M = 1 \to Rel R))) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$
44	43	exp43	$⊢ N = 1 \to (M = 0 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
45		simp1	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to N \in ℤ_{\geq 2}$
46		simp3	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to R \in V$
47		relexpuzrel	$⊢ (N \in ℤ_{\geq 2} \land R \in V) \to Rel (R ↑_{r} N)$
48	45 46 47	syl2anc	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to Rel (R ↑_{r} N)$
49		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
50	45 49	syl	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to N \in ℕ$
51	50 46 25	syl2anc	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to dom (R ↑_{r} N) \subseteq dom R$
52	51 27	sstrdi	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to dom (R ↑_{r} N) \subseteq dom R \cup ran R$
53	48 52 29	syl2anc	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to {(R ↑_{r} N) ↾}_{(dom R \cup ran R)} = R ↑_{r} N$
54	8 53	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$
55		simp2	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to M = 0$
56	55	oveq2d	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to R ↑_{r} M = R ↑_{r} 0$
57	46 33	syl	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
58	56 57	eqtrd	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to R ↑_{r} M = {I ↾}_{(dom R \cup ran R)}$
59	58	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)})$
60	55	oveq2d	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to N + M = N + 0$
61		eluzelcn	$⊢ N \in ℤ_{\geq 2} \to N \in ℂ$
62	45 61	syl	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to N \in ℂ$
63	62	addid1d	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to N + 0 = N$
64	60 63	eqtrd	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to N + M = N$
65	64	oveq2d	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to R ↑_{r} (N + M) = R ↑_{r} N$
66	54 59 65	3eqtr4d	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$
67	66	a1d	$⊢ (N \in ℤ_{\geq 2} \land M = 0 \land R \in V) \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))$
68	67	3exp	$⊢ N \in ℤ_{\geq 2} \to (M = 0 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
69	44 68	jaoi	$⊢ (N = 1 \lor N \in ℤ_{\geq 2}) \to (M = 0 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
70	7 69	sylbi	$⊢ N \in ℕ \to (M = 0 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
71	70	com12	$⊢ M = 0 \to (N \in ℕ \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
72	6 71	jaoi	$⊢ (M \in ℕ \lor M = 0) \to (N \in ℕ \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
73	2 72	sylbi	$⊢ M \in ℕ_{0} \to (N \in ℕ \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
74	73	com12	$⊢ N \in ℕ \to (M \in ℕ_{0} \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
75	74	3impd	$⊢ N \in ℕ \to ((M \in ℕ_{0} \land R \in V \land (N + M = 1 \to Rel R)) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))$
76		elnn1uz2	$⊢ M \in ℕ \leftrightarrow (M = 1 \lor M \in ℤ_{\geq 2})$
77		coires1	$⊢ R^{-1} \circ ({I ↾}_{(dom R^{-1} \cup ran R^{-1})}) = {R^{-1} ↾}_{(dom R^{-1} \cup ran R^{-1})}$
78		relcnv	$⊢ Rel R^{-1}$
79		ssun1	$⊢ dom R^{-1} \subseteq dom R^{-1} \cup ran R^{-1}$
80	78 79	pm3.2i	$⊢ (Rel R^{-1} \land dom R^{-1} \subseteq dom R^{-1} \cup ran R^{-1})$
81		relssres	$⊢ (Rel R^{-1} \land dom R^{-1} \subseteq dom R^{-1} \cup ran R^{-1}) \to {R^{-1} ↾}_{(dom R^{-1} \cup ran R^{-1})} = R^{-1}$
82	80 81	mp1i	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to {R^{-1} ↾}_{(dom R^{-1} \cup ran R^{-1})} = R^{-1}$
83	77 82	syl5eq	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to R^{-1} \circ ({I ↾}_{(dom R^{-1} \cup ran R^{-1})}) = R^{-1}$
84		cnvco	$⊢ {((R ↑_{r} N) \circ (R ↑_{r} M))}^{-1} = {(R ↑_{r} M)}^{-1} \circ {(R ↑_{r} N)}^{-1}$
85		simplr	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to M = 1$
86		1nn0	$⊢ 1 \in ℕ_{0}$
87	85 86	eqeltrdi	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to M \in ℕ_{0}$
88		simprl	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to R \in V$
89		relexpcnv	$⊢ (M \in ℕ_{0} \land R \in V) \to {(R ↑_{r} M)}^{-1} = R^{-1} ↑_{r} M$
90	87 88 89	syl2anc	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to {(R ↑_{r} M)}^{-1} = R^{-1} ↑_{r} M$
91	85	oveq2d	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to R^{-1} ↑_{r} M = R^{-1} ↑_{r} 1$
92		cnvexg	$⊢ R \in V \to R^{-1} \in V$
93	88 92	syl	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to R^{-1} \in V$
94		relexp1g	$⊢ R^{-1} \in V \to R^{-1} ↑_{r} 1 = R^{-1}$
95	93 94	syl	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to R^{-1} ↑_{r} 1 = R^{-1}$
96	90 91 95	3eqtrd	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to {(R ↑_{r} M)}^{-1} = R^{-1}$
97		simpll	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to N = 0$
98		0nn0	$⊢ 0 \in ℕ_{0}$
99	97 98	eqeltrdi	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to N \in ℕ_{0}$
100		relexpcnv	$⊢ (N \in ℕ_{0} \land R \in V) \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N$
101	99 88 100	syl2anc	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N$
102	97	oveq2d	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to R^{-1} ↑_{r} N = R^{-1} ↑_{r} 0$
103		relexp0g	$⊢ R^{-1} \in V \to R^{-1} ↑_{r} 0 = {I ↾}_{(dom R^{-1} \cup ran R^{-1})}$
104	93 103	syl	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to R^{-1} ↑_{r} 0 = {I ↾}_{(dom R^{-1} \cup ran R^{-1})}$
105	101 102 104	3eqtrd	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to {(R ↑_{r} N)}^{-1} = {I ↾}_{(dom R^{-1} \cup ran R^{-1})}$
106	96 105	coeq12d	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to {(R ↑_{r} M)}^{-1} \circ {(R ↑_{r} N)}^{-1} = R^{-1} \circ ({I ↾}_{(dom R^{-1} \cup ran R^{-1})})$
107	84 106	syl5eq	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to {((R ↑_{r} N) \circ (R ↑_{r} M))}^{-1} = R^{-1} \circ ({I ↾}_{(dom R^{-1} \cup ran R^{-1})})$
108	99 87	nn0addcld	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to N + M \in ℕ_{0}$
109		relexpcnv	$⊢ (N + M \in ℕ_{0} \land R \in V) \to {(R ↑_{r} (N + M))}^{-1} = R^{-1} ↑_{r} (N + M)$
110	108 88 109	syl2anc	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to {(R ↑_{r} (N + M))}^{-1} = R^{-1} ↑_{r} (N + M)$
111	97 85	oveq12d	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to N + M = 0 + 1$
112		0p1e1	$⊢ 0 + 1 = 1$
113	111 112	syl6eq	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to N + M = 1$
114	113	oveq2d	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to R^{-1} ↑_{r} (N + M) = R^{-1} ↑_{r} 1$
115	110 114 95	3eqtrd	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to {(R ↑_{r} (N + M))}^{-1} = R^{-1}$
116	83 107 115	3eqtr4d	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to {((R ↑_{r} N) \circ (R ↑_{r} M))}^{-1} = {(R ↑_{r} (N + M))}^{-1}$
117		relco	$⊢ Rel ((R ↑_{r} N) \circ (R ↑_{r} M))$
118		simprr	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to (N + M = 1 \to Rel R)$
119	113 118	mpd	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to Rel R$
120	113	oveq2d	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to R ↑_{r} (N + M) = R ↑_{r} 1$
121	88 18	syl	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to R ↑_{r} 1 = R$
122	120 121	eqtrd	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to R ↑_{r} (N + M) = R$
123	122	releqd	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to (Rel (R ↑_{r} (N + M)) \leftrightarrow Rel R)$
124	119 123	mpbird	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to Rel (R ↑_{r} (N + M))$
125		cnveqb	$⊢ (Rel ((R ↑_{r} N) \circ (R ↑_{r} M)) \land Rel (R ↑_{r} (N + M))) \to ((R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M) \leftrightarrow {((R ↑_{r} N) \circ (R ↑_{r} M))}^{-1} = {(R ↑_{r} (N + M))}^{-1})$
126	117 124 125	sylancr	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to ((R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M) \leftrightarrow {((R ↑_{r} N) \circ (R ↑_{r} M))}^{-1} = {(R ↑_{r} (N + M))}^{-1})$
127	116 126	mpbird	$⊢ ((N = 0 \land M = 1) \land (R \in V \land (N + M = 1 \to Rel R))) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$
128	127	exp43	$⊢ N = 0 \to (M = 1 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
129	128	com12	$⊢ M = 1 \to (N = 0 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
130		coires1	$⊢ (R^{-1} ↑_{r} M) \circ ({I ↾}_{(dom R^{-1} \cup ran R^{-1})}) = {(R^{-1} ↑_{r} M) ↾}_{(dom R^{-1} \cup ran R^{-1})}$
131		simp2	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to M \in ℤ_{\geq 2}$
132		simp3	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to R \in V$
133	132 92	syl	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to R^{-1} \in V$
134		relexpuzrel	$⊢ (M \in ℤ_{\geq 2} \land R^{-1} \in V) \to Rel (R^{-1} ↑_{r} M)$
135	131 133 134	syl2anc	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to Rel (R^{-1} ↑_{r} M)$
136		eluz2nn	$⊢ M \in ℤ_{\geq 2} \to M \in ℕ$
137	131 136	syl	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to M \in ℕ$
138		relexpnndm	$⊢ (M \in ℕ \land R^{-1} \in V) \to dom (R^{-1} ↑_{r} M) \subseteq dom R^{-1}$
139	137 133 138	syl2anc	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to dom (R^{-1} ↑_{r} M) \subseteq dom R^{-1}$
140	139 79	sstrdi	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to dom (R^{-1} ↑_{r} M) \subseteq dom R^{-1} \cup ran R^{-1}$
141		relssres	$⊢ (Rel (R^{-1} ↑_{r} M) \land dom (R^{-1} ↑_{r} M) \subseteq dom R^{-1} \cup ran R^{-1}) \to {(R^{-1} ↑_{r} M) ↾}_{(dom R^{-1} \cup ran R^{-1})} = R^{-1} ↑_{r} M$
142	135 140 141	syl2anc	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to {(R^{-1} ↑_{r} M) ↾}_{(dom R^{-1} \cup ran R^{-1})} = R^{-1} ↑_{r} M$
143	130 142	syl5eq	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to (R^{-1} ↑_{r} M) \circ ({I ↾}_{(dom R^{-1} \cup ran R^{-1})}) = R^{-1} ↑_{r} M$
144		simp1	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to N = 0$
145	144	oveq2d	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to R^{-1} ↑_{r} N = R^{-1} ↑_{r} 0$
146	133 103	syl	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to R^{-1} ↑_{r} 0 = {I ↾}_{(dom R^{-1} \cup ran R^{-1})}$
147	145 146	eqtrd	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to R^{-1} ↑_{r} N = {I ↾}_{(dom R^{-1} \cup ran R^{-1})}$
148	147	coeq2d	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to (R^{-1} ↑_{r} M) \circ (R^{-1} ↑_{r} N) = (R^{-1} ↑_{r} M) \circ ({I ↾}_{(dom R^{-1} \cup ran R^{-1})})$
149	144	oveq1d	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to N + M = 0 + M$
150		eluzelcn	$⊢ M \in ℤ_{\geq 2} \to M \in ℂ$
151	131 150	syl	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to M \in ℂ$
152	151	addid2d	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to 0 + M = M$
153	149 152	eqtrd	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to N + M = M$
154	153	oveq2d	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to R^{-1} ↑_{r} (N + M) = R^{-1} ↑_{r} M$
155	143 148 154	3eqtr4d	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to (R^{-1} ↑_{r} M) \circ (R^{-1} ↑_{r} N) = R^{-1} ↑_{r} (N + M)$
156		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
157	131 136 156	3syl	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to M \in ℕ_{0}$
158	157 132 89	syl2anc	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to {(R ↑_{r} M)}^{-1} = R^{-1} ↑_{r} M$
159	144 98	eqeltrdi	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to N \in ℕ_{0}$
160	159 132 100	syl2anc	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N$
161	158 160	coeq12d	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to {(R ↑_{r} M)}^{-1} \circ {(R ↑_{r} N)}^{-1} = (R^{-1} ↑_{r} M) \circ (R^{-1} ↑_{r} N)$
162	84 161	syl5eq	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to {((R ↑_{r} N) \circ (R ↑_{r} M))}^{-1} = (R^{-1} ↑_{r} M) \circ (R^{-1} ↑_{r} N)$
163	159 157	nn0addcld	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to N + M \in ℕ_{0}$
164	163 132 109	syl2anc	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to {(R ↑_{r} (N + M))}^{-1} = R^{-1} ↑_{r} (N + M)$
165	155 162 164	3eqtr4d	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to {((R ↑_{r} N) \circ (R ↑_{r} M))}^{-1} = {(R ↑_{r} (N + M))}^{-1}$
166	159	nn0cnd	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to N \in ℂ$
167	151 166	addcomd	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to M + N = N + M$
168		uzaddcl	$⊢ (M \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to M + N \in ℤ_{\geq 2}$
169	131 159 168	syl2anc	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to M + N \in ℤ_{\geq 2}$
170	167 169	eqeltrrd	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to N + M \in ℤ_{\geq 2}$
171		relexpuzrel	$⊢ (N + M \in ℤ_{\geq 2} \land R \in V) \to Rel (R ↑_{r} (N + M))$
172	170 132 171	syl2anc	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to Rel (R ↑_{r} (N + M))$
173	117 172 125	sylancr	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to ((R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M) \leftrightarrow {((R ↑_{r} N) \circ (R ↑_{r} M))}^{-1} = {(R ↑_{r} (N + M))}^{-1})$
174	165 173	mpbird	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$
175	174	a1d	$⊢ (N = 0 \land M \in ℤ_{\geq 2} \land R \in V) \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))$
176	175	3exp	$⊢ N = 0 \to (M \in ℤ_{\geq 2} \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
177	176	com12	$⊢ M \in ℤ_{\geq 2} \to (N = 0 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
178	129 177	jaoi	$⊢ (M = 1 \lor M \in ℤ_{\geq 2}) \to (N = 0 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
179	76 178	sylbi	$⊢ M \in ℕ \to (N = 0 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
180		coires1	$⊢ (R ↑_{r} 0) \circ ({I ↾}_{(dom R \cup ran R)}) = {(R ↑_{r} 0) ↾}_{(dom R \cup ran R)}$
181		simp3	$⊢ (N = 0 \land M = 0 \land R \in V) \to R \in V$
182		relexp0rel	$⊢ R \in V \to Rel (R ↑_{r} 0)$
183	181 182	syl	$⊢ (N = 0 \land M = 0 \land R \in V) \to Rel (R ↑_{r} 0)$
184	181 33	syl	$⊢ (N = 0 \land M = 0 \land R \in V) \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
185	184	dmeqd	$⊢ (N = 0 \land M = 0 \land R \in V) \to dom (R ↑_{r} 0) = dom ({I ↾}_{(dom R \cup ran R)})$
186		dmresi	$⊢ dom ({I ↾}_{(dom R \cup ran R)}) = dom R \cup ran R$
187	185 186	syl6eq	$⊢ (N = 0 \land M = 0 \land R \in V) \to dom (R ↑_{r} 0) = dom R \cup ran R$
188		eqimss	$⊢ dom (R ↑_{r} 0) = dom R \cup ran R \to dom (R ↑_{r} 0) \subseteq dom R \cup ran R$
189	187 188	syl	$⊢ (N = 0 \land M = 0 \land R \in V) \to dom (R ↑_{r} 0) \subseteq dom R \cup ran R$
190		relssres	$⊢ (Rel (R ↑_{r} 0) \land dom (R ↑_{r} 0) \subseteq dom R \cup ran R) \to {(R ↑_{r} 0) ↾}_{(dom R \cup ran R)} = R ↑_{r} 0$
191	183 189 190	syl2anc	$⊢ (N = 0 \land M = 0 \land R \in V) \to {(R ↑_{r} 0) ↾}_{(dom R \cup ran R)} = R ↑_{r} 0$
192	180 191	syl5eq	$⊢ (N = 0 \land M = 0 \land R \in V) \to (R ↑_{r} 0) \circ ({I ↾}_{(dom R \cup ran R)}) = R ↑_{r} 0$
193		simp1	$⊢ (N = 0 \land M = 0 \land R \in V) \to N = 0$
194	193	oveq2d	$⊢ (N = 0 \land M = 0 \land R \in V) \to R ↑_{r} N = R ↑_{r} 0$
195		simp2	$⊢ (N = 0 \land M = 0 \land R \in V) \to M = 0$
196	195	oveq2d	$⊢ (N = 0 \land M = 0 \land R \in V) \to R ↑_{r} M = R ↑_{r} 0$
197	196 184	eqtrd	$⊢ (N = 0 \land M = 0 \land R \in V) \to R ↑_{r} M = {I ↾}_{(dom R \cup ran R)}$
198	194 197	coeq12d	$⊢ (N = 0 \land M = 0 \land R \in V) \to (R ↑_{r} N) \circ (R ↑_{r} M) = (R ↑_{r} 0) \circ ({I ↾}_{(dom R \cup ran R)})$
199	193 195	oveq12d	$⊢ (N = 0 \land M = 0 \land R \in V) \to N + M = 0 + 0$
200		00id	$⊢ 0 + 0 = 0$
201	199 200	syl6eq	$⊢ (N = 0 \land M = 0 \land R \in V) \to N + M = 0$
202	201	oveq2d	$⊢ (N = 0 \land M = 0 \land R \in V) \to R ↑_{r} (N + M) = R ↑_{r} 0$
203	192 198 202	3eqtr4d	$⊢ (N = 0 \land M = 0 \land R \in V) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$
204	203	a1d	$⊢ (N = 0 \land M = 0 \land R \in V) \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))$
205	204	3exp	$⊢ N = 0 \to (M = 0 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
206	205	com12	$⊢ M = 0 \to (N = 0 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
207	179 206	jaoi	$⊢ (M \in ℕ \lor M = 0) \to (N = 0 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
208	2 207	sylbi	$⊢ M \in ℕ_{0} \to (N = 0 \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
209	208	com12	$⊢ N = 0 \to (M \in ℕ_{0} \to (R \in V \to ((N + M = 1 \to Rel R) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))))$
210	209	3impd	$⊢ N = 0 \to ((M \in ℕ_{0} \land R \in V \land (N + M = 1 \to Rel R)) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))$
211	75 210	jaoi	$⊢ (N \in ℕ \lor N = 0) \to ((M \in ℕ_{0} \land R \in V \land (N + M = 1 \to Rel R)) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))$
212	1 211	sylbi	$⊢ N \in ℕ_{0} \to ((M \in ℕ_{0} \land R \in V \land (N + M = 1 \to Rel R)) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))$
213	212	imp	$⊢ (N \in ℕ_{0} \land (M \in ℕ_{0} \land R \in V \land (N + M = 1 \to Rel R))) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$

Metamath Proof Explorer

Theorem relexpaddg

Proof