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

Metamath Proof Explorer

Theorem ntrl2v2e

Description: A walk which is not a trail: In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk, see wlk2v2e , but not a trail. Notice that G is a simple graph (without loops) only if X =/= Y . (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 8-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Hypotheses wlk2v2e.i ⊢ I = ⟨“ X Y ”⟩
wlk2v2e.f ⊢ F = ⟨“ 0 0 ”⟩
wlk2v2e.x ⊢ X ∈ V
wlk2v2e.y ⊢ Y ∈ V
wlk2v2e.p ⊢ P = ⟨“ XYX ”⟩
wlk2v2e.g ⊢ G = X Y I
Assertion ntrl2v2e ⊢ ¬ F Trails ⁡ G P

Proof

Step Hyp Ref Expression
1 wlk2v2e.i ⊢ I = ⟨“ X Y ”⟩
2 wlk2v2e.f ⊢ F = ⟨“ 0 0 ”⟩
3 wlk2v2e.x ⊢ X ∈ V
4 wlk2v2e.y ⊢ Y ∈ V
5 wlk2v2e.p ⊢ P = ⟨“ XYX ”⟩
6 wlk2v2e.g ⊢ G = X Y I
7 0z ⊢ 0 ∈ ℤ
8 1z ⊢ 1 ∈ ℤ
9 7 8 7 3pm3.2i ⊢ 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 0 ∈ ℤ
10 0ne1 ⊢ 0 ≠ 1
11 s2prop ⊢ 0 ∈ ℤ ∧ 0 ∈ ℤ → ⟨“ 0 0 ”⟩ = 0 0 1 0
12 7 7 11 mp2an ⊢ ⟨“ 0 0 ”⟩ = 0 0 1 0
13 2 12 eqtri ⊢ F = 0 0 1 0
14 13 fpropnf1 ⊢ 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 0 ≠ 1 → Fun ⁡ F ∧ ¬ Fun ⁡ F -1
15 9 10 14 mp2an ⊢ Fun ⁡ F ∧ ¬ Fun ⁡ F -1
16 15 simpri ⊢ ¬ Fun ⁡ F -1
17 16 intnan ⊢ ¬ F Walks ⁡ G P ∧ Fun ⁡ F -1
18 istrl ⊢ F Trails ⁡ G P ↔ F Walks ⁡ G P ∧ Fun ⁡ F -1
19 17 18 mtbir ⊢ ¬ F Trails ⁡ G P