Metamath Proof Explorer


Theorem wkslem2

Description: Lemma 2 for walks to substitute the index of the condition for vertices and edges in a walk. (Contributed by AV, 23-Apr-2021)

Ref Expression
Assertion wkslem2 A=BA+1=Cif-PA=PA+1IFA=PAPAPA+1IFAif-PB=PCIFB=PBPBPCIFB

Proof

Step Hyp Ref Expression
1 fveq2 A=BPA=PB
2 1 adantr A=BA+1=CPA=PB
3 fveq2 A+1=CPA+1=PC
4 3 adantl A=BA+1=CPA+1=PC
5 2 4 eqeq12d A=BA+1=CPA=PA+1PB=PC
6 2fveq3 A=BIFA=IFB
7 1 sneqd A=BPA=PB
8 6 7 eqeq12d A=BIFA=PAIFB=PB
9 8 adantr A=BA+1=CIFA=PAIFB=PB
10 2 4 preq12d A=BA+1=CPAPA+1=PBPC
11 6 adantr A=BA+1=CIFA=IFB
12 10 11 sseq12d A=BA+1=CPAPA+1IFAPBPCIFB
13 5 9 12 ifpbi123d A=BA+1=Cif-PA=PA+1IFA=PAPAPA+1IFAif-PB=PCIFB=PBPBPCIFB