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 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion lp1cycl ( ( 𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 } ) → ⟨“ 𝐽 ”⟩ ( Cycles ‘ 𝐺 ) ⟨“ 𝐴 𝐴 ”⟩ )

Proof

Step Hyp Ref Expression
1 lppthon.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 1 lppthon ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 } ) → ⟨“ 𝐽 ”⟩ ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐴 ) ⟨“ 𝐴 𝐴 ”⟩ )
3 pthonispth ⊢ ( ⟨“ 𝐽 ”⟩ ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐴 ) ⟨“ 𝐴 𝐴 ”⟩ → ⟨“ 𝐽 ”⟩ ( Paths ‘ 𝐺 ) ⟨“ 𝐴 𝐴 ”⟩ )
4 2 3 syl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 } ) → ⟨“ 𝐽 ”⟩ ( Paths ‘ 𝐺 ) ⟨“ 𝐴 𝐴 ”⟩ )
5 1 lpvtx ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 } ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
6 s2fv1 ⊢ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) → ( ⟨“ 𝐴 𝐴 ”⟩ ‘ 1 ) = 𝐴 )
7 s1len ⊢ ( ♯ ‘ ⟨“ 𝐽 ”⟩ ) = 1
8 7 fveq2i ⊢ ( ⟨“ 𝐴 𝐴 ”⟩ ‘ ( ♯ ‘ ⟨“ 𝐽 ”⟩ ) ) = ( ⟨“ 𝐴 𝐴 ”⟩ ‘ 1 )
9 8 a1i ⊢ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) → ( ⟨“ 𝐴 𝐴 ”⟩ ‘ ( ♯ ‘ ⟨“ 𝐽 ”⟩ ) ) = ( ⟨“ 𝐴 𝐴 ”⟩ ‘ 1 ) )
10 s2fv0 ⊢ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) → ( ⟨“ 𝐴 𝐴 ”⟩ ‘ 0 ) = 𝐴 )
11 6 9 10 3eqtr4rd ⊢ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) → ( ⟨“ 𝐴 𝐴 ”⟩ ‘ 0 ) = ( ⟨“ 𝐴 𝐴 ”⟩ ‘ ( ♯ ‘ ⟨“ 𝐽 ”⟩ ) ) )
12 5 11 syl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 } ) → ( ⟨“ 𝐴 𝐴 ”⟩ ‘ 0 ) = ( ⟨“ 𝐴 𝐴 ”⟩ ‘ ( ♯ ‘ ⟨“ 𝐽 ”⟩ ) ) )
13 iscycl ⊢ ( ⟨“ 𝐽 ”⟩ ( Cycles ‘ 𝐺 ) ⟨“ 𝐴 𝐴 ”⟩ ↔ ( ⟨“ 𝐽 ”⟩ ( Paths ‘ 𝐺 ) ⟨“ 𝐴 𝐴 ”⟩ ∧ ( ⟨“ 𝐴 𝐴 ”⟩ ‘ 0 ) = ( ⟨“ 𝐴 𝐴 ”⟩ ‘ ( ♯ ‘ ⟨“ 𝐽 ”⟩ ) ) ) )
14 4 12 13 sylanbrc ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 } ) → ⟨“ 𝐽 ”⟩ ( Cycles ‘ 𝐺 ) ⟨“ 𝐴 𝐴 ”⟩ )