Metamath Proof Explorer


Theorem wlkp1lem3

Description: Lemma for wlkp1 . (Contributed by AV, 6-Mar-2021)

Ref Expression
Hypotheses wlkp1.v
|- V = ( Vtx ` G )
wlkp1.i
|- I = ( iEdg ` G )
wlkp1.f
|- ( ph -> Fun I )
wlkp1.a
|- ( ph -> I e. Fin )
wlkp1.b
|- ( ph -> B e. W )
wlkp1.c
|- ( ph -> C e. V )
wlkp1.d
|- ( ph -> -. B e. dom I )
wlkp1.w
|- ( ph -> F ( Walks ` G ) P )
wlkp1.n
|- N = ( # ` F )
wlkp1.e
|- ( ph -> E e. ( Edg ` G ) )
wlkp1.x
|- ( ph -> { ( P ` N ) , C } C_ E )
wlkp1.u
|- ( ph -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) )
wlkp1.h
|- H = ( F u. { <. N , B >. } )
Assertion wlkp1lem3
|- ( ph -> ( ( iEdg ` S ) ` ( H ` N ) ) = ( ( I u. { <. B , E >. } ) ` B ) )

Proof

Step Hyp Ref Expression
1 wlkp1.v
 |-  V = ( Vtx ` G )
2 wlkp1.i
 |-  I = ( iEdg ` G )
3 wlkp1.f
 |-  ( ph -> Fun I )
4 wlkp1.a
 |-  ( ph -> I e. Fin )
5 wlkp1.b
 |-  ( ph -> B e. W )
6 wlkp1.c
 |-  ( ph -> C e. V )
7 wlkp1.d
 |-  ( ph -> -. B e. dom I )
8 wlkp1.w
 |-  ( ph -> F ( Walks ` G ) P )
9 wlkp1.n
 |-  N = ( # ` F )
10 wlkp1.e
 |-  ( ph -> E e. ( Edg ` G ) )
11 wlkp1.x
 |-  ( ph -> { ( P ` N ) , C } C_ E )
12 wlkp1.u
 |-  ( ph -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) )
13 wlkp1.h
 |-  H = ( F u. { <. N , B >. } )
14 13 a1i
 |-  ( ph -> H = ( F u. { <. N , B >. } ) )
15 14 fveq1d
 |-  ( ph -> ( H ` N ) = ( ( F u. { <. N , B >. } ) ` N ) )
16 9 fvexi
 |-  N e. _V
17 2 wlkf
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
18 lencl
 |-  ( F e. Word dom I -> ( # ` F ) e. NN0 )
19 wrddm
 |-  ( F e. Word dom I -> dom F = ( 0 ..^ ( # ` F ) ) )
20 fzonel
 |-  -. ( # ` F ) e. ( 0 ..^ ( # ` F ) )
21 9 a1i
 |-  ( ( ( # ` F ) e. NN0 /\ dom F = ( 0 ..^ ( # ` F ) ) ) -> N = ( # ` F ) )
22 simpr
 |-  ( ( ( # ` F ) e. NN0 /\ dom F = ( 0 ..^ ( # ` F ) ) ) -> dom F = ( 0 ..^ ( # ` F ) ) )
23 21 22 eleq12d
 |-  ( ( ( # ` F ) e. NN0 /\ dom F = ( 0 ..^ ( # ` F ) ) ) -> ( N e. dom F <-> ( # ` F ) e. ( 0 ..^ ( # ` F ) ) ) )
24 20 23 mtbiri
 |-  ( ( ( # ` F ) e. NN0 /\ dom F = ( 0 ..^ ( # ` F ) ) ) -> -. N e. dom F )
25 18 19 24 syl2anc
 |-  ( F e. Word dom I -> -. N e. dom F )
26 8 17 25 3syl
 |-  ( ph -> -. N e. dom F )
27 fsnunfv
 |-  ( ( N e. _V /\ B e. W /\ -. N e. dom F ) -> ( ( F u. { <. N , B >. } ) ` N ) = B )
28 16 5 26 27 mp3an2i
 |-  ( ph -> ( ( F u. { <. N , B >. } ) ` N ) = B )
29 15 28 eqtrd
 |-  ( ph -> ( H ` N ) = B )
30 12 29 fveq12d
 |-  ( ph -> ( ( iEdg ` S ) ` ( H ` N ) ) = ( ( I u. { <. B , E >. } ) ` B ) )