Metamath Proof Explorer


Theorem relexpsucl

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

Ref Expression
Assertion relexpsucl R V Rel R N 0 R r N + 1 = R R r N

Proof

Step Hyp Ref Expression
1 elnn0 N 0 N N = 0
2 simp3 N Rel R R V R V
3 simp1 N Rel R R V N
4 relexpsucnnl R V N R r N + 1 = R R r N
5 2 3 4 syl2anc N Rel R R V R r N + 1 = R R r N
6 5 3expib N Rel R R V R r N + 1 = R R r N
7 simp2 N = 0 Rel R R V Rel R
8 relcoi1 Rel R R I R = R
9 7 8 syl N = 0 Rel R R V R I R = R
10 simp1 N = 0 Rel R R V N = 0
11 10 oveq2d N = 0 Rel R R V R r N = R r 0
12 simp3 N = 0 Rel R R V R V
13 relexp0 R V Rel R R r 0 = I R
14 12 7 13 syl2anc N = 0 Rel R R V R r 0 = I R
15 11 14 eqtrd N = 0 Rel R R V R r N = I R
16 15 coeq2d N = 0 Rel R R V R R r N = R I R
17 10 oveq1d N = 0 Rel R R V N + 1 = 0 + 1
18 0p1e1 0 + 1 = 1
19 17 18 eqtrdi N = 0 Rel R R V N + 1 = 1
20 19 oveq2d N = 0 Rel R R V R r N + 1 = R r 1
21 relexp1g R V R r 1 = R
22 12 21 syl N = 0 Rel R R V R r 1 = R
23 20 22 eqtrd N = 0 Rel R R V R r N + 1 = R
24 9 16 23 3eqtr4rd N = 0 Rel R R V R r N + 1 = R R r N
25 24 3expib N = 0 Rel R R V R r N + 1 = R R r N
26 6 25 jaoi N N = 0 Rel R R V R r N + 1 = R R r N
27 1 26 sylbi N 0 Rel R R V R r N + 1 = R R r N
28 27 3impib N 0 Rel R R V R r N + 1 = R R r N
29 28 3com13 R V Rel R N 0 R r N + 1 = R R r N