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 ⊢φ→FCircuits⁡GP
crctcsh.n ⊢N=F
crctcsh.s ⊢φ→S∈0..^N
crctcsh.h ⊢H=FcyclShiftS
crctcsh.q ⊢Q=x∈0…N⟼ifx≤N−SP⁡x+SP⁡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 ⊢φ→FCircuits⁡GP
4 crctcsh.n ⊢N=F
5 crctcsh.s ⊢φ→S∈0..^N
6 crctcsh.h ⊢H=FcyclShiftS
7 crctcsh.q ⊢Q=x∈0…N⟼ifx≤N−SP⁡x+SP⁡x+S-N
8 crctistrl ⊢FCircuits⁡GP→FTrails⁡GP
9 trliswlk ⊢FTrails⁡GP→FWalks⁡GP
10 wlkv ⊢FWalks⁡GP→G∈V∧F∈V∧P∈V
11 simp1 ⊢G∈V∧F∈V∧P∈V→G∈V
12 9 10 11 3syl ⊢FTrails⁡GP→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⟼ifx≤N−SP⁡x+SP⁡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