This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ewlkprop

Description: Properties of an s-walk of edges. (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion ewlkprop ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ewlksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 df-ewlks ⊢ EdgWalks = ( 𝑔 ∈ V , 𝑠 ∈ ℕ0* ↦ { 𝑓 ∣ [ ( iEdg ‘ 𝑔 ) / 𝑖 ] ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } )
3 2 elmpocl ⊢ ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) )
4 simpr ⊢ ( ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ∧ ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ) → ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) )
5 1 isewlk ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
6 5 3expa ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
7 6 biimpd ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
8 7 expcom ⊢ ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) )
9 8 pm2.43a ⊢ ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) → ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
10 9 imp ⊢ ( ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ∧ ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ) → ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
11 3anass ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ↔ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
12 4 10 11 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ∧ ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ) → ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
13 3 12 mpdan ⊢ ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )