Metamath Proof Explorer

Theorem hashwwlksnext

Description: Number of walks (as words) extended by an edge as a sum over the prefixes. (Contributed by Alexander van der Vekens, 21-Aug-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Hypotheses wwlksnextprop.x ⊢X=N+1WWalksNG
wwlksnextprop.e ⊢E=Edg⁡G
wwlksnextprop.y ⊢Y=w∈NWWalksNG|w⁡0=P
Assertion hashwwlksnext ⊢Vtx⁡G∈Fin→x∈X|∃y∈YxprefixM=y∧y⁡0=P∧lastS⁡ylastS⁡x∈E=∑y∈Yx∈X|xprefixM=y∧y⁡0=P∧lastS⁡ylastS⁡x∈E

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x ⊢X=N+1WWalksNG
2 wwlksnextprop.e ⊢E=Edg⁡G
3 wwlksnextprop.y ⊢Y=w∈NWWalksNG|w⁡0=P
4 wwlksnfi ⊢Vtx⁡G∈Fin→NWWalksNG∈Fin
5 ssrab2 ⊢w∈NWWalksNG|w⁡0=P⊆NWWalksNG
6 ssfi ⊢NWWalksNG∈Fin∧w∈NWWalksNG|w⁡0=P⊆NWWalksNG→w∈NWWalksNG|w⁡0=P∈Fin
7 4 5 6 sylancl ⊢Vtx⁡G∈Fin→w∈NWWalksNG|w⁡0=P∈Fin
8 3 7 eqeltrid ⊢Vtx⁡G∈Fin→Y∈Fin
9 wwlksnfi ⊢Vtx⁡G∈Fin→N+1WWalksNG∈Fin
10 1 9 eqeltrid ⊢Vtx⁡G∈Fin→X∈Fin
11 rabfi ⊢X∈Fin→x∈X|xprefixM=y∧y⁡0=P∧lastS⁡ylastS⁡x∈E∈Fin
12 10 11 syl ⊢Vtx⁡G∈Fin→x∈X|xprefixM=y∧y⁡0=P∧lastS⁡ylastS⁡x∈E∈Fin
13 12 adantr ⊢Vtx⁡G∈Fin∧y∈Y→x∈X|xprefixM=y∧y⁡0=P∧lastS⁡ylastS⁡x∈E∈Fin
14 1 2 3 disjxwwlkn ⊢Disjy∈Yx∈X|xprefixM=y∧y⁡0=P∧lastS⁡ylastS⁡x∈E
15 14 a1i ⊢Vtx⁡G∈Fin→Disjy∈Yx∈X|xprefixM=y∧y⁡0=P∧lastS⁡ylastS⁡x∈E
16 8 13 15 hashrabrex ⊢Vtx⁡G∈Fin→x∈X|∃y∈YxprefixM=y∧y⁡0=P∧lastS⁡ylastS⁡x∈E=∑y∈Yx∈X|xprefixM=y∧y⁡0=P∧lastS⁡ylastS⁡x∈E