Metamath Proof Explorer

Theorem relexpsucnnl

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

Ref Expression
Assertion relexpsucnnl ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 + 1 ) = ( 1 + 1 ) )
2 1 oveq2d ⊢ ( 𝑛 = 1 → ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ↑𝑟 ( 1 + 1 ) ) )
3 oveq2 ⊢ ( 𝑛 = 1 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 1 ) )
4 3 coeq2d ⊢ ( 𝑛 = 1 → ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 1 ) ) )
5 2 4 eqeq12d ⊢ ( 𝑛 = 1 → ( ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) ↔ ( 𝑅 ↑𝑟 ( 1 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 1 ) ) ) )
6 5 imbi2d ⊢ ( 𝑛 = 1 → ( ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) ) ↔ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( 1 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 1 ) ) ) ) )
7 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 + 1 ) = ( 𝑚 + 1 ) )
8 7 oveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
9 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑚 ) )
10 9 coeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) )
11 8 10 eqeq12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) ↔ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) ) )
12 11 imbi2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) ) ↔ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) ) ) )
13 oveq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 + 1 ) = ( ( 𝑚 + 1 ) + 1 ) )
14 13 oveq2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ↑𝑟 ( ( 𝑚 + 1 ) + 1 ) ) )
15 oveq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
16 15 coeq2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) )
17 14 16 eqeq12d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) ↔ ( 𝑅 ↑𝑟 ( ( 𝑚 + 1 ) + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) ) )
18 17 imbi2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) ) ↔ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( ( 𝑚 + 1 ) + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) ) ) )
19 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 + 1 ) = ( 𝑁 + 1 ) )
20 19 oveq2d ⊢ ( 𝑛 = 𝑁 → ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) )
21 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑁 ) )
22 21 coeq2d ⊢ ( 𝑛 = 𝑁 → ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) )
23 20 22 eqeq12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) ↔ ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) ) )
24 23 imbi2d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) ) ↔ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) ) ) )
25 relexp1g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
26 25 coeq1d ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 1 ) ∘ 𝑅 ) = ( 𝑅 ∘ 𝑅 ) )
27 1nn ⊢ 1 ∈ ℕ
28 relexpsucnnr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 1 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 1 + 1 ) ) = ( ( 𝑅 ↑𝑟 1 ) ∘ 𝑅 ) )
29 27 28 mpan2 ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( 1 + 1 ) ) = ( ( 𝑅 ↑𝑟 1 ) ∘ 𝑅 ) )
30 25 coeq2d ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∘ ( 𝑅 ↑𝑟 1 ) ) = ( 𝑅 ∘ 𝑅 ) )
31 26 29 30 3eqtr4d ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( 1 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 1 ) ) )
32 coeq1 ⊢ ( ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) → ( ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ∘ 𝑅 ) = ( ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) ∘ 𝑅 ) )
33 coass ⊢ ( ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) ∘ 𝑅 ) = ( 𝑅 ∘ ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
34 32 33 eqtrdi ⊢ ( ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) → ( ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ∘ 𝑅 ) = ( 𝑅 ∘ ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) ) )
35 34 adantl ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) ) → ( ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ∘ 𝑅 ) = ( 𝑅 ∘ ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) ) )
36 simpl ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) ) → ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) )
37 peano2nn ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ℕ )
38 37 anim2i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) → ( 𝑅 ∈ 𝑉 ∧ ( 𝑚 + 1 ) ∈ ℕ ) )
39 relexpsucnnr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑚 + 1 ) ∈ ℕ ) → ( 𝑅 ↑𝑟 ( ( 𝑚 + 1 ) + 1 ) ) = ( ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ∘ 𝑅 ) )
40 36 38 39 3syl ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) ) → ( 𝑅 ↑𝑟 ( ( 𝑚 + 1 ) + 1 ) ) = ( ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ∘ 𝑅 ) )
41 relexpsucnnr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
42 41 adantr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
43 42 coeq2d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) ) → ( 𝑅 ∘ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) = ( 𝑅 ∘ ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) ) )
44 35 40 43 3eqtr4d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) ) → ( 𝑅 ↑𝑟 ( ( 𝑚 + 1 ) + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) )
45 44 ex ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) → ( 𝑅 ↑𝑟 ( ( 𝑚 + 1 ) + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) ) )
46 45 expcom ⊢ ( 𝑚 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) → ( 𝑅 ↑𝑟 ( ( 𝑚 + 1 ) + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) ) ) )
47 46 a2d ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑚 ) ) ) → ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( ( 𝑚 + 1 ) + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) ) ) )
48 6 12 18 24 31 47 nnind ⊢ ( 𝑁 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) ) )
49 48 impcom ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) )