Metamath Proof Explorer


Theorem upwlkwlk

Description: A simple walk is a walk. (Contributed by AV, 30-Dec-2020) (Proof shortened by AV, 27-Feb-2021)

Ref Expression
Assertion upwlkwlk ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃𝐹 ( Walks ‘ 𝐺 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 1 2 upwlkbprop ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
4 idd ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) )
5 idd ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
6 ifpprsnss ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) )
7 6 a1i ( ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) )
8 7 ralimdva ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) )
9 4 5 8 3anim123d ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) ) )
10 1 2 isupwlk ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
11 1 2 iswlk ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) ) )
12 9 10 11 3imtr4d ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) )
13 3 12 mpcom ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃𝐹 ( Walks ‘ 𝐺 ) 𝑃 )