Metamath Proof Explorer

Theorem wwlksnon

Description: The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 11-May-2021)

Ref Expression
Hypothesis wwlksnon.v ⊢V=Vtx⁡G
Assertion wwlksnon ⊢N∈ℕ0∧G∈U→NWWalksNOnG=a∈V,b∈V⟼w∈NWWalksNG|w⁡0=a∧w⁡N=b

Proof

Step Hyp Ref Expression
1 wwlksnon.v ⊢V=Vtx⁡G
2 df-wwlksnon ⊢WWalksNOn=n∈ℕ0,g∈V⟼a∈Vtx⁡g,b∈Vtx⁡g⟼w∈nWWalksNg|w⁡0=a∧w⁡n=b
3 2 a1i ⊢N∈ℕ0∧G∈U→WWalksNOn=n∈ℕ0,g∈V⟼a∈Vtx⁡g,b∈Vtx⁡g⟼w∈nWWalksNg|w⁡0=a∧w⁡n=b
4 fveq2 ⊢g=G→Vtx⁡g=Vtx⁡G
5 4 1 eqtr4di ⊢g=G→Vtx⁡g=V
6 5 adantl ⊢n=N∧g=G→Vtx⁡g=V
7 oveq12 ⊢n=N∧g=G→nWWalksNg=NWWalksNG
8 fveqeq2 ⊢n=N→w⁡n=b↔w⁡N=b
9 8 anbi2d ⊢n=N→w⁡0=a∧w⁡n=b↔w⁡0=a∧w⁡N=b
10 9 adantr ⊢n=N∧g=G→w⁡0=a∧w⁡n=b↔w⁡0=a∧w⁡N=b
11 7 10 rabeqbidv ⊢n=N∧g=G→w∈nWWalksNg|w⁡0=a∧w⁡n=b=w∈NWWalksNG|w⁡0=a∧w⁡N=b
12 6 6 11 mpoeq123dv ⊢n=N∧g=G→a∈Vtx⁡g,b∈Vtx⁡g⟼w∈nWWalksNg|w⁡0=a∧w⁡n=b=a∈V,b∈V⟼w∈NWWalksNG|w⁡0=a∧w⁡N=b
13 12 adantl ⊢N∈ℕ0∧G∈U∧n=N∧g=G→a∈Vtx⁡g,b∈Vtx⁡g⟼w∈nWWalksNg|w⁡0=a∧w⁡n=b=a∈V,b∈V⟼w∈NWWalksNG|w⁡0=a∧w⁡N=b
14 simpl ⊢N∈ℕ0∧G∈U→N∈ℕ0
15 elex ⊢G∈U→G∈V
16 15 adantl ⊢N∈ℕ0∧G∈U→G∈V
17 1 fvexi ⊢V∈V
18 17 17 mpoex ⊢a∈V,b∈V⟼w∈NWWalksNG|w⁡0=a∧w⁡N=b∈V
19 18 a1i ⊢N∈ℕ0∧G∈U→a∈V,b∈V⟼w∈NWWalksNG|w⁡0=a∧w⁡N=b∈V
20 3 13 14 16 19 ovmpod ⊢N∈ℕ0∧G∈U→NWWalksNOnG=a∈V,b∈V⟼w∈NWWalksNG|w⁡0=a∧w⁡N=b