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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	crctcsh.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	crctcsh.d	⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
	crctcsh.n	⊢ 𝑁 = ( ♯ ‘ 𝐹 )
	crctcsh.s	⊢ ( 𝜑 → 𝑆 ∈ ( 0 ..^ 𝑁 ) )
	crctcsh.h	⊢ 𝐻 = ( 𝐹 cyclShift 𝑆 )
	crctcsh.q	⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
Assertion	crctcshtrl	⊢ ( 𝜑 → 𝐻 ( Trails ‘ 𝐺 ) 𝑄 )

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	1 2 3 4 5 6 7	crctcshwlk	⊢ ( 𝜑 → 𝐻 ( Walks ‘ 𝐺 ) 𝑄 )
9		crctistrl	⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
10	2	trlf1	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 )
11		df-f1	⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ∧ Fun ^◡ 𝐹 ) )
12		iswrdi	⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → 𝐹 ∈ Word dom 𝐼 )
13	12	anim1i	⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ∧ Fun ^◡ 𝐹 ) → ( 𝐹 ∈ Word dom 𝐼 ∧ Fun ^◡ 𝐹 ) )
14	11 13	sylbi	⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ( 𝐹 ∈ Word dom 𝐼 ∧ Fun ^◡ 𝐹 ) )
15	10 14	syl	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ Word dom 𝐼 ∧ Fun ^◡ 𝐹 ) )
16	3 9 15	3syl	⊢ ( 𝜑 → ( 𝐹 ∈ Word dom 𝐼 ∧ Fun ^◡ 𝐹 ) )
17		elfzoelz	⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → 𝑆 ∈ ℤ )
18	5 17	syl	⊢ ( 𝜑 → 𝑆 ∈ ℤ )
19		df-3an	⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ Fun ^◡ 𝐹 ∧ 𝑆 ∈ ℤ ) ↔ ( ( 𝐹 ∈ Word dom 𝐼 ∧ Fun ^◡ 𝐹 ) ∧ 𝑆 ∈ ℤ ) )
20	16 18 19	sylanbrc	⊢ ( 𝜑 → ( 𝐹 ∈ Word dom 𝐼 ∧ Fun ^◡ 𝐹 ∧ 𝑆 ∈ ℤ ) )
21		cshinj	⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ Fun ^◡ 𝐹 ∧ 𝑆 ∈ ℤ ) → ( 𝐻 = ( 𝐹 cyclShift 𝑆 ) → Fun ^◡ 𝐻 ) )
22	20 6 21	mpisyl	⊢ ( 𝜑 → Fun ^◡ 𝐻 )
23		istrl	⊢ ( 𝐻 ( Trails ‘ 𝐺 ) 𝑄 ↔ ( 𝐻 ( Walks ‘ 𝐺 ) 𝑄 ∧ Fun ^◡ 𝐻 ) )
24	8 22 23	sylanbrc	⊢ ( 𝜑 → 𝐻 ( Trails ‘ 𝐺 ) 𝑄 )

Metamath Proof Explorer

Theorem crctcshtrl

Proof