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

Metamath Proof Explorer

Theorem upgrewlkle2

Description: In a pseudograph, there is no s-walk of edges of length greater than 1 with s>2. (Contributed by AV, 4-Jan-2021)

Ref Expression
Assertion upgrewlkle2 
|- ( ( G e. UPGraph /\ F e. ( G EdgWalks S ) /\ 1 < ( # ` F ) ) -> S <_ 2 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
2 1 ewlkprop 
 |-  ( F e. ( G EdgWalks S ) -> ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
3 fvex 
 |-  ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) e. _V
4 hashin 
 |-  ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) e. _V -> ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) )
5 3 4 ax-mp 
 |-  ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) )
6 simpl3 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) /\ k e. ( 1 ..^ ( # ` F ) ) ) -> G e. UPGraph )
7 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
8 1 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
9 7 8 syl 
 |-  ( G e. UPGraph -> Fun ( iEdg ` G ) )
10 9 funfnd 
 |-  ( G e. UPGraph -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
11 10 3ad2ant3 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
12 11 adantr 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) /\ k e. ( 1 ..^ ( # ` F ) ) ) -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
13 elfzofz 
 |-  ( k e. ( 1 ..^ ( # ` F ) ) -> k e. ( 1 ... ( # ` F ) ) )
14 fz1fzo0m1 
 |-  ( k e. ( 1 ... ( # ` F ) ) -> ( k - 1 ) e. ( 0 ..^ ( # ` F ) ) )
15 13 14 syl 
 |-  ( k e. ( 1 ..^ ( # ` F ) ) -> ( k - 1 ) e. ( 0 ..^ ( # ` F ) ) )
16 wrdsymbcl 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ ( k - 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` ( k - 1 ) ) e. dom ( iEdg ` G ) )
17 15 16 sylan2 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ k e. ( 1 ..^ ( # ` F ) ) ) -> ( F ` ( k - 1 ) ) e. dom ( iEdg ` G ) )
18 17 3ad2antl2 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) /\ k e. ( 1 ..^ ( # ` F ) ) ) -> ( F ` ( k - 1 ) ) e. dom ( iEdg ` G ) )
19 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
20 19 1 upgrle 
 |-  ( ( G e. UPGraph /\ ( iEdg ` G ) Fn dom ( iEdg ` G ) /\ ( F ` ( k - 1 ) ) e. dom ( iEdg ` G ) ) -> ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) <_ 2 )
21 6 12 18 20 syl3anc 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) /\ k e. ( 1 ..^ ( # ` F ) ) ) -> ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) <_ 2 )
22 3 inex1 
 |-  ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) e. _V
23 hashxrcl 
 |-  ( ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) e. _V -> ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) e. RR* )
24 22 23 ax-mp 
 |-  ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) e. RR*
25 hashxrcl 
 |-  ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) e. _V -> ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) e. RR* )
26 3 25 ax-mp 
 |-  ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) e. RR*
27 2re 
 |-  2 e. RR
28 27 rexri 
 |-  2 e. RR*
29 24 26 28 3pm3.2i 
 |-  ( ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) e. RR* /\ ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) e. RR* /\ 2 e. RR* )
30 29 a1i 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) /\ k e. ( 1 ..^ ( # ` F ) ) ) -> ( ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) e. RR* /\ ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) e. RR* /\ 2 e. RR* ) )
31 xrletr 
 |-  ( ( ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) e. RR* /\ ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) e. RR* /\ 2 e. RR* ) -> ( ( ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) /\ ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) <_ 2 ) -> ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ 2 ) )
32 30 31 syl 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) /\ k e. ( 1 ..^ ( # ` F ) ) ) -> ( ( ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) /\ ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) <_ 2 ) -> ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ 2 ) )
33 21 32 mpan2d 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) /\ k e. ( 1 ..^ ( # ` F ) ) ) -> ( ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ ( # ` ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) ) -> ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ 2 ) )
34 5 33 mpi 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) /\ k e. ( 1 ..^ ( # ` F ) ) ) -> ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ 2 )
35 xnn0xr 
 |-  ( S e. NN0* -> S e. RR* )
36 24 a1i 
 |-  ( S e. NN0* -> ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) e. RR* )
37 28 a1i 
 |-  ( S e. NN0* -> 2 e. RR* )
38 xrletr 
 |-  ( ( S e. RR* /\ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) e. RR* /\ 2 e. RR* ) -> ( ( S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) /\ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ 2 ) -> S <_ 2 ) )
39 35 36 37 38 syl3anc 
 |-  ( S e. NN0* -> ( ( S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) /\ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ 2 ) -> S <_ 2 ) )
40 39 expcomd 
 |-  ( S e. NN0* -> ( ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ 2 -> ( S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> S <_ 2 ) ) )
41 40 adantl 
 |-  ( ( G e. _V /\ S e. NN0* ) -> ( ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ 2 -> ( S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> S <_ 2 ) ) )
42 41 3ad2ant1 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) -> ( ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ 2 -> ( S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> S <_ 2 ) ) )
43 42 adantr 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) /\ k e. ( 1 ..^ ( # ` F ) ) ) -> ( ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <_ 2 -> ( S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> S <_ 2 ) ) )
44 34 43 mpd 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) /\ k e. ( 1 ..^ ( # ` F ) ) ) -> ( S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> S <_ 2 ) )
45 44 ralimdva 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) -> ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> A. k e. ( 1 ..^ ( # ` F ) ) S <_ 2 ) )
46 45 3exp 
 |-  ( ( G e. _V /\ S e. NN0* ) -> ( F e. Word dom ( iEdg ` G ) -> ( G e. UPGraph -> ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> A. k e. ( 1 ..^ ( # ` F ) ) S <_ 2 ) ) ) )
47 46 com34 
 |-  ( ( G e. _V /\ S e. NN0* ) -> ( F e. Word dom ( iEdg ` G ) -> ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( G e. UPGraph -> A. k e. ( 1 ..^ ( # ` F ) ) S <_ 2 ) ) ) )
48 47 3imp 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) -> ( G e. UPGraph -> A. k e. ( 1 ..^ ( # ` F ) ) S <_ 2 ) )
49 lencl 
 |-  ( F e. Word dom ( iEdg ` G ) -> ( # ` F ) e. NN0 )
50 1zzd 
 |-  ( ( # ` F ) e. NN0 -> 1 e. ZZ )
51 nn0z 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. ZZ )
52 fzon 
 |-  ( ( 1 e. ZZ /\ ( # ` F ) e. ZZ ) -> ( ( # ` F ) <_ 1 <-> ( 1 ..^ ( # ` F ) ) = (/) ) )
53 50 51 52 syl2anc 
 |-  ( ( # ` F ) e. NN0 -> ( ( # ` F ) <_ 1 <-> ( 1 ..^ ( # ` F ) ) = (/) ) )
54 nn0re 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. RR )
55 1red 
 |-  ( ( # ` F ) e. NN0 -> 1 e. RR )
56 54 55 lenltd 
 |-  ( ( # ` F ) e. NN0 -> ( ( # ` F ) <_ 1 <-> -. 1 < ( # ` F ) ) )
57 53 56 bitr3d 
 |-  ( ( # ` F ) e. NN0 -> ( ( 1 ..^ ( # ` F ) ) = (/) <-> -. 1 < ( # ` F ) ) )
58 57 biimpd 
 |-  ( ( # ` F ) e. NN0 -> ( ( 1 ..^ ( # ` F ) ) = (/) -> -. 1 < ( # ` F ) ) )
59 58 necon2ad 
 |-  ( ( # ` F ) e. NN0 -> ( 1 < ( # ` F ) -> ( 1 ..^ ( # ` F ) ) =/= (/) ) )
60 rspn0 
 |-  ( ( 1 ..^ ( # ` F ) ) =/= (/) -> ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ 2 -> S <_ 2 ) )
61 59 60 syl6com 
 |-  ( 1 < ( # ` F ) -> ( ( # ` F ) e. NN0 -> ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ 2 -> S <_ 2 ) ) )
62 61 com3l 
 |-  ( ( # ` F ) e. NN0 -> ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ 2 -> ( 1 < ( # ` F ) -> S <_ 2 ) ) )
63 49 62 syl 
 |-  ( F e. Word dom ( iEdg ` G ) -> ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ 2 -> ( 1 < ( # ` F ) -> S <_ 2 ) ) )
64 63 3ad2ant2 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) -> ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ 2 -> ( 1 < ( # ` F ) -> S <_ 2 ) ) )
65 48 64 syld 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) -> ( G e. UPGraph -> ( 1 < ( # ` F ) -> S <_ 2 ) ) )
66 2 65 syl 
 |-  ( F e. ( G EdgWalks S ) -> ( G e. UPGraph -> ( 1 < ( # ` F ) -> S <_ 2 ) ) )
67 66 3imp21 
 |-  ( ( G e. UPGraph /\ F e. ( G EdgWalks S ) /\ 1 < ( # ` F ) ) -> S <_ 2 )