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

Metamath Proof Explorer

Theorem usgr2trlncrct

Description: In a simple graph, any trail of length 2 is not a circuit. (Contributed by AV, 5-Jun-2021)

Ref Expression
Assertion usgr2trlncrct ⊢ G ∈ USGraph ∧ F = 2 → F Trails ⁡ G P → ¬ F Circuits ⁡ G P

Proof

Step Hyp Ref Expression
1 usgr2trlncl ⊢ G ∈ USGraph ∧ F = 2 → F Trails ⁡ G P → P ⁡ 0 ≠ P ⁡ 2
2 1 imp ⊢ G ∈ USGraph ∧ F = 2 ∧ F Trails ⁡ G P → P ⁡ 0 ≠ P ⁡ 2
3 crctprop ⊢ F Circuits ⁡ G P → F Trails ⁡ G P ∧ P ⁡ 0 = P ⁡ F
4 fveq2 ⊢ F = 2 → P ⁡ F = P ⁡ 2
5 4 eqeq2d ⊢ F = 2 → P ⁡ 0 = P ⁡ F ↔ P ⁡ 0 = P ⁡ 2
6 5 biimpcd ⊢ P ⁡ 0 = P ⁡ F → F = 2 → P ⁡ 0 = P ⁡ 2
7 3 6 simpl2im ⊢ F Circuits ⁡ G P → F = 2 → P ⁡ 0 = P ⁡ 2
8 7 com12 ⊢ F = 2 → F Circuits ⁡ G P → P ⁡ 0 = P ⁡ 2
9 8 ad2antlr ⊢ G ∈ USGraph ∧ F = 2 ∧ F Trails ⁡ G P → F Circuits ⁡ G P → P ⁡ 0 = P ⁡ 2
10 9 necon3ad ⊢ G ∈ USGraph ∧ F = 2 ∧ F Trails ⁡ G P → P ⁡ 0 ≠ P ⁡ 2 → ¬ F Circuits ⁡ G P
11 2 10 mpd ⊢ G ∈ USGraph ∧ F = 2 ∧ F Trails ⁡ G P → ¬ F Circuits ⁡ G P
12 11 ex ⊢ G ∈ USGraph ∧ F = 2 → F Trails ⁡ G P → ¬ F Circuits ⁡ G P