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 ∈ USHGraph ∧ H ∈ USHGraph → ∃ p ∃ f f Cycles ⁡ G p ∧ f = N ∧ ¬ ∃ p ∃ f f Cycles ⁡ H p ∧ f = N → ¬ G ≃ 𝑔𝑟 H

Proof

Step Hyp Ref Expression
1 brgric ⊢ G ≃ 𝑔𝑟 H ↔ G GraphIso H ≠ ∅
2 n0rex ⊢ G GraphIso H ≠ ∅ → ∃ i ∈ G GraphIso H i ∈ G GraphIso H
3 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
4 eqid ⊢ iEdg ⁡ H = iEdg ⁡ H
5 simprll ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → G ∈ USHGraph
6 simprlr ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → H ∈ USHGraph
7 simpl ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → i ∈ 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 -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ j
11 10 cbvmptv ⊢ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = j ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ j
12 cycliswlk ⊢ f Cycles ⁡ G p → f Walks ⁡ G p
13 12 ad2antrl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → f Walks ⁡ G p
14 13 adantl ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → f Walks ⁡ G p
15 3 4 5 6 7 11 14 upgrimwlklen ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Walks ⁡ H i ∘ p ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = f
16 simprrl ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → f Cycles ⁡ G p
17 3 4 5 6 7 11 16 upgrimcycls ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Cycles ⁡ H i ∘ p
18 simp3 ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Walks ⁡ H i ∘ p ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = f ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Cycles ⁡ H i ∘ p → x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Cycles ⁡ H i ∘ p
19 simp2r ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Walks ⁡ H i ∘ p ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = f ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Cycles ⁡ H i ∘ p → x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = f
20 simprrr ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → f = N
21 20 3ad2ant1 ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Walks ⁡ H i ∘ p ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = f ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Cycles ⁡ H i ∘ p → f = N
22 19 21 eqtrd ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Walks ⁡ H i ∘ p ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = f ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Cycles ⁡ H i ∘ p → x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = N
23 vex ⊢ i ∈ V
24 vex ⊢ p ∈ V
25 23 24 coex ⊢ i ∘ p ∈ V
26 vex ⊢ f ∈ V
27 26 dmex ⊢ dom ⁡ f ∈ V
28 27 mptex ⊢ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x ∈ V
29 breq12 ⊢ g = x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x ∧ q = i ∘ p → g Cycles ⁡ H q ↔ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Cycles ⁡ H i ∘ p
30 29 ancoms ⊢ q = i ∘ p ∧ g = x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x → g Cycles ⁡ H q ↔ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Cycles ⁡ H i ∘ p
31 fveqeq2 ⊢ g = x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x → g = N ↔ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = N
32 31 adantl ⊢ q = i ∘ p ∧ g = x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x → g = N ↔ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = N
33 30 32 anbi12d ⊢ q = i ∘ p ∧ g = x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x → g Cycles ⁡ H q ∧ g = N ↔ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Cycles ⁡ H i ∘ p ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = N
34 25 28 33 spc2ev ⊢ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Cycles ⁡ H i ∘ p ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = N → ∃ q ∃ g g Cycles ⁡ H q ∧ g = N
35 18 22 34 syl2anc ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Walks ⁡ H i ∘ p ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x = f ∧ x ∈ dom ⁡ f ⟼ iEdg ⁡ H -1 ⁡ i iEdg ⁡ G ⁡ f ⁡ x Cycles ⁡ H i ∘ p → ∃ q ∃ g g Cycles ⁡ H q ∧ g = N
36 15 17 35 mpd3an23 ⊢ i ∈ G GraphIso H ∧ G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → ∃ q ∃ g g Cycles ⁡ H q ∧ g = N
37 36 ex ⊢ i ∈ G GraphIso H → G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → ∃ q ∃ g g Cycles ⁡ H q ∧ g = N
38 37 rexlimivw ⊢ ∃ i ∈ G GraphIso H i ∈ G GraphIso H → G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → ∃ q ∃ g g Cycles ⁡ H q ∧ g = N
39 2 38 syl ⊢ G GraphIso H ≠ ∅ → G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → ∃ q ∃ g g Cycles ⁡ H q ∧ g = N
40 1 39 sylbi ⊢ G ≃ 𝑔𝑟 H → G ∈ USHGraph ∧ H ∈ USHGraph ∧ f Cycles ⁡ G p ∧ f = N → ∃ q ∃ g g Cycles ⁡ H q ∧ g = N
41 40 expdcom ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → f Cycles ⁡ G p ∧ f = N → G ≃ 𝑔𝑟 H → ∃ q ∃ g g Cycles ⁡ H q ∧ g = N
42 41 exlimdvv ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → ∃ p ∃ f f Cycles ⁡ G p ∧ f = N → G ≃ 𝑔𝑟 H → ∃ q ∃ g g Cycles ⁡ H q ∧ g = N
43 42 imp ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ ∃ p ∃ f f Cycles ⁡ G p ∧ f = N → G ≃ 𝑔𝑟 H → ∃ q ∃ 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 ⊢ ∃ p ∃ f f Cycles ⁡ H p ∧ f = N ↔ ∃ q ∃ g g Cycles ⁡ H q ∧ g = N
50 43 49 imbitrrdi ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ ∃ p ∃ f f Cycles ⁡ G p ∧ f = N → G ≃ 𝑔𝑟 H → ∃ p ∃ f f Cycles ⁡ H p ∧ f = N
51 50 con3d ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ ∃ p ∃ f f Cycles ⁡ G p ∧ f = N → ¬ ∃ p ∃ f f Cycles ⁡ H p ∧ f = N → ¬ G ≃ 𝑔𝑟 H
52 51 expimpd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → ∃ p ∃ f f Cycles ⁡ G p ∧ f = N ∧ ¬ ∃ p ∃ f f Cycles ⁡ H p ∧ f = N → ¬ G ≃ 𝑔𝑟 H