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

Metamath Proof Explorer

Theorem lp1cycl

Description: A loop (which is an edge at index J ) induces a cycle of length 1 in a hypergraph. (Contributed by AV, 2-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Hypothesis lppthon.i ⊢ I = iEdg ⁡ G
Assertion lp1cycl ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → ⟨“ J ”⟩ Cycles ⁡ G ⟨“ AA ”⟩

Proof

Step Hyp Ref Expression
1 lppthon.i ⊢ I = iEdg ⁡ G
2 1 lppthon ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → ⟨“ J ”⟩ A PathsOn ⁡ G A ⟨“ AA ”⟩
3 pthonispth ⊢ ⟨“ J ”⟩ A PathsOn ⁡ G A ⟨“ AA ”⟩ → ⟨“ J ”⟩ Paths ⁡ G ⟨“ AA ”⟩
4 2 3 syl ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → ⟨“ J ”⟩ Paths ⁡ G ⟨“ AA ”⟩
5 1 lpvtx ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → A ∈ Vtx ⁡ G
6 s2fv1 ⊢ A ∈ Vtx ⁡ G → ⟨“ AA ”⟩ ⁡ 1 = A
7 s1len ⊢ ⟨“ J ”⟩ = 1
8 7 fveq2i ⊢ ⟨“ AA ”⟩ ⁡ ⟨“ J ”⟩ = ⟨“ AA ”⟩ ⁡ 1
9 8 a1i ⊢ A ∈ Vtx ⁡ G → ⟨“ AA ”⟩ ⁡ ⟨“ J ”⟩ = ⟨“ AA ”⟩ ⁡ 1
10 s2fv0 ⊢ A ∈ Vtx ⁡ G → ⟨“ AA ”⟩ ⁡ 0 = A
11 6 9 10 3eqtr4rd ⊢ A ∈ Vtx ⁡ G → ⟨“ AA ”⟩ ⁡ 0 = ⟨“ AA ”⟩ ⁡ ⟨“ J ”⟩
12 5 11 syl ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → ⟨“ AA ”⟩ ⁡ 0 = ⟨“ AA ”⟩ ⁡ ⟨“ J ”⟩
13 iscycl ⊢ ⟨“ J ”⟩ Cycles ⁡ G ⟨“ AA ”⟩ ↔ ⟨“ J ”⟩ Paths ⁡ G ⟨“ AA ”⟩ ∧ ⟨“ AA ”⟩ ⁡ 0 = ⟨“ AA ”⟩ ⁡ ⟨“ J ”⟩
14 4 12 13 sylanbrc ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → ⟨“ J ”⟩ Cycles ⁡ G ⟨“ AA ”⟩