Theorem crctcshlem3

Description: Lemma for crctcsh . (Contributed by AV, 10-Mar-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	crctcshlem3	|- ( ph -> ( G e. _V /\ H e. _V /\ Q e. _V ) )

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		crctistrl	|- ( F ( Circuits ` G ) P -> F ( Trails ` G ) P )
9		trliswlk	|- ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
10		wlkv	|- ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
11		simp1	|- ( ( G e. _V /\ F e. _V /\ P e. _V ) -> G e. _V )
12	9 10 11	3syl	|- ( F ( Trails ` G ) P -> G e. _V )
13	3 8 12	3syl	|- ( ph -> G e. _V )
14	6	ovexi	|- H e. _V
15	14	a1i	|- ( ph -> H e. _V )
16		ovex	|- ( 0 ... N ) e. _V
17	16	mptex	|- ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) ) e. _V
18	7 17	eqeltri	|- Q e. _V
19	18	a1i	|- ( ph -> Q e. _V )
20	13 15 19	3jca	|- ( ph -> ( G e. _V /\ H e. _V /\ Q e. _V ) )