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

Metamath Proof Explorer

Theorem upgrimcycls

Description: Graph isomorphisms between simple pseudographs map cycles onto cycles. (Contributed by AV, 31-Oct-2025)

Ref Expression
Hypotheses upgrimwlk.i 
|- I = ( iEdg ` G )
upgrimwlk.j 
|- J = ( iEdg ` H )
upgrimwlk.g 
|- ( ph -> G e. USPGraph )
upgrimwlk.h 
|- ( ph -> H e. USPGraph )
upgrimwlk.n 
|- ( ph -> N e. ( G GraphIso H ) )
upgrimwlk.e 
|- E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) )
upgrimcycls.c 
|- ( ph -> F ( Cycles ` G ) P )
Assertion upgrimcycls 
|- ( ph -> E ( Cycles ` H ) ( N o. P ) )

Proof

Step Hyp Ref Expression
1 upgrimwlk.i 
 |-  I = ( iEdg ` G )
2 upgrimwlk.j 
 |-  J = ( iEdg ` H )
3 upgrimwlk.g 
 |-  ( ph -> G e. USPGraph )
4 upgrimwlk.h 
 |-  ( ph -> H e. USPGraph )
5 upgrimwlk.n 
 |-  ( ph -> N e. ( G GraphIso H ) )
6 upgrimwlk.e 
 |-  E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) )
7 upgrimcycls.c 
 |-  ( ph -> F ( Cycles ` G ) P )
8 cyclispth 
 |-  ( F ( Cycles ` G ) P -> F ( Paths ` G ) P )
9 7 8 syl 
 |-  ( ph -> F ( Paths ` G ) P )
10 1 2 3 4 5 6 9 upgrimpths 
 |-  ( ph -> E ( Paths ` H ) ( N o. P ) )
11 iscycl 
 |-  ( F ( Cycles ` G ) P <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
12 11 simprbi 
 |-  ( F ( Cycles ` G ) P -> ( P ` 0 ) = ( P ` ( # ` F ) ) )
13 7 12 syl 
 |-  ( ph -> ( P ` 0 ) = ( P ` ( # ` F ) ) )
14 13 fveq2d 
 |-  ( ph -> ( N ` ( P ` 0 ) ) = ( N ` ( P ` ( # ` F ) ) ) )
15 cycliswlk 
 |-  ( F ( Cycles ` G ) P -> F ( Walks ` G ) P )
16 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
17 16 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
18 7 15 17 3syl 
 |-  ( ph -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
19 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
20 7 15 19 3syl 
 |-  ( ph -> ( # ` F ) e. NN0 )
21 0elfz 
 |-  ( ( # ` F ) e. NN0 -> 0 e. ( 0 ... ( # ` F ) ) )
22 20 21 syl 
 |-  ( ph -> 0 e. ( 0 ... ( # ` F ) ) )
23 18 22 fvco3d 
 |-  ( ph -> ( ( N o. P ) ` 0 ) = ( N ` ( P ` 0 ) ) )
24 1 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
25 7 15 24 3syl 
 |-  ( ph -> F e. Word dom I )
26 1 2 3 4 5 6 25 upgrimwlklem1 
 |-  ( ph -> ( # ` E ) = ( # ` F ) )
27 26 fveq2d 
 |-  ( ph -> ( ( N o. P ) ` ( # ` E ) ) = ( ( N o. P ) ` ( # ` F ) ) )
28 nn0fz0 
 |-  ( ( # ` F ) e. NN0 <-> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
29 20 28 sylib 
 |-  ( ph -> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
30 18 29 fvco3d 
 |-  ( ph -> ( ( N o. P ) ` ( # ` F ) ) = ( N ` ( P ` ( # ` F ) ) ) )
31 27 30 eqtrd 
 |-  ( ph -> ( ( N o. P ) ` ( # ` E ) ) = ( N ` ( P ` ( # ` F ) ) ) )
32 14 23 31 3eqtr4d 
 |-  ( ph -> ( ( N o. P ) ` 0 ) = ( ( N o. P ) ` ( # ` E ) ) )
33 iscycl 
 |-  ( E ( Cycles ` H ) ( N o. P ) <-> ( E ( Paths ` H ) ( N o. P ) /\ ( ( N o. P ) ` 0 ) = ( ( N o. P ) ` ( # ` E ) ) ) )
34 10 32 33 sylanbrc 
 |-  ( ph -> E ( Cycles ` H ) ( N o. P ) )