Metamath Proof Explorer


Theorem clwlkclwwlkf1lem2

Description: Lemma 2 for clwlkclwwlkf1 . (Contributed by AV, 24-May-2022) (Revised by AV, 30-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlkf.c C=wClWalksG|11stw
clwlkclwwlkf.a A=1stU
clwlkclwwlkf.b B=2ndU
clwlkclwwlkf.d D=1stW
clwlkclwwlkf.e E=2ndW
Assertion clwlkclwwlkf1lem2 UCWCBprefixA=EprefixDA=Di0..^ABi=Ei

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c C=wClWalksG|11stw
2 clwlkclwwlkf.a A=1stU
3 clwlkclwwlkf.b B=2ndU
4 clwlkclwwlkf.d D=1stW
5 clwlkclwwlkf.e E=2ndW
6 1 2 3 clwlkclwwlkflem UCAWalksGBB0=BAA
7 1 4 5 clwlkclwwlkflem WCDWalksGEE0=EDD
8 6 7 anim12i UCWCAWalksGBB0=BAADWalksGEE0=EDD
9 eqid VtxG=VtxG
10 9 wlkpwrd AWalksGBBWordVtxG
11 10 3ad2ant1 AWalksGBB0=BAABWordVtxG
12 9 wlkpwrd DWalksGEEWordVtxG
13 12 3ad2ant1 DWalksGEE0=EDDEWordVtxG
14 11 13 anim12i AWalksGBB0=BAADWalksGEE0=EDDBWordVtxGEWordVtxG
15 nnnn0 AA0
16 15 3ad2ant3 AWalksGBB0=BAAA0
17 nnnn0 DD0
18 17 3ad2ant3 DWalksGEE0=EDDD0
19 16 18 anim12i AWalksGBB0=BAADWalksGEE0=EDDA0D0
20 wlklenvp1 AWalksGBB=A+1
21 nnre AA
22 21 lep1d AAA+1
23 breq2 B=A+1ABAA+1
24 22 23 syl5ibr B=A+1AAB
25 20 24 syl AWalksGBAAB
26 25 a1d AWalksGBB0=BAAAB
27 26 3imp AWalksGBB0=BAAAB
28 wlklenvp1 DWalksGEE=D+1
29 nnre DD
30 29 lep1d DDD+1
31 breq2 E=D+1DEDD+1
32 30 31 syl5ibr E=D+1DDE
33 28 32 syl DWalksGEDDE
34 33 a1d DWalksGEE0=EDDDE
35 34 3imp DWalksGEE0=EDDDE
36 27 35 anim12i AWalksGBB0=BAADWalksGEE0=EDDABDE
37 14 19 36 3jca AWalksGBB0=BAADWalksGEE0=EDDBWordVtxGEWordVtxGA0D0ABDE
38 pfxeq BWordVtxGEWordVtxGA0D0ABDEBprefixA=EprefixDA=Di0..^ABi=Ei
39 8 37 38 3syl UCWCBprefixA=EprefixDA=Di0..^ABi=Ei
40 39 biimp3a UCWCBprefixA=EprefixDA=Di0..^ABi=Ei