Theorem clwlkcomp

Description: A closed walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 17-Feb-2021)

	Ref	Expression
Hypotheses	isclwlke.v	|- V = ( Vtx ` G )
	isclwlke.i	|- I = ( iEdg ` G )
	clwlkcomp.1	|- F = ( 1st ` W )
	clwlkcomp.2	|- P = ( 2nd ` W )
Assertion	clwlkcomp	|- ( ( G e. X /\ W e. ( S X. T ) ) -> ( W e. ( ClWalks ` G ) <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isclwlke.v	|- V = ( Vtx ` G )
2		isclwlke.i	|- I = ( iEdg ` G )
3		clwlkcomp.1	|- F = ( 1st ` W )
4		clwlkcomp.2	|- P = ( 2nd ` W )
5	3	eqcomi	|- ( 1st ` W ) = F
6	4	eqcomi	|- ( 2nd ` W ) = P
7	5 6	pm3.2i	|- ( ( 1st ` W ) = F /\ ( 2nd ` W ) = P )
8		eqop	|- ( W e. ( S X. T ) -> ( W = <. F , P >. <-> ( ( 1st ` W ) = F /\ ( 2nd ` W ) = P ) ) )
9	7 8	mpbiri	|- ( W e. ( S X. T ) -> W = <. F , P >. )
10	9	eleq1d	|- ( W e. ( S X. T ) -> ( W e. ( ClWalks ` G ) <-> <. F , P >. e. ( ClWalks ` G ) ) )
11		df-br	|- ( F ( ClWalks ` G ) P <-> <. F , P >. e. ( ClWalks ` G ) )
12	10 11	bitr4di	|- ( W e. ( S X. T ) -> ( W e. ( ClWalks ` G ) <-> F ( ClWalks ` G ) P ) )
13	1 2	isclwlke	|- ( G e. X -> ( F ( ClWalks ` G ) P <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) ) )
14	12 13	sylan9bbr	|- ( ( G e. X /\ W e. ( S X. T ) ) -> ( W e. ( ClWalks ` G ) <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) ) )