Metamath Proof Explorer


Theorem relexpaddnn

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

Ref Expression
Assertion relexpaddnn ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 𝑁 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑁 + 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑛 = 1 → ( 𝑅𝑟 𝑛 ) = ( 𝑅𝑟 1 ) )
2 1 coeq1d ( 𝑛 = 1 → ( ( 𝑅𝑟 𝑛 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( ( 𝑅𝑟 1 ) ∘ ( 𝑅𝑟 𝑀 ) ) )
3 oveq1 ( 𝑛 = 1 → ( 𝑛 + 𝑀 ) = ( 1 + 𝑀 ) )
4 3 oveq2d ( 𝑛 = 1 → ( 𝑅𝑟 ( 𝑛 + 𝑀 ) ) = ( 𝑅𝑟 ( 1 + 𝑀 ) ) )
5 2 4 eqeq12d ( 𝑛 = 1 → ( ( ( 𝑅𝑟 𝑛 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑛 + 𝑀 ) ) ↔ ( ( 𝑅𝑟 1 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 1 + 𝑀 ) ) ) )
6 5 imbi2d ( 𝑛 = 1 → ( ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 𝑛 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑛 + 𝑀 ) ) ) ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 1 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 1 + 𝑀 ) ) ) ) )
7 oveq2 ( 𝑛 = 𝑘 → ( 𝑅𝑟 𝑛 ) = ( 𝑅𝑟 𝑘 ) )
8 7 coeq1d ( 𝑛 = 𝑘 → ( ( 𝑅𝑟 𝑛 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) )
9 oveq1 ( 𝑛 = 𝑘 → ( 𝑛 + 𝑀 ) = ( 𝑘 + 𝑀 ) )
10 9 oveq2d ( 𝑛 = 𝑘 → ( 𝑅𝑟 ( 𝑛 + 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) )
11 8 10 eqeq12d ( 𝑛 = 𝑘 → ( ( ( 𝑅𝑟 𝑛 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑛 + 𝑀 ) ) ↔ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) )
12 11 imbi2d ( 𝑛 = 𝑘 → ( ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 𝑛 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑛 + 𝑀 ) ) ) ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) ) )
13 oveq2 ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑅𝑟 𝑛 ) = ( 𝑅𝑟 ( 𝑘 + 1 ) ) )
14 13 coeq1d ( 𝑛 = ( 𝑘 + 1 ) → ( ( 𝑅𝑟 𝑛 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( ( 𝑅𝑟 ( 𝑘 + 1 ) ) ∘ ( 𝑅𝑟 𝑀 ) ) )
15 oveq1 ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 + 𝑀 ) = ( ( 𝑘 + 1 ) + 𝑀 ) )
16 15 oveq2d ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑅𝑟 ( 𝑛 + 𝑀 ) ) = ( 𝑅𝑟 ( ( 𝑘 + 1 ) + 𝑀 ) ) )
17 14 16 eqeq12d ( 𝑛 = ( 𝑘 + 1 ) → ( ( ( 𝑅𝑟 𝑛 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑛 + 𝑀 ) ) ↔ ( ( 𝑅𝑟 ( 𝑘 + 1 ) ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( ( 𝑘 + 1 ) + 𝑀 ) ) ) )
18 17 imbi2d ( 𝑛 = ( 𝑘 + 1 ) → ( ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 𝑛 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑛 + 𝑀 ) ) ) ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 ( 𝑘 + 1 ) ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( ( 𝑘 + 1 ) + 𝑀 ) ) ) ) )
19 oveq2 ( 𝑛 = 𝑁 → ( 𝑅𝑟 𝑛 ) = ( 𝑅𝑟 𝑁 ) )
20 19 coeq1d ( 𝑛 = 𝑁 → ( ( 𝑅𝑟 𝑛 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( ( 𝑅𝑟 𝑁 ) ∘ ( 𝑅𝑟 𝑀 ) ) )
21 oveq1 ( 𝑛 = 𝑁 → ( 𝑛 + 𝑀 ) = ( 𝑁 + 𝑀 ) )
22 21 oveq2d ( 𝑛 = 𝑁 → ( 𝑅𝑟 ( 𝑛 + 𝑀 ) ) = ( 𝑅𝑟 ( 𝑁 + 𝑀 ) ) )
23 20 22 eqeq12d ( 𝑛 = 𝑁 → ( ( ( 𝑅𝑟 𝑛 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑛 + 𝑀 ) ) ↔ ( ( 𝑅𝑟 𝑁 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑁 + 𝑀 ) ) ) )
24 23 imbi2d ( 𝑛 = 𝑁 → ( ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 𝑛 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑛 + 𝑀 ) ) ) ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 𝑁 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
25 relexp1g ( 𝑅𝑉 → ( 𝑅𝑟 1 ) = 𝑅 )
26 25 adantl ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( 𝑅𝑟 1 ) = 𝑅 )
27 26 coeq1d ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 1 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅 ∘ ( 𝑅𝑟 𝑀 ) ) )
28 relexpsucnnl ( ( 𝑅𝑉𝑀 ∈ ℕ ) → ( 𝑅𝑟 ( 𝑀 + 1 ) ) = ( 𝑅 ∘ ( 𝑅𝑟 𝑀 ) ) )
29 28 ancoms ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( 𝑅𝑟 ( 𝑀 + 1 ) ) = ( 𝑅 ∘ ( 𝑅𝑟 𝑀 ) ) )
30 simpl ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → 𝑀 ∈ ℕ )
31 30 nncnd ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → 𝑀 ∈ ℂ )
32 1cnd ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → 1 ∈ ℂ )
33 31 32 addcomd ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( 𝑀 + 1 ) = ( 1 + 𝑀 ) )
34 33 oveq2d ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( 𝑅𝑟 ( 𝑀 + 1 ) ) = ( 𝑅𝑟 ( 1 + 𝑀 ) ) )
35 27 29 34 3eqtr2d ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 1 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 1 + 𝑀 ) ) )
36 simp2r ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → 𝑅𝑉 )
37 simp1 ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → 𝑘 ∈ ℕ )
38 relexpsucnnl ( ( 𝑅𝑉𝑘 ∈ ℕ ) → ( 𝑅𝑟 ( 𝑘 + 1 ) ) = ( 𝑅 ∘ ( 𝑅𝑟 𝑘 ) ) )
39 36 37 38 syl2anc ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → ( 𝑅𝑟 ( 𝑘 + 1 ) ) = ( 𝑅 ∘ ( 𝑅𝑟 𝑘 ) ) )
40 39 coeq1d ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → ( ( 𝑅𝑟 ( 𝑘 + 1 ) ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( ( 𝑅 ∘ ( 𝑅𝑟 𝑘 ) ) ∘ ( 𝑅𝑟 𝑀 ) ) )
41 coass ( ( 𝑅 ∘ ( 𝑅𝑟 𝑘 ) ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅 ∘ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) )
42 40 41 eqtrdi ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → ( ( 𝑅𝑟 ( 𝑘 + 1 ) ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅 ∘ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) ) )
43 simp3 ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) )
44 43 coeq2d ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → ( 𝑅 ∘ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) ) = ( 𝑅 ∘ ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) )
45 37 nncnd ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → 𝑘 ∈ ℂ )
46 1cnd ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → 1 ∈ ℂ )
47 31 3ad2ant2 ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → 𝑀 ∈ ℂ )
48 45 46 47 add32d ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → ( ( 𝑘 + 1 ) + 𝑀 ) = ( ( 𝑘 + 𝑀 ) + 1 ) )
49 48 oveq2d ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → ( 𝑅𝑟 ( ( 𝑘 + 1 ) + 𝑀 ) ) = ( 𝑅𝑟 ( ( 𝑘 + 𝑀 ) + 1 ) ) )
50 30 3ad2ant2 ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → 𝑀 ∈ ℕ )
51 37 50 nnaddcld ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → ( 𝑘 + 𝑀 ) ∈ ℕ )
52 relexpsucnnl ( ( 𝑅𝑉 ∧ ( 𝑘 + 𝑀 ) ∈ ℕ ) → ( 𝑅𝑟 ( ( 𝑘 + 𝑀 ) + 1 ) ) = ( 𝑅 ∘ ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) )
53 36 51 52 syl2anc ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → ( 𝑅𝑟 ( ( 𝑘 + 𝑀 ) + 1 ) ) = ( 𝑅 ∘ ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) )
54 49 53 eqtr2d ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → ( 𝑅 ∘ ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) = ( 𝑅𝑟 ( ( 𝑘 + 1 ) + 𝑀 ) ) )
55 42 44 54 3eqtrd ( ( 𝑘 ∈ ℕ ∧ ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) ∧ ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → ( ( 𝑅𝑟 ( 𝑘 + 1 ) ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( ( 𝑘 + 1 ) + 𝑀 ) ) )
56 55 3exp ( 𝑘 ∈ ℕ → ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) → ( ( 𝑅𝑟 ( 𝑘 + 1 ) ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( ( 𝑘 + 1 ) + 𝑀 ) ) ) ) )
57 56 a2d ( 𝑘 ∈ ℕ → ( ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 𝑘 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑘 + 𝑀 ) ) ) → ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 ( 𝑘 + 1 ) ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( ( 𝑘 + 1 ) + 𝑀 ) ) ) ) )
58 6 12 18 24 35 57 nnind ( 𝑁 ∈ ℕ → ( ( 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 𝑁 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑁 + 𝑀 ) ) ) )
59 58 3impib ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 𝑁 ) ∘ ( 𝑅𝑟 𝑀 ) ) = ( 𝑅𝑟 ( 𝑁 + 𝑀 ) ) )