Theorem crctcshlem4

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	crctcshlem4	⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝐻 = 𝐹 ∧ 𝑄 = 𝑃 ) )

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		oveq2	⊢ ( 𝑆 = 0 → ( 𝐹 cyclShift 𝑆 ) = ( 𝐹 cyclShift 0 ) )
9		crctiswlk	⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
10	2	wlkf	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
11	3 9 10	3syl	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
12		cshw0	⊢ ( 𝐹 ∈ Word dom 𝐼 → ( 𝐹 cyclShift 0 ) = 𝐹 )
13	11 12	syl	⊢ ( 𝜑 → ( 𝐹 cyclShift 0 ) = 𝐹 )
14	8 13	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝐹 cyclShift 𝑆 ) = 𝐹 )
15	6 14	syl5eq	⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → 𝐻 = 𝐹 )
16		oveq2	⊢ ( 𝑆 = 0 → ( 𝑁 − 𝑆 ) = ( 𝑁 − 0 ) )
17	1 2 3 4	crctcshlem1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
18	17	nn0cnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
19	18	subid1d	⊢ ( 𝜑 → ( 𝑁 − 0 ) = 𝑁 )
20	16 19	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝑁 − 𝑆 ) = 𝑁 )
21	20	breq2d	⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝑥 ≤ ( 𝑁 − 𝑆 ) ↔ 𝑥 ≤ 𝑁 ) )
22	21	adantr	⊢ ( ( ( 𝜑 ∧ 𝑆 = 0 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 ≤ ( 𝑁 − 𝑆 ) ↔ 𝑥 ≤ 𝑁 ) )
23		oveq2	⊢ ( 𝑆 = 0 → ( 𝑥 + 𝑆 ) = ( 𝑥 + 0 ) )
24	23	adantl	⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝑥 + 𝑆 ) = ( 𝑥 + 0 ) )
25		elfzelz	⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑥 ∈ ℤ )
26	25	zcnd	⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑥 ∈ ℂ )
27	26	addid1d	⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → ( 𝑥 + 0 ) = 𝑥 )
28	24 27	sylan9eq	⊢ ( ( ( 𝜑 ∧ 𝑆 = 0 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 + 𝑆 ) = 𝑥 )
29	28	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑆 = 0 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) = ( 𝑃 ‘ 𝑥 ) )
30	28	fvoveq1d	⊢ ( ( ( 𝜑 ∧ 𝑆 = 0 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) = ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) )
31	22 29 30	ifbieq12d	⊢ ( ( ( 𝜑 ∧ 𝑆 = 0 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) = if ( 𝑥 ≤ 𝑁 , ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) ) )
32	31	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ) = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ 𝑁 , ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) ) ) )
33		elfzle2	⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑥 ≤ 𝑁 )
34	33	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → 𝑥 ≤ 𝑁 )
35	34	iftrued	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → if ( 𝑥 ≤ 𝑁 , ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) ) = ( 𝑃 ‘ 𝑥 ) )
36	35	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ 𝑁 , ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) ) ) = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ‘ 𝑥 ) ) )
37	1	wlkp	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
38	3 9 37	3syl	⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
39		ffn	⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) )
40	4	eqcomi	⊢ ( ♯ ‘ 𝐹 ) = 𝑁
41	40	oveq2i	⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 𝑁 )
42	41	fneq2i	⊢ ( 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) ↔ 𝑃 Fn ( 0 ... 𝑁 ) )
43	39 42	sylib	⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → 𝑃 Fn ( 0 ... 𝑁 ) )
44	43	adantl	⊢ ( ( 𝜑 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → 𝑃 Fn ( 0 ... 𝑁 ) )
45		dffn5	⊢ ( 𝑃 Fn ( 0 ... 𝑁 ) ↔ 𝑃 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ‘ 𝑥 ) ) )
46	44 45	sylib	⊢ ( ( 𝜑 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → 𝑃 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ‘ 𝑥 ) ) )
47	46	eqcomd	⊢ ( ( 𝜑 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ‘ 𝑥 ) ) = 𝑃 )
48	38 47	mpdan	⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ‘ 𝑥 ) ) = 𝑃 )
49	36 48	eqtrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ 𝑁 , ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) ) ) = 𝑃 )
50	49	adantr	⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ 𝑁 , ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) ) ) = 𝑃 )
51	32 50	eqtrd	⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ) = 𝑃 )
52	7 51	syl5eq	⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → 𝑄 = 𝑃 )
53	15 52	jca	⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝐻 = 𝐹 ∧ 𝑄 = 𝑃 ) )