relexpsucr

Description: A reduction for relation exponentiation to the right. (Contributed by RP, 23-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		simp3	$⊢ (N \in ℕ \land Rel R \land R \in V) \to R \in V$
3		simp1	$⊢ (N \in ℕ \land Rel R \land R \in V) \to N \in ℕ$
4		relexpsucnnr	$⊢ (R \in V \land N \in ℕ) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$
5	2 3 4	syl2anc	$⊢ (N \in ℕ \land Rel R \land R \in V) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$
6	5	3expib	$⊢ N \in ℕ \to ((Rel R \land R \in V) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R)$
7		simp2	$⊢ (N = 0 \land Rel R \land R \in V) \to Rel R$
8		relcoi2	$⊢ Rel R \to ({I ↾}_{⋃ ⋃ R}) \circ R = R$
9	8	eqcomd	$⊢ Rel R \to R = ({I ↾}_{⋃ ⋃ R}) \circ R$
10	7 9	syl	$⊢ (N = 0 \land Rel R \land R \in V) \to R = ({I ↾}_{⋃ ⋃ R}) \circ R$
11		simp1	$⊢ (N = 0 \land Rel R \land R \in V) \to N = 0$
12	11	oveq1d	$⊢ (N = 0 \land Rel R \land R \in V) \to N + 1 = 0 + 1$
13		0p1e1	$⊢ 0 + 1 = 1$
14	12 13	eqtrdi	$⊢ (N = 0 \land Rel R \land R \in V) \to N + 1 = 1$
15	14	oveq2d	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} (N + 1) = R ↑_{r} 1$
16		simp3	$⊢ (N = 0 \land Rel R \land R \in V) \to R \in V$
17		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
18	16 17	syl	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} 1 = R$
19	15 18	eqtrd	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} (N + 1) = R$
20	11	oveq2d	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} N = R ↑_{r} 0$
21		relexp0	$⊢ (R \in V \land Rel R) \to R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R}$
22	16 7 21	syl2anc	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R}$
23	20 22	eqtrd	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} N = {I ↾}_{⋃ ⋃ R}$
24	23	coeq1d	$⊢ (N = 0 \land Rel R \land R \in V) \to (R ↑_{r} N) \circ R = ({I ↾}_{⋃ ⋃ R}) \circ R$
25	10 19 24	3eqtr4d	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$
26	25	3expib	$⊢ N = 0 \to ((Rel R \land R \in V) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R)$
27	6 26	jaoi	$⊢ (N \in ℕ \lor N = 0) \to ((Rel R \land R \in V) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R)$
28	1 27	sylbi	$⊢ N \in ℕ_{0} \to ((Rel R \land R \in V) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R)$
29	28	3impib	$⊢ (N \in ℕ_{0} \land Rel R \land R \in V) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$
30	29	3com13	$⊢ (R \in V \land Rel R \land N \in ℕ_{0}) \to R ↑_{r} (N + 1) = (R ↑_{r} N) \circ R$

Metamath Proof Explorer

Theorem relexpsucr

Proof