relexpsucnnl

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

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ n = 1 \to n + 1 = 1 + 1$
2	1	oveq2d	$⊢ n = 1 \to R ↑_{r} (n + 1) = R ↑_{r} (1 + 1)$
3		oveq2	$⊢ n = 1 \to R ↑_{r} n = R ↑_{r} 1$
4	3	coeq2d	$⊢ n = 1 \to R \circ (R ↑_{r} n) = R \circ (R ↑_{r} 1)$
5	2 4	eqeq12d	$⊢ n = 1 \to (R ↑_{r} (n + 1) = R \circ (R ↑_{r} n) \leftrightarrow R ↑_{r} (1 + 1) = R \circ (R ↑_{r} 1))$
6	5	imbi2d	$⊢ n = 1 \to ((R \in V \to R ↑_{r} (n + 1) = R \circ (R ↑_{r} n)) \leftrightarrow (R \in V \to R ↑_{r} (1 + 1) = R \circ (R ↑_{r} 1)))$
7		oveq1	$⊢ n = m \to n + 1 = m + 1$
8	7	oveq2d	$⊢ n = m \to R ↑_{r} (n + 1) = R ↑_{r} (m + 1)$
9		oveq2	$⊢ n = m \to R ↑_{r} n = R ↑_{r} m$
10	9	coeq2d	$⊢ n = m \to R \circ (R ↑_{r} n) = R \circ (R ↑_{r} m)$
11	8 10	eqeq12d	$⊢ n = m \to (R ↑_{r} (n + 1) = R \circ (R ↑_{r} n) \leftrightarrow R ↑_{r} (m + 1) = R \circ (R ↑_{r} m))$
12	11	imbi2d	$⊢ n = m \to ((R \in V \to R ↑_{r} (n + 1) = R \circ (R ↑_{r} n)) \leftrightarrow (R \in V \to R ↑_{r} (m + 1) = R \circ (R ↑_{r} m)))$
13		oveq1	$⊢ n = m + 1 \to n + 1 = m + 1 + 1$
14	13	oveq2d	$⊢ n = m + 1 \to R ↑_{r} (n + 1) = R ↑_{r} (m + 1 + 1)$
15		oveq2	$⊢ n = m + 1 \to R ↑_{r} n = R ↑_{r} (m + 1)$
16	15	coeq2d	$⊢ n = m + 1 \to R \circ (R ↑_{r} n) = R \circ (R ↑_{r} (m + 1))$
17	14 16	eqeq12d	$⊢ n = m + 1 \to (R ↑_{r} (n + 1) = R \circ (R ↑_{r} n) \leftrightarrow R ↑_{r} (m + 1 + 1) = R \circ (R ↑_{r} (m + 1)))$
18	17	imbi2d	$⊢ n = m + 1 \to ((R \in V \to R ↑_{r} (n + 1) = R \circ (R ↑_{r} n)) \leftrightarrow (R \in V \to R ↑_{r} (m + 1 + 1) = R \circ (R ↑_{r} (m + 1))))$
19		oveq1	$⊢ n = N \to n + 1 = N + 1$
20	19	oveq2d	$⊢ n = N \to R ↑_{r} (n + 1) = R ↑_{r} (N + 1)$
21		oveq2	$⊢ n = N \to R ↑_{r} n = R ↑_{r} N$
22	21	coeq2d	$⊢ n = N \to R \circ (R ↑_{r} n) = R \circ (R ↑_{r} N)$
23	20 22	eqeq12d	$⊢ n = N \to (R ↑_{r} (n + 1) = R \circ (R ↑_{r} n) \leftrightarrow R ↑_{r} (N + 1) = R \circ (R ↑_{r} N))$
24	23	imbi2d	$⊢ n = N \to ((R \in V \to R ↑_{r} (n + 1) = R \circ (R ↑_{r} n)) \leftrightarrow (R \in V \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N)))$
25		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
26	25	coeq1d	$⊢ R \in V \to (R ↑_{r} 1) \circ R = R \circ R$
27		1nn	$⊢ 1 \in ℕ$
28		relexpsucnnr	$⊢ (R \in V \land 1 \in ℕ) \to R ↑_{r} (1 + 1) = (R ↑_{r} 1) \circ R$
29	27 28	mpan2	$⊢ R \in V \to R ↑_{r} (1 + 1) = (R ↑_{r} 1) \circ R$
30	25	coeq2d	$⊢ R \in V \to R \circ (R ↑_{r} 1) = R \circ R$
31	26 29 30	3eqtr4d	$⊢ R \in V \to R ↑_{r} (1 + 1) = R \circ (R ↑_{r} 1)$
32		coeq1	$⊢ R ↑_{r} (m + 1) = R \circ (R ↑_{r} m) \to (R ↑_{r} (m + 1)) \circ R = (R \circ (R ↑_{r} m)) \circ R$
33		coass	$⊢ (R \circ (R ↑_{r} m)) \circ R = R \circ ((R ↑_{r} m) \circ R)$
34	32 33	eqtrdi	$⊢ R ↑_{r} (m + 1) = R \circ (R ↑_{r} m) \to (R ↑_{r} (m + 1)) \circ R = R \circ ((R ↑_{r} m) \circ R)$
35	34	adantl	$⊢ ((R \in V \land m \in ℕ) \land R ↑_{r} (m + 1) = R \circ (R ↑_{r} m)) \to (R ↑_{r} (m + 1)) \circ R = R \circ ((R ↑_{r} m) \circ R)$
36		simpl	$⊢ ((R \in V \land m \in ℕ) \land R ↑_{r} (m + 1) = R \circ (R ↑_{r} m)) \to (R \in V \land m \in ℕ)$
37		peano2nn	$⊢ m \in ℕ \to m + 1 \in ℕ$
38	37	anim2i	$⊢ (R \in V \land m \in ℕ) \to (R \in V \land m + 1 \in ℕ)$
39		relexpsucnnr	$⊢ (R \in V \land m + 1 \in ℕ) \to R ↑_{r} (m + 1 + 1) = (R ↑_{r} (m + 1)) \circ R$
40	36 38 39	3syl	$⊢ ((R \in V \land m \in ℕ) \land R ↑_{r} (m + 1) = R \circ (R ↑_{r} m)) \to R ↑_{r} (m + 1 + 1) = (R ↑_{r} (m + 1)) \circ R$
41		relexpsucnnr	$⊢ (R \in V \land m \in ℕ) \to R ↑_{r} (m + 1) = (R ↑_{r} m) \circ R$
42	41	adantr	$⊢ ((R \in V \land m \in ℕ) \land R ↑_{r} (m + 1) = R \circ (R ↑_{r} m)) \to R ↑_{r} (m + 1) = (R ↑_{r} m) \circ R$
43	42	coeq2d	$⊢ ((R \in V \land m \in ℕ) \land R ↑_{r} (m + 1) = R \circ (R ↑_{r} m)) \to R \circ (R ↑_{r} (m + 1)) = R \circ ((R ↑_{r} m) \circ R)$
44	35 40 43	3eqtr4d	$⊢ ((R \in V \land m \in ℕ) \land R ↑_{r} (m + 1) = R \circ (R ↑_{r} m)) \to R ↑_{r} (m + 1 + 1) = R \circ (R ↑_{r} (m + 1))$
45	44	ex	$⊢ (R \in V \land m \in ℕ) \to (R ↑_{r} (m + 1) = R \circ (R ↑_{r} m) \to R ↑_{r} (m + 1 + 1) = R \circ (R ↑_{r} (m + 1)))$
46	45	expcom	$⊢ m \in ℕ \to (R \in V \to (R ↑_{r} (m + 1) = R \circ (R ↑_{r} m) \to R ↑_{r} (m + 1 + 1) = R \circ (R ↑_{r} (m + 1))))$
47	46	a2d	$⊢ m \in ℕ \to ((R \in V \to R ↑_{r} (m + 1) = R \circ (R ↑_{r} m)) \to (R \in V \to R ↑_{r} (m + 1 + 1) = R \circ (R ↑_{r} (m + 1))))$
48	6 12 18 24 31 47	nnind	$⊢ N \in ℕ \to (R \in V \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N))$
49	48	impcom	$⊢ (R \in V \land N \in ℕ) \to R ↑_{r} (N + 1) = R \circ (R ↑_{r} N)$

Metamath Proof Explorer

Theorem relexpsucnnl

Proof