Theorem crctcshlem3

Description: Lemma for crctcsh . (Contributed by AV, 10-Mar-2021)

	Ref	Expression
Hypotheses	crctcsh.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	crctcsh.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	crctcsh.d	⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
	crctcsh.n	⊢ 𝑁 = ( ♯ ‘ 𝐹 )
	crctcsh.s	⊢ ( 𝜑 → 𝑆 ∈ ( 0 ..^ 𝑁 ) )
	crctcsh.h	⊢ 𝐻 = ( 𝐹 cyclShift 𝑆 )
	crctcsh.q	⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
Assertion	crctcshlem3	⊢ ( 𝜑 → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		crctcsh.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		crctcsh.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		crctcsh.d	⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
4		crctcsh.n	⊢ 𝑁 = ( ♯ ‘ 𝐹 )
5		crctcsh.s	⊢ ( 𝜑 → 𝑆 ∈ ( 0 ..^ 𝑁 ) )
6		crctcsh.h	⊢ 𝐻 = ( 𝐹 cyclShift 𝑆 )
7		crctcsh.q	⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
8		crctistrl	⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
9		trliswlk	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
10		wlkv	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
11		simp1	⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → 𝐺 ∈ V )
12	9 10 11	3syl	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐺 ∈ V )
13	3 8 12	3syl	⊢ ( 𝜑 → 𝐺 ∈ V )
14	6	ovexi	⊢ 𝐻 ∈ V
15	14	a1i	⊢ ( 𝜑 → 𝐻 ∈ V )
16		ovex	⊢ ( 0 ... 𝑁 ) ∈ V
17	16	mptex	⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ) ∈ V
18	7 17	eqeltri	⊢ 𝑄 ∈ V
19	18	a1i	⊢ ( 𝜑 → 𝑄 ∈ V )
20	13 15 19	3jca	⊢ ( 𝜑 → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V ) )