Metamath Proof Explorer

Theorem umgr3cyclex

Description: If there are three (different) vertices in a multigraph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017) (Revised by AV, 12-Feb-2021)

Ref Expression
Hypotheses uhgr3cyclex.v ⊢ V = Vtx ⁡ G
uhgr3cyclex.e ⊢ E = Edg ⁡ G
Assertion umgr3cyclex ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A

Proof

Step Hyp Ref Expression
1 uhgr3cyclex.v ⊢ V = Vtx ⁡ G
2 uhgr3cyclex.e ⊢ E = Edg ⁡ G
3 umgruhgr ⊢ G ∈ UMGraph → G ∈ UHGraph
4 3 3ad2ant1 ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → G ∈ UHGraph
5 simp2 ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A ∈ V ∧ B ∈ V ∧ C ∈ V
6 2 umgredgne ⊢ G ∈ UMGraph ∧ A B ∈ E → A ≠ B
7 6 3ad2antr1 ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A ≠ B
8 prcom ⊢ C A = A C
9 8 eleq1i ⊢ C A ∈ E ↔ A C ∈ E
10 9 biimpi ⊢ C A ∈ E → A C ∈ E
11 10 3ad2ant3 ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A C ∈ E
12 2 umgredgne ⊢ G ∈ UMGraph ∧ A C ∈ E → A ≠ C
13 11 12 sylan2 ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A ≠ C
14 simp2 ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → B C ∈ E
15 2 umgredgne ⊢ G ∈ UMGraph ∧ B C ∈ E → B ≠ C
16 14 15 sylan2 ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → B ≠ C
17 7 13 16 3jca ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A ≠ B ∧ A ≠ C ∧ B ≠ C
18 17 3adant2 ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A ≠ B ∧ A ≠ C ∧ B ≠ C
19 simp3 ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
20 1 2 uhgr3cyclex ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
21 4 5 18 19 20 syl121anc ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A