relexpcnv

Description: Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020)

		Ref	Expression
	Assertion	relexpcnv	$⊢ (N \in ℕ_{0} \land R \in V) \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		oveq2	$⊢ n = 1 \to R ↑_{r} n = R ↑_{r} 1$
3	2	cnveqd	$⊢ n = 1 \to {(R ↑_{r} n)}^{-1} = {(R ↑_{r} 1)}^{-1}$
4		oveq2	$⊢ n = 1 \to R^{-1} ↑_{r} n = R^{-1} ↑_{r} 1$
5	3 4	eqeq12d	$⊢ n = 1 \to ({(R ↑_{r} n)}^{-1} = R^{-1} ↑_{r} n \leftrightarrow {(R ↑_{r} 1)}^{-1} = R^{-1} ↑_{r} 1)$
6	5	imbi2d	$⊢ n = 1 \to ((R \in V \to {(R ↑_{r} n)}^{-1} = R^{-1} ↑_{r} n) \leftrightarrow (R \in V \to {(R ↑_{r} 1)}^{-1} = R^{-1} ↑_{r} 1))$
7		oveq2	$⊢ n = m \to R ↑_{r} n = R ↑_{r} m$
8	7	cnveqd	$⊢ n = m \to {(R ↑_{r} n)}^{-1} = {(R ↑_{r} m)}^{-1}$
9		oveq2	$⊢ n = m \to R^{-1} ↑_{r} n = R^{-1} ↑_{r} m$
10	8 9	eqeq12d	$⊢ n = m \to ({(R ↑_{r} n)}^{-1} = R^{-1} ↑_{r} n \leftrightarrow {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m)$
11	10	imbi2d	$⊢ n = m \to ((R \in V \to {(R ↑_{r} n)}^{-1} = R^{-1} ↑_{r} n) \leftrightarrow (R \in V \to {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m))$
12		oveq2	$⊢ n = m + 1 \to R ↑_{r} n = R ↑_{r} (m + 1)$
13	12	cnveqd	$⊢ n = m + 1 \to {(R ↑_{r} n)}^{-1} = {(R ↑_{r} (m + 1))}^{-1}$
14		oveq2	$⊢ n = m + 1 \to R^{-1} ↑_{r} n = R^{-1} ↑_{r} (m + 1)$
15	13 14	eqeq12d	$⊢ n = m + 1 \to ({(R ↑_{r} n)}^{-1} = R^{-1} ↑_{r} n \leftrightarrow {(R ↑_{r} (m + 1))}^{-1} = R^{-1} ↑_{r} (m + 1))$
16	15	imbi2d	$⊢ n = m + 1 \to ((R \in V \to {(R ↑_{r} n)}^{-1} = R^{-1} ↑_{r} n) \leftrightarrow (R \in V \to {(R ↑_{r} (m + 1))}^{-1} = R^{-1} ↑_{r} (m + 1)))$
17		oveq2	$⊢ n = N \to R ↑_{r} n = R ↑_{r} N$
18	17	cnveqd	$⊢ n = N \to {(R ↑_{r} n)}^{-1} = {(R ↑_{r} N)}^{-1}$
19		oveq2	$⊢ n = N \to R^{-1} ↑_{r} n = R^{-1} ↑_{r} N$
20	18 19	eqeq12d	$⊢ n = N \to ({(R ↑_{r} n)}^{-1} = R^{-1} ↑_{r} n \leftrightarrow {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N)$
21	20	imbi2d	$⊢ n = N \to ((R \in V \to {(R ↑_{r} n)}^{-1} = R^{-1} ↑_{r} n) \leftrightarrow (R \in V \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N))$
22		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
23	22	cnveqd	$⊢ R \in V \to {(R ↑_{r} 1)}^{-1} = R^{-1}$
24		cnvexg	$⊢ R \in V \to R^{-1} \in V$
25		relexp1g	$⊢ R^{-1} \in V \to R^{-1} ↑_{r} 1 = R^{-1}$
26	24 25	syl	$⊢ R \in V \to R^{-1} ↑_{r} 1 = R^{-1}$
27	23 26	eqtr4d	$⊢ R \in V \to {(R ↑_{r} 1)}^{-1} = R^{-1} ↑_{r} 1$
28		cnvco	$⊢ {((R ↑_{r} m) \circ R)}^{-1} = R^{-1} \circ {(R ↑_{r} m)}^{-1}$
29		simp3	$⊢ (m \in ℕ \land R \in V \land {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m) \to {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m$
30	29	coeq2d	$⊢ (m \in ℕ \land R \in V \land {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m) \to R^{-1} \circ {(R ↑_{r} m)}^{-1} = R^{-1} \circ (R^{-1} ↑_{r} m)$
31	28 30	eqtrid	$⊢ (m \in ℕ \land R \in V \land {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m) \to {((R ↑_{r} m) \circ R)}^{-1} = R^{-1} \circ (R^{-1} ↑_{r} m)$
32		simp2	$⊢ (m \in ℕ \land R \in V \land {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m) \to R \in V$
33		simp1	$⊢ (m \in ℕ \land R \in V \land {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m) \to m \in ℕ$
34		relexpsucnnr	$⊢ (R \in V \land m \in ℕ) \to R ↑_{r} (m + 1) = (R ↑_{r} m) \circ R$
35	32 33 34	syl2anc	$⊢ (m \in ℕ \land R \in V \land {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m) \to R ↑_{r} (m + 1) = (R ↑_{r} m) \circ R$
36	35	cnveqd	$⊢ (m \in ℕ \land R \in V \land {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m) \to {(R ↑_{r} (m + 1))}^{-1} = {((R ↑_{r} m) \circ R)}^{-1}$
37	32 24	syl	$⊢ (m \in ℕ \land R \in V \land {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m) \to R^{-1} \in V$
38		relexpsucnnl	$⊢ (R^{-1} \in V \land m \in ℕ) \to R^{-1} ↑_{r} (m + 1) = R^{-1} \circ (R^{-1} ↑_{r} m)$
39	37 33 38	syl2anc	$⊢ (m \in ℕ \land R \in V \land {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m) \to R^{-1} ↑_{r} (m + 1) = R^{-1} \circ (R^{-1} ↑_{r} m)$
40	31 36 39	3eqtr4d	$⊢ (m \in ℕ \land R \in V \land {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m) \to {(R ↑_{r} (m + 1))}^{-1} = R^{-1} ↑_{r} (m + 1)$
41	40	3exp	$⊢ m \in ℕ \to (R \in V \to ({(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m \to {(R ↑_{r} (m + 1))}^{-1} = R^{-1} ↑_{r} (m + 1)))$
42	41	a2d	$⊢ m \in ℕ \to ((R \in V \to {(R ↑_{r} m)}^{-1} = R^{-1} ↑_{r} m) \to (R \in V \to {(R ↑_{r} (m + 1))}^{-1} = R^{-1} ↑_{r} (m + 1)))$
43	6 11 16 21 27 42	nnind	$⊢ N \in ℕ \to (R \in V \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N)$
44		cnvresid	$⊢ {({I ↾}_{(dom R \cup ran R)})}^{-1} = {I ↾}_{(dom R \cup ran R)}$
45		uncom	$⊢ dom R \cup ran R = ran R \cup dom R$
46		df-rn	$⊢ ran R = dom R^{-1}$
47		dfdm4	$⊢ dom R = ran R^{-1}$
48	46 47	uneq12i	$⊢ ran R \cup dom R = dom R^{-1} \cup ran R^{-1}$
49	45 48	eqtri	$⊢ dom R \cup ran R = dom R^{-1} \cup ran R^{-1}$
50	49	reseq2i	$⊢ {I ↾}_{(dom R \cup ran R)} = {I ↾}_{(dom R^{-1} \cup ran R^{-1})}$
51	44 50	eqtri	$⊢ {({I ↾}_{(dom R \cup ran R)})}^{-1} = {I ↾}_{(dom R^{-1} \cup ran R^{-1})}$
52		oveq2	$⊢ N = 0 \to R ↑_{r} N = R ↑_{r} 0$
53		relexp0g	$⊢ R \in V \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
54	52 53	sylan9eq	$⊢ (N = 0 \land R \in V) \to R ↑_{r} N = {I ↾}_{(dom R \cup ran R)}$
55	54	cnveqd	$⊢ (N = 0 \land R \in V) \to {(R ↑_{r} N)}^{-1} = {({I ↾}_{(dom R \cup ran R)})}^{-1}$
56		oveq2	$⊢ N = 0 \to R^{-1} ↑_{r} N = R^{-1} ↑_{r} 0$
57	56	adantr	$⊢ (N = 0 \land R \in V) \to R^{-1} ↑_{r} N = R^{-1} ↑_{r} 0$
58		simpr	$⊢ (N = 0 \land R \in V) \to R \in V$
59		relexp0g	$⊢ R^{-1} \in V \to R^{-1} ↑_{r} 0 = {I ↾}_{(dom R^{-1} \cup ran R^{-1})}$
60	58 24 59	3syl	$⊢ (N = 0 \land R \in V) \to R^{-1} ↑_{r} 0 = {I ↾}_{(dom R^{-1} \cup ran R^{-1})}$
61	57 60	eqtrd	$⊢ (N = 0 \land R \in V) \to R^{-1} ↑_{r} N = {I ↾}_{(dom R^{-1} \cup ran R^{-1})}$
62	51 55 61	3eqtr4a	$⊢ (N = 0 \land R \in V) \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N$
63	62	ex	$⊢ N = 0 \to (R \in V \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N)$
64	43 63	jaoi	$⊢ (N \in ℕ \lor N = 0) \to (R \in V \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N)$
65	1 64	sylbi	$⊢ N \in ℕ_{0} \to (R \in V \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N)$
66	65	imp	$⊢ (N \in ℕ_{0} \land R \in V) \to {(R ↑_{r} N)}^{-1} = R^{-1} ↑_{r} N$

Metamath Proof Explorer

Theorem relexpcnv

Proof