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 + 1 WWalksN G
wwlksnextprop.e ⊢ E = Edg ⁡ G
wwlksnextprop.y ⊢ Y = w ∈ N WWalksN G | w ⁡ 0 = P
Assertion hashwwlksnext ⊢ Vtx ⁡ G ∈ Fin → x ∈ X | ∃ y ∈ Y x prefix M = y ∧ y ⁡ 0 = P ∧ lastS ⁡ y lastS ⁡ x ∈ E = ∑ y ∈ Y x ∈ X | x prefix M = y ∧ y ⁡ 0 = P ∧ lastS ⁡ y lastS ⁡ x ∈ E

Proof

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