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	$⊢ φ \to F Circuits (G) P$
	crctcsh.n	$⊢ N = \|F\|$
	crctcsh.s	$⊢ φ \to S \in (0 ..^N)$
	crctcsh.h	$⊢ H = F cyclShift S$
	crctcsh.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
Assertion	crctcshtrl	$⊢ φ \to H Trails (G) Q$

Proof

Step	Hyp	Ref	Expression
1		crctcsh.v	$⊢ V = Vtx (G)$
2		crctcsh.i	$⊢ I = iEdg (G)$
3		crctcsh.d	$⊢ φ \to F Circuits (G) P$
4		crctcsh.n	$⊢ N = \|F\|$
5		crctcsh.s	$⊢ φ \to S \in (0 ..^N)$
6		crctcsh.h	$⊢ H = F cyclShift S$
7		crctcsh.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
8	1 2 3 4 5 6 7	crctcshwlk	$⊢ φ \to H Walks (G) Q$
9		crctistrl	$⊢ F Circuits (G) P \to F Trails (G) P$
10	2	trlf1	$⊢ F Trails (G) P \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I$
11		df-f1	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \leftrightarrow (F : (0 ..^\|F\|) ⟶ dom I \land Fun F^{-1})$
12		iswrdi	$⊢ F : (0 ..^\|F\|) ⟶ dom I \to F \in Word dom I$
13	12	anim1i	$⊢ (F : (0 ..^\|F\|) ⟶ dom I \land Fun F^{-1}) \to (F \in Word dom I \land Fun F^{-1})$
14	11 13	sylbi	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to (F \in Word dom I \land Fun F^{-1})$
15	10 14	syl	$⊢ F Trails (G) P \to (F \in Word dom I \land Fun F^{-1})$
16	3 9 15	3syl	$⊢ φ \to (F \in Word dom I \land Fun F^{-1})$
17		elfzoelz	$⊢ S \in (0 ..^N) \to S \in ℤ$
18	5 17	syl	$⊢ φ \to S \in ℤ$
19		df-3an	$⊢ (F \in Word dom I \land Fun F^{-1} \land S \in ℤ) \leftrightarrow ((F \in Word dom I \land Fun F^{-1}) \land S \in ℤ)$
20	16 18 19	sylanbrc	$⊢ φ \to (F \in Word dom I \land Fun F^{-1} \land S \in ℤ)$
21		cshinj	$⊢ (F \in Word dom I \land Fun F^{-1} \land S \in ℤ) \to (H = F cyclShift S \to Fun H^{-1})$
22	20 6 21	mpisyl	$⊢ φ \to Fun H^{-1}$
23		istrl	$⊢ H Trails (G) Q \leftrightarrow (H Walks (G) Q \land Fun H^{-1})$
24	8 22 23	sylanbrc	$⊢ φ \to H Trails (G) Q$

Metamath Proof Explorer

Theorem crctcshtrl

Proof