relexpaddnn

Description: Relation composition becomes addition under exponentiation. (Contributed by RP, 23-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ n = 1 \to R ↑_{r} n = R ↑_{r} 1$
2	1	coeq1d	$⊢ n = 1 \to (R ↑_{r} n) \circ (R ↑_{r} M) = (R ↑_{r} 1) \circ (R ↑_{r} M)$
3		oveq1	$⊢ n = 1 \to n + M = 1 + M$
4	3	oveq2d	$⊢ n = 1 \to R ↑_{r} (n + M) = R ↑_{r} (1 + M)$
5	2 4	eqeq12d	$⊢ n = 1 \to ((R ↑_{r} n) \circ (R ↑_{r} M) = R ↑_{r} (n + M) \leftrightarrow (R ↑_{r} 1) \circ (R ↑_{r} M) = R ↑_{r} (1 + M))$
6	5	imbi2d	$⊢ n = 1 \to (((M \in ℕ \land R \in V) \to (R ↑_{r} n) \circ (R ↑_{r} M) = R ↑_{r} (n + M)) \leftrightarrow ((M \in ℕ \land R \in V) \to (R ↑_{r} 1) \circ (R ↑_{r} M) = R ↑_{r} (1 + M)))$
7		oveq2	$⊢ n = k \to R ↑_{r} n = R ↑_{r} k$
8	7	coeq1d	$⊢ n = k \to (R ↑_{r} n) \circ (R ↑_{r} M) = (R ↑_{r} k) \circ (R ↑_{r} M)$
9		oveq1	$⊢ n = k \to n + M = k + M$
10	9	oveq2d	$⊢ n = k \to R ↑_{r} (n + M) = R ↑_{r} (k + M)$
11	8 10	eqeq12d	$⊢ n = k \to ((R ↑_{r} n) \circ (R ↑_{r} M) = R ↑_{r} (n + M) \leftrightarrow (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M))$
12	11	imbi2d	$⊢ n = k \to (((M \in ℕ \land R \in V) \to (R ↑_{r} n) \circ (R ↑_{r} M) = R ↑_{r} (n + M)) \leftrightarrow ((M \in ℕ \land R \in V) \to (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)))$
13		oveq2	$⊢ n = k + 1 \to R ↑_{r} n = R ↑_{r} (k + 1)$
14	13	coeq1d	$⊢ n = k + 1 \to (R ↑_{r} n) \circ (R ↑_{r} M) = (R ↑_{r} (k + 1)) \circ (R ↑_{r} M)$
15		oveq1	$⊢ n = k + 1 \to n + M = k + 1 + M$
16	15	oveq2d	$⊢ n = k + 1 \to R ↑_{r} (n + M) = R ↑_{r} (k + 1 + M)$
17	14 16	eqeq12d	$⊢ n = k + 1 \to ((R ↑_{r} n) \circ (R ↑_{r} M) = R ↑_{r} (n + M) \leftrightarrow (R ↑_{r} (k + 1)) \circ (R ↑_{r} M) = R ↑_{r} (k + 1 + M))$
18	17	imbi2d	$⊢ n = k + 1 \to (((M \in ℕ \land R \in V) \to (R ↑_{r} n) \circ (R ↑_{r} M) = R ↑_{r} (n + M)) \leftrightarrow ((M \in ℕ \land R \in V) \to (R ↑_{r} (k + 1)) \circ (R ↑_{r} M) = R ↑_{r} (k + 1 + M)))$
19		oveq2	$⊢ n = N \to R ↑_{r} n = R ↑_{r} N$
20	19	coeq1d	$⊢ n = N \to (R ↑_{r} n) \circ (R ↑_{r} M) = (R ↑_{r} N) \circ (R ↑_{r} M)$
21		oveq1	$⊢ n = N \to n + M = N + M$
22	21	oveq2d	$⊢ n = N \to R ↑_{r} (n + M) = R ↑_{r} (N + M)$
23	20 22	eqeq12d	$⊢ n = N \to ((R ↑_{r} n) \circ (R ↑_{r} M) = R ↑_{r} (n + M) \leftrightarrow (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))$
24	23	imbi2d	$⊢ n = N \to (((M \in ℕ \land R \in V) \to (R ↑_{r} n) \circ (R ↑_{r} M) = R ↑_{r} (n + M)) \leftrightarrow ((M \in ℕ \land R \in V) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)))$
25		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
26	25	adantl	$⊢ (M \in ℕ \land R \in V) \to R ↑_{r} 1 = R$
27	26	coeq1d	$⊢ (M \in ℕ \land R \in V) \to (R ↑_{r} 1) \circ (R ↑_{r} M) = R \circ (R ↑_{r} M)$
28		relexpsucnnl	$⊢ (R \in V \land M \in ℕ) \to R ↑_{r} (M + 1) = R \circ (R ↑_{r} M)$
29	28	ancoms	$⊢ (M \in ℕ \land R \in V) \to R ↑_{r} (M + 1) = R \circ (R ↑_{r} M)$
30		simpl	$⊢ (M \in ℕ \land R \in V) \to M \in ℕ$
31	30	nncnd	$⊢ (M \in ℕ \land R \in V) \to M \in ℂ$
32		1cnd	$⊢ (M \in ℕ \land R \in V) \to 1 \in ℂ$
33	31 32	addcomd	$⊢ (M \in ℕ \land R \in V) \to M + 1 = 1 + M$
34	33	oveq2d	$⊢ (M \in ℕ \land R \in V) \to R ↑_{r} (M + 1) = R ↑_{r} (1 + M)$
35	27 29 34	3eqtr2d	$⊢ (M \in ℕ \land R \in V) \to (R ↑_{r} 1) \circ (R ↑_{r} M) = R ↑_{r} (1 + M)$
36		simp2r	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to R \in V$
37		simp1	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to k \in ℕ$
38		relexpsucnnl	$⊢ (R \in V \land k \in ℕ) \to R ↑_{r} (k + 1) = R \circ (R ↑_{r} k)$
39	36 37 38	syl2anc	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to R ↑_{r} (k + 1) = R \circ (R ↑_{r} k)$
40	39	coeq1d	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to (R ↑_{r} (k + 1)) \circ (R ↑_{r} M) = (R \circ (R ↑_{r} k)) \circ (R ↑_{r} M)$
41		coass	$⊢ (R \circ (R ↑_{r} k)) \circ (R ↑_{r} M) = R \circ ((R ↑_{r} k) \circ (R ↑_{r} M))$
42	40 41	syl6eq	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to (R ↑_{r} (k + 1)) \circ (R ↑_{r} M) = R \circ ((R ↑_{r} k) \circ (R ↑_{r} M))$
43		simp3	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)$
44	43	coeq2d	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to R \circ ((R ↑_{r} k) \circ (R ↑_{r} M)) = R \circ (R ↑_{r} (k + M))$
45	37	nncnd	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to k \in ℂ$
46		1cnd	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to 1 \in ℂ$
47	31	3ad2ant2	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to M \in ℂ$
48	45 46 47	add32d	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to k + 1 + M = k + M + 1$
49	48	oveq2d	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to R ↑_{r} (k + 1 + M) = R ↑_{r} (k + M + 1)$
50	30	3ad2ant2	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to M \in ℕ$
51	37 50	nnaddcld	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to k + M \in ℕ$
52		relexpsucnnl	$⊢ (R \in V \land k + M \in ℕ) \to R ↑_{r} (k + M + 1) = R \circ (R ↑_{r} (k + M))$
53	36 51 52	syl2anc	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to R ↑_{r} (k + M + 1) = R \circ (R ↑_{r} (k + M))$
54	49 53	eqtr2d	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to R \circ (R ↑_{r} (k + M)) = R ↑_{r} (k + 1 + M)$
55	42 44 54	3eqtrd	$⊢ (k \in ℕ \land (M \in ℕ \land R \in V) \land (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to (R ↑_{r} (k + 1)) \circ (R ↑_{r} M) = R ↑_{r} (k + 1 + M)$
56	55	3exp	$⊢ k \in ℕ \to ((M \in ℕ \land R \in V) \to ((R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M) \to (R ↑_{r} (k + 1)) \circ (R ↑_{r} M) = R ↑_{r} (k + 1 + M)))$
57	56	a2d	$⊢ k \in ℕ \to (((M \in ℕ \land R \in V) \to (R ↑_{r} k) \circ (R ↑_{r} M) = R ↑_{r} (k + M)) \to ((M \in ℕ \land R \in V) \to (R ↑_{r} (k + 1)) \circ (R ↑_{r} M) = R ↑_{r} (k + 1 + M)))$
58	6 12 18 24 35 57	nnind	$⊢ N \in ℕ \to ((M \in ℕ \land R \in V) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))$
59	58	3impib	$⊢ (N \in ℕ \land M \in ℕ \land R \in V) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$

Metamath Proof Explorer

Theorem relexpaddnn

Proof