Metamath Proof Explorer

Theorem relexpmulnn

Description: With exponents limited to the counting numbers, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020)

Ref Expression
Assertion relexpmulnn ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = 1 → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 1 ) )
2 oveq2 ⊢ ( 𝑥 = 1 → ( 𝐽 · 𝑥 ) = ( 𝐽 · 1 ) )
3 2 oveq2d ⊢ ( 𝑥 = 1 → ( 𝑅 ↑𝑟 ( 𝐽 · 𝑥 ) ) = ( 𝑅 ↑𝑟 ( 𝐽 · 1 ) ) )
4 1 3 eqeq12d ⊢ ( 𝑥 = 1 → ( ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑥 ) ) ↔ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 1 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 1 ) ) ) )
5 4 imbi2d ⊢ ( 𝑥 = 1 → ( ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑥 ) ) ) ↔ ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 1 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 1 ) ) ) ) )
6 oveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) )
7 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐽 · 𝑥 ) = ( 𝐽 · 𝑦 ) )
8 7 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑅 ↑𝑟 ( 𝐽 · 𝑥 ) ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) )
9 6 8 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑥 ) ) ↔ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) )
10 9 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑥 ) ) ) ↔ ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) ) )
11 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) )
12 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐽 · 𝑥 ) = ( 𝐽 · ( 𝑦 + 1 ) ) )
13 12 oveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑅 ↑𝑟 ( 𝐽 · 𝑥 ) ) = ( 𝑅 ↑𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) )
14 11 13 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑥 ) ) ↔ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝑅 ↑𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) ) )
15 14 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑥 ) ) ) ↔ ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝑅 ↑𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) ) ) )
16 oveq2 ⊢ ( 𝑥 = 𝐾 → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) )
17 oveq2 ⊢ ( 𝑥 = 𝐾 → ( 𝐽 · 𝑥 ) = ( 𝐽 · 𝐾 ) )
18 17 oveq2d ⊢ ( 𝑥 = 𝐾 → ( 𝑅 ↑𝑟 ( 𝐽 · 𝑥 ) ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝐾 ) ) )
19 16 18 eqeq12d ⊢ ( 𝑥 = 𝐾 → ( ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑥 ) ) ↔ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝐾 ) ) ) )
20 19 imbi2d ⊢ ( 𝑥 = 𝐾 → ( ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑥 ) ) ) ↔ ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝐾 ) ) ) ) )
21 ovexd ⊢ ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( 𝑅 ↑𝑟 𝐽 ) ∈ V )
22 21 relexp1d ⊢ ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 1 ) = ( 𝑅 ↑𝑟 𝐽 ) )
23 simp1 ⊢ ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → 𝐽 ∈ ℕ )
24 nnre ⊢ ( 𝐽 ∈ ℕ → 𝐽 ∈ ℝ )
25 ax-1rid ⊢ ( 𝐽 ∈ ℝ → ( 𝐽 · 1 ) = 𝐽 )
26 23 24 25 3syl ⊢ ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( 𝐽 · 1 ) = 𝐽 )
27 26 eqcomd ⊢ ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → 𝐽 = ( 𝐽 · 1 ) )
28 27 oveq2d ⊢ ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( 𝑅 ↑𝑟 𝐽 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 1 ) ) )
29 22 28 eqtrd ⊢ ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 1 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 1 ) ) )
30 ovex ⊢ ( 𝑅 ↑𝑟 𝐽 ) ∈ V
31 simp1 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → 𝑦 ∈ ℕ )
32 relexpsucnnr ⊢ ( ( ( 𝑅 ↑𝑟 𝐽 ) ∈ V ∧ 𝑦 ∈ ℕ ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) ∘ ( 𝑅 ↑𝑟 𝐽 ) ) )
33 30 31 32 sylancr ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) ∘ ( 𝑅 ↑𝑟 𝐽 ) ) )
34 simp3 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) )
35 34 coeq1d ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) ∘ ( 𝑅 ↑𝑟 𝐽 ) ) = ( ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ∘ ( 𝑅 ↑𝑟 𝐽 ) ) )
36 simp21 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → 𝐽 ∈ ℕ )
37 36 31 nnmulcld ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( 𝐽 · 𝑦 ) ∈ ℕ )
38 simp22 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → 𝑅 ∈ 𝑉 )
39 relexpaddnn ⊢ ( ( ( 𝐽 · 𝑦 ) ∈ ℕ ∧ 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ∘ ( 𝑅 ↑𝑟 𝐽 ) ) = ( 𝑅 ↑𝑟 ( ( 𝐽 · 𝑦 ) + 𝐽 ) ) )
40 37 36 38 39 syl3anc ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ∘ ( 𝑅 ↑𝑟 𝐽 ) ) = ( 𝑅 ↑𝑟 ( ( 𝐽 · 𝑦 ) + 𝐽 ) ) )
41 35 40 eqtrd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) ∘ ( 𝑅 ↑𝑟 𝐽 ) ) = ( 𝑅 ↑𝑟 ( ( 𝐽 · 𝑦 ) + 𝐽 ) ) )
42 36 nncnd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → 𝐽 ∈ ℂ )
43 31 nncnd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → 𝑦 ∈ ℂ )
44 1cnd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → 1 ∈ ℂ )
45 42 43 44 adddid ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( 𝐽 · ( 𝑦 + 1 ) ) = ( ( 𝐽 · 𝑦 ) + ( 𝐽 · 1 ) ) )
46 42 mulridd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( 𝐽 · 1 ) = 𝐽 )
47 46 oveq2d ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝐽 · 𝑦 ) + ( 𝐽 · 1 ) ) = ( ( 𝐽 · 𝑦 ) + 𝐽 ) )
48 45 47 eqtr2d ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝐽 · 𝑦 ) + 𝐽 ) = ( 𝐽 · ( 𝑦 + 1 ) ) )
49 48 oveq2d ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( 𝑅 ↑𝑟 ( ( 𝐽 · 𝑦 ) + 𝐽 ) ) = ( 𝑅 ↑𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) )
50 41 49 eqtrd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) ∘ ( 𝑅 ↑𝑟 𝐽 ) ) = ( 𝑅 ↑𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) )
51 33 50 eqtrd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝑅 ↑𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) )
52 51 3exp ⊢ ( 𝑦 ∈ ℕ → ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝑅 ↑𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) ) ) )
53 52 a2d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝑅 ↑𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) ) ) )
54 5 10 15 20 29 53 nnind ⊢ ( 𝐾 ∈ ℕ → ( ( 𝐽 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝐾 ) ) ) )
55 54 3expd ⊢ ( 𝐾 ∈ ℕ → ( 𝐽 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( 𝐼 = ( 𝐽 · 𝐾 ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝐾 ) ) ) ) ) )
56 55 impcom ⊢ ( ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝑅 ∈ 𝑉 → ( 𝐼 = ( 𝐽 · 𝐾 ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝐾 ) ) ) ) )
57 56 impd ⊢ ( ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝐾 ) ) ) )
58 57 impcom ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 ( 𝐽 · 𝐾 ) ) )
59 simplr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → 𝐼 = ( 𝐽 · 𝐾 ) )
60 59 eqcomd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → ( 𝐽 · 𝐾 ) = 𝐼 )
61 60 oveq2d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → ( 𝑅 ↑𝑟 ( 𝐽 · 𝐾 ) ) = ( 𝑅 ↑𝑟 𝐼 ) )
62 58 61 eqtrd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )