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 e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> <" J "> ( Cycles ` G ) <" A A "> )

Proof

Step	Hyp	Ref	Expression
1		lppthon.i	|- I = ( iEdg ` G )
2	1	lppthon	|- ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> <" J "> ( A ( PathsOn ` G ) A ) <" A A "> )
3		pthonispth	|- ( <" J "> ( A ( PathsOn ` G ) A ) <" A A "> -> <" J "> ( Paths ` G ) <" A A "> )
4	2 3	syl	|- ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> <" J "> ( Paths ` G ) <" A A "> )
5	1	lpvtx	|- ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> A e. ( Vtx ` G ) )
6		s2fv1	|- ( A e. ( Vtx ` G ) -> ( <" A A "> ` 1 ) = A )
7		s1len	|- ( # ` <" J "> ) = 1
8	7	fveq2i	|- ( <" A A "> ` ( # ` <" J "> ) ) = ( <" A A "> ` 1 )
9	8	a1i	|- ( A e. ( Vtx ` G ) -> ( <" A A "> ` ( # ` <" J "> ) ) = ( <" A A "> ` 1 ) )
10		s2fv0	|- ( A e. ( Vtx ` G ) -> ( <" A A "> ` 0 ) = A )
11	6 9 10	3eqtr4rd	|- ( A e. ( Vtx ` G ) -> ( <" A A "> ` 0 ) = ( <" A A "> ` ( # ` <" J "> ) ) )
12	5 11	syl	|- ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> ( <" A A "> ` 0 ) = ( <" A A "> ` ( # ` <" J "> ) ) )
13		iscycl	|- ( <" J "> ( Cycles ` G ) <" A A "> <-> ( <" J "> ( Paths ` G ) <" A A "> /\ ( <" A A "> ` 0 ) = ( <" A A "> ` ( # ` <" J "> ) ) ) )
14	4 12 13	sylanbrc	|- ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> <" J "> ( Cycles ` G ) <" A A "> )