relexpsucl

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

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

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		relexpsucnnl	$⊢ (R \in V \land N \in ℕ) \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N)$
5	2 3 4	syl2anc	$⊢ (N \in ℕ \land Rel R \land R \in V) \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N)$
6	5	3expib	$⊢ N \in ℕ \to ((Rel R \land R \in V) \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N))$
7		simp2	$⊢ (N = 0 \land Rel R \land R \in V) \to Rel R$
8		relcoi1	$⊢ Rel R \to R \circ ({I ↾}_{⋃ ⋃ R}) = R$
9	7 8	syl	$⊢ (N = 0 \land Rel R \land R \in V) \to R \circ ({I ↾}_{⋃ ⋃ R}) = R$
10		simp1	$⊢ (N = 0 \land Rel R \land R \in V) \to N = 0$
11	10	oveq2d	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} N = R ↑_{r} 0$
12		simp3	$⊢ (N = 0 \land Rel R \land R \in V) \to R \in V$
13		relexp0	$⊢ (R \in V \land Rel R) \to R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R}$
14	12 7 13	syl2anc	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R}$
15	11 14	eqtrd	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} N = {I ↾}_{⋃ ⋃ R}$
16	15	coeq2d	$⊢ (N = 0 \land Rel R \land R \in V) \to R \circ (R ↑_{r} N) = R \circ ({I ↾}_{⋃ ⋃ R})$
17	10	oveq1d	$⊢ (N = 0 \land Rel R \land R \in V) \to N + 1 = 0 + 1$
18		0p1e1	$⊢ 0 + 1 = 1$
19	17 18	eqtrdi	$⊢ (N = 0 \land Rel R \land R \in V) \to N + 1 = 1$
20	19	oveq2d	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} (N + 1) = R ↑_{r} 1$
21		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
22	12 21	syl	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} 1 = R$
23	20 22	eqtrd	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} (N + 1) = R$
24	9 16 23	3eqtr4rd	$⊢ (N = 0 \land Rel R \land R \in V) \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N)$
25	24	3expib	$⊢ N = 0 \to ((Rel R \land R \in V) \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N))$
26	6 25	jaoi	$⊢ (N \in ℕ \lor N = 0) \to ((Rel R \land R \in V) \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N))$
27	1 26	sylbi	$⊢ N \in ℕ_{0} \to ((Rel R \land R \in V) \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N))$
28	27	3impib	$⊢ (N \in ℕ_{0} \land Rel R \land R \in V) \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N)$
29	28	3com13	$⊢ (R \in V \land Rel R \land N \in ℕ_{0}) \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N)$

Metamath Proof Explorer

Theorem relexpsucl

Proof