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 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )