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 ‘ 𝐺 ) ⟨“ 𝐴 𝐴 ”⟩ )