Metamath Proof Explorer

Theorem relexpsucr

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

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

Proof

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