crctcshtrl

Description: Cyclically shifting the indices of a circuit <. F , P >. results in a trail <. H , Q >. . (Contributed by AV, 14-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Hypotheses	crctcsh.v	\|- V = ( Vtx ` G )
	crctcsh.i	\|- I = ( iEdg ` G )
	crctcsh.d	\|- ( ph -> F ( Circuits ` G ) P )
	crctcsh.n	\|- N = ( # ` F )
	crctcsh.s	\|- ( ph -> S e. ( 0 ..^ N ) )
	crctcsh.h	\|- H = ( F cyclShift S )
	crctcsh.q	\|- Q = ( x e. ( 0 ... N ) \|-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
Assertion	crctcshtrl	\|- ( ph -> H ( Trails ` G ) Q )

Proof

Step	Hyp	Ref	Expression
1		crctcsh.v	\|- V = ( Vtx ` G )
2		crctcsh.i	\|- I = ( iEdg ` G )
3		crctcsh.d	\|- ( ph -> F ( Circuits ` G ) P )
4		crctcsh.n	\|- N = ( # ` F )
5		crctcsh.s	\|- ( ph -> S e. ( 0 ..^ N ) )
6		crctcsh.h	\|- H = ( F cyclShift S )
7		crctcsh.q	\|- Q = ( x e. ( 0 ... N ) \|-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
8	1 2 3 4 5 6 7	crctcshwlk	\|- ( ph -> H ( Walks ` G ) Q )
9		crctistrl	\|- ( F ( Circuits ` G ) P -> F ( Trails ` G ) P )
10	2	trlf1	\|- ( F ( Trails ` G ) P -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I )
11		df-f1	\|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I <-> ( F : ( 0 ..^ ( # ` F ) ) --> dom I /\ Fun `' F ) )
12		iswrdi	\|- ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> F e. Word dom I )
13	12	anim1i	\|- ( ( F : ( 0 ..^ ( # ` F ) ) --> dom I /\ Fun `' F ) -> ( F e. Word dom I /\ Fun `' F ) )
14	11 13	sylbi	\|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> ( F e. Word dom I /\ Fun `' F ) )
15	3 9 10 14	4syl	\|- ( ph -> ( F e. Word dom I /\ Fun `' F ) )
16		elfzoelz	\|- ( S e. ( 0 ..^ N ) -> S e. ZZ )
17	5 16	syl	\|- ( ph -> S e. ZZ )
18		df-3an	\|- ( ( F e. Word dom I /\ Fun `' F /\ S e. ZZ ) <-> ( ( F e. Word dom I /\ Fun `' F ) /\ S e. ZZ ) )
19	15 17 18	sylanbrc	\|- ( ph -> ( F e. Word dom I /\ Fun `' F /\ S e. ZZ ) )
20		cshinj	\|- ( ( F e. Word dom I /\ Fun `' F /\ S e. ZZ ) -> ( H = ( F cyclShift S ) -> Fun `' H ) )
21	19 6 20	mpisyl	\|- ( ph -> Fun `' H )
22		istrl	\|- ( H ( Trails ` G ) Q <-> ( H ( Walks ` G ) Q /\ Fun `' H ) )
23	8 21 22	sylanbrc	\|- ( ph -> H ( Trails ` G ) Q )

Metamath Proof Explorer

Theorem crctcshtrl

Proof