This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → F Circuits ⁡ G P
crctcsh.n ⊢ N = F
crctcsh.s ⊢ φ → S ∈ 0 ..^ N
crctcsh.h ⊢ H = F cyclShift S
crctcsh.q ⊢ Q = x ∈ 0 … N ⟼ if x ≤ N − S P ⁡ x + S P ⁡ x + S - N
Assertion crctcshlem3 ⊢ φ → G ∈ V ∧ H ∈ V ∧ Q ∈ V

Proof

Step Hyp Ref Expression
1 crctcsh.v ⊢ V = Vtx ⁡ G
2 crctcsh.i ⊢ I = iEdg ⁡ G
3 crctcsh.d ⊢ φ → F Circuits ⁡ G P
4 crctcsh.n ⊢ N = F
5 crctcsh.s ⊢ φ → S ∈ 0 ..^ N
6 crctcsh.h ⊢ H = F cyclShift S
7 crctcsh.q ⊢ Q = x ∈ 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 ∈ V ∧ F ∈ V ∧ P ∈ V
11 simp1 ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → G ∈ V
12 9 10 11 3syl ⊢ F Trails ⁡ G P → G ∈ V
13 3 8 12 3syl ⊢ φ → G ∈ V
14 6 ovexi ⊢ H ∈ V
15 14 a1i ⊢ φ → H ∈ V
16 ovex ⊢ 0 … N ∈ V
17 16 mptex ⊢ x ∈ 0 … N ⟼ if x ≤ N − S P ⁡ x + S P ⁡ x + S - N ∈ V
18 7 17 eqeltri ⊢ Q ∈ V
19 18 a1i ⊢ φ → Q ∈ V
20 13 15 19 3jca ⊢ φ → G ∈ V ∧ H ∈ V ∧ Q ∈ V