Metamath Proof Explorer

Theorem relexpsucl

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

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

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 )
3 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ ℕ )
4 relexpsucnnl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) )
5 2 3 4 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) )
6 5 3expib ⊢ ( 𝑁 ∈ ℕ → ( ( Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) ) )
7 simp2 ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → Rel 𝑅 )
8 relcoi1 ⊢ ( Rel 𝑅 → ( 𝑅 ∘ ( I ↾ ∪ ∪ 𝑅 ) ) = 𝑅 )
9 7 8 syl ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ∘ ( I ↾ ∪ ∪ 𝑅 ) ) = 𝑅 )
10 simp1 ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 = 0 )
11 10 oveq2d ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( 𝑅 ↑𝑟 0 ) )
12 simp3 ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 )
13 relexp0 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) )
14 12 7 13 syl2anc ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) )
15 11 14 eqtrd ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( I ↾ ∪ ∪ 𝑅 ) )
16 15 coeq2d ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) = ( 𝑅 ∘ ( I ↾ ∪ ∪ 𝑅 ) ) )
17 10 oveq1d ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 1 ) = ( 0 + 1 ) )
18 0p1e1 ⊢ ( 0 + 1 ) = 1
19 17 18 eqtrdi ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 1 ) = 1 )
20 19 oveq2d ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ↑𝑟 1 ) )
21 relexp1g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
22 12 21 syl ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
23 20 22 eqtrd ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = 𝑅 )
24 9 16 23 3eqtr4rd ⊢ ( ( 𝑁 = 0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) )
25 24 3expib ⊢ ( 𝑁 = 0 → ( ( Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) ) )
26 6 25 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( ( Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) ) )
27 1 26 sylbi ⊢ ( 𝑁 ∈ ℕ0 → ( ( Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) ) )
28 27 3impib ⊢ ( ( 𝑁 ∈ ℕ0 ∧ Rel 𝑅 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) )
29 28 3com13 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑁 ) ) )