Metamath Proof Explorer

Theorem isupwlk

Description: Properties of a pair of functions to be a simple walk. (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 28-Dec-2020)

Ref Expression
Hypotheses upwlksfval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
upwlksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion isupwlk ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 upwlksfval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 upwlksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 df-br ⊢ ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ ( UPWalks ‘ 𝐺 ) )
4 1 2 upwlksfval ⊢ ( 𝐺 ∈ 𝑊 → ( UPWalks ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } )
5 4 3ad2ant1 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( UPWalks ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } )
6 5 eleq2d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( ⟨ 𝐹 , 𝑃 ⟩ ∈ ( UPWalks ‘ 𝐺 ) ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } ) )
7 3 6 bitrid ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } ) )
8 eleq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ Word dom 𝐼 ↔ 𝐹 ∈ Word dom 𝐼 ) )
9 8 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑓 ∈ Word dom 𝐼 ↔ 𝐹 ∈ Word dom 𝐼 ) )
10 simpr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → 𝑝 = 𝑃 )
11 fveq2 ⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) )
12 11 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 0 ... ( ♯ ‘ 𝑓 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
13 12 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 0 ... ( ♯ ‘ 𝑓 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
14 10 13 feq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
15 11 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
16 15 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
17 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
18 17 fveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
19 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) )
20 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
21 19 20 preq12d ⊢ ( 𝑝 = 𝑃 → { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
22 18 21 eqeqan12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
23 16 22 raleqbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ↔ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
24 9 14 23 3anbi123d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
25 24 opelopabga ⊢ ( ( 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( ⟨ 𝐹 , 𝑃 ⟩ ∈ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
26 25 3adant1 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( ⟨ 𝐹 , 𝑃 ⟩ ∈ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
27 7 26 bitrd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )