Metamath Proof Explorer


Theorem relexpsucl

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

Ref Expression
Assertion relexpsucl RVRelRN0RrN+1=RRrN

Proof

Step Hyp Ref Expression
1 elnn0 N0NN=0
2 simp3 NRelRRVRV
3 simp1 NRelRRVN
4 relexpsucnnl RVNRrN+1=RRrN
5 2 3 4 syl2anc NRelRRVRrN+1=RRrN
6 5 3expib NRelRRVRrN+1=RRrN
7 simp2 N=0RelRRVRelR
8 relcoi1 RelRRIR=R
9 7 8 syl N=0RelRRVRIR=R
10 simp1 N=0RelRRVN=0
11 10 oveq2d N=0RelRRVRrN=Rr0
12 simp3 N=0RelRRVRV
13 relexp0 RVRelRRr0=IR
14 12 7 13 syl2anc N=0RelRRVRr0=IR
15 11 14 eqtrd N=0RelRRVRrN=IR
16 15 coeq2d N=0RelRRVRRrN=RIR
17 10 oveq1d N=0RelRRVN+1=0+1
18 0p1e1 0+1=1
19 17 18 eqtrdi N=0RelRRVN+1=1
20 19 oveq2d N=0RelRRVRrN+1=Rr1
21 relexp1g RVRr1=R
22 12 21 syl N=0RelRRVRr1=R
23 20 22 eqtrd N=0RelRRVRrN+1=R
24 9 16 23 3eqtr4rd N=0RelRRVRrN+1=RRrN
25 24 3expib N=0RelRRVRrN+1=RRrN
26 6 25 jaoi NN=0RelRRVRrN+1=RRrN
27 1 26 sylbi N0RelRRVRrN+1=RRrN
28 27 3impib N0RelRRVRrN+1=RRrN
29 28 3com13 RVRelRN0RrN+1=RRrN