Metamath Proof Explorer

Theorem cycldlenngric

Description: Two simple pseudographs are not isomorphic if one has a cycle and the other has no cycle of the same length. (Contributed by AV, 6-Nov-2025)

Ref Expression
Assertion cycldlenngric 
|- ( ( G e. USPGraph /\ H e. USPGraph ) -> ( ( E. p E. f ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) /\ -. E. p E. f ( f ( Cycles ` H ) p /\ ( # ` f ) = N ) ) -> -. G ~=gr H ) )

Proof

Step Hyp Ref Expression
1 brgric 
 |-  ( G ~=gr H <-> ( G GraphIso H ) =/= (/) )
2 n0rex 
 |-  ( ( G GraphIso H ) =/= (/) -> E. i e. ( G GraphIso H ) i e. ( G GraphIso H ) )
3 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
4 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
5 simprll 
 |-  ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) -> G e. USPGraph )
6 simprlr 
 |-  ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) -> H e. USPGraph )
7 simpl 
 |-  ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) -> i e. ( G GraphIso H ) )
8 2fveq3 
 |-  ( x = j -> ( ( iEdg ` G ) ` ( f ` x ) ) = ( ( iEdg ` G ) ` ( f ` j ) ) )
9 8 imaeq2d 
 |-  ( x = j -> ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) = ( i " ( ( iEdg ` G ) ` ( f ` j ) ) ) )
10 9 fveq2d 
 |-  ( x = j -> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) = ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` j ) ) ) ) )
11 10 cbvmptv 
 |-  ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) = ( j e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` j ) ) ) ) )
12 cycliswlk 
 |-  ( f ( Cycles ` G ) p -> f ( Walks ` G ) p )
13 12 ad2antrl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) -> f ( Walks ` G ) p )
14 13 adantl 
 |-  ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) -> f ( Walks ` G ) p )
15 3 4 5 6 7 11 14 upgrimwlklen 
 |-  ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) -> ( ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Walks ` H ) ( i o. p ) /\ ( # ` ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) = ( # ` f ) ) )
16 simprrl 
 |-  ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) -> f ( Cycles ` G ) p )
17 3 4 5 6 7 11 16 upgrimcycls 
 |-  ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) -> ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Cycles ` H ) ( i o. p ) )
18 simp3 
 |-  ( ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) /\ ( ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Walks ` H ) ( i o. p ) /\ ( # ` ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) = ( # ` f ) ) /\ ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Cycles ` H ) ( i o. p ) ) -> ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Cycles ` H ) ( i o. p ) )
19 simp2r 
 |-  ( ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) /\ ( ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Walks ` H ) ( i o. p ) /\ ( # ` ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) = ( # ` f ) ) /\ ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Cycles ` H ) ( i o. p ) ) -> ( # ` ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) = ( # ` f ) )
20 simprrr 
 |-  ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) -> ( # ` f ) = N )
21 20 3ad2ant1 
 |-  ( ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) /\ ( ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Walks ` H ) ( i o. p ) /\ ( # ` ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) = ( # ` f ) ) /\ ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Cycles ` H ) ( i o. p ) ) -> ( # ` f ) = N )
22 19 21 eqtrd 
 |-  ( ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) /\ ( ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Walks ` H ) ( i o. p ) /\ ( # ` ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) = ( # ` f ) ) /\ ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Cycles ` H ) ( i o. p ) ) -> ( # ` ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) = N )
23 vex 
 |-  i e. _V
24 vex 
 |-  p e. _V
25 23 24 coex 
 |-  ( i o. p ) e. _V
26 vex 
 |-  f e. _V
27 26 dmex 
 |-  dom f e. _V
28 27 mptex 
 |-  ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) e. _V
29 breq12 
 |-  ( ( g = ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) /\ q = ( i o. p ) ) -> ( g ( Cycles ` H ) q <-> ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Cycles ` H ) ( i o. p ) ) )
30 29 ancoms 
 |-  ( ( q = ( i o. p ) /\ g = ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) -> ( g ( Cycles ` H ) q <-> ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Cycles ` H ) ( i o. p ) ) )
31 fveqeq2 
 |-  ( g = ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) -> ( ( # ` g ) = N <-> ( # ` ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) = N ) )
32 31 adantl 
 |-  ( ( q = ( i o. p ) /\ g = ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) -> ( ( # ` g ) = N <-> ( # ` ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) = N ) )
33 30 32 anbi12d 
 |-  ( ( q = ( i o. p ) /\ g = ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) -> ( ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) <-> ( ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Cycles ` H ) ( i o. p ) /\ ( # ` ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) = N ) ) )
34 25 28 33 spc2ev 
 |-  ( ( ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Cycles ` H ) ( i o. p ) /\ ( # ` ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) = N ) -> E. q E. g ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) )
35 18 22 34 syl2anc 
 |-  ( ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) /\ ( ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Walks ` H ) ( i o. p ) /\ ( # ` ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ) = ( # ` f ) ) /\ ( x e. dom f |-> ( `' ( iEdg ` H ) ` ( i " ( ( iEdg ` G ) ` ( f ` x ) ) ) ) ) ( Cycles ` H ) ( i o. p ) ) -> E. q E. g ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) )
36 15 17 35 mpd3an23 
 |-  ( ( i e. ( G GraphIso H ) /\ ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) ) -> E. q E. g ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) )
37 36 ex 
 |-  ( i e. ( G GraphIso H ) -> ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) -> E. q E. g ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) ) )
38 37 rexlimivw 
 |-  ( E. i e. ( G GraphIso H ) i e. ( G GraphIso H ) -> ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) -> E. q E. g ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) ) )
39 2 38 syl 
 |-  ( ( G GraphIso H ) =/= (/) -> ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) -> E. q E. g ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) ) )
40 1 39 sylbi 
 |-  ( G ~=gr H -> ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) -> E. q E. g ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) ) )
41 40 expdcom 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) -> ( G ~=gr H -> E. q E. g ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) ) ) )
42 41 exlimdvv 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( E. p E. f ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) -> ( G ~=gr H -> E. q E. g ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) ) ) )
43 42 imp 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ E. p E. f ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) -> ( G ~=gr H -> E. q E. g ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) ) )
44 breq12 
 |-  ( ( f = g /\ p = q ) -> ( f ( Cycles ` H ) p <-> g ( Cycles ` H ) q ) )
45 44 ancoms 
 |-  ( ( p = q /\ f = g ) -> ( f ( Cycles ` H ) p <-> g ( Cycles ` H ) q ) )
46 fveqeq2 
 |-  ( f = g -> ( ( # ` f ) = N <-> ( # ` g ) = N ) )
47 46 adantl 
 |-  ( ( p = q /\ f = g ) -> ( ( # ` f ) = N <-> ( # ` g ) = N ) )
48 45 47 anbi12d 
 |-  ( ( p = q /\ f = g ) -> ( ( f ( Cycles ` H ) p /\ ( # ` f ) = N ) <-> ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) ) )
49 48 cbvex2vw 
 |-  ( E. p E. f ( f ( Cycles ` H ) p /\ ( # ` f ) = N ) <-> E. q E. g ( g ( Cycles ` H ) q /\ ( # ` g ) = N ) )
50 43 49 imbitrrdi 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ E. p E. f ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) -> ( G ~=gr H -> E. p E. f ( f ( Cycles ` H ) p /\ ( # ` f ) = N ) ) )
51 50 con3d 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ E. p E. f ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) ) -> ( -. E. p E. f ( f ( Cycles ` H ) p /\ ( # ` f ) = N ) -> -. G ~=gr H ) )
52 51 expimpd 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( ( E. p E. f ( f ( Cycles ` G ) p /\ ( # ` f ) = N ) /\ -. E. p E. f ( f ( Cycles ` H ) p /\ ( # ` f ) = N ) ) -> -. G ~=gr H ) )