Metamath Proof Explorer


Theorem crctcshlem4

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 crctcshlem4 φ S = 0 H = F Q = P

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 oveq2 S = 0 F cyclShift S = F cyclShift 0
9 crctiswlk F Circuits G P F Walks G P
10 2 wlkf F Walks G P F Word dom I
11 cshw0 F Word dom I F cyclShift 0 = F
12 3 9 10 11 4syl φ F cyclShift 0 = F
13 8 12 sylan9eqr φ S = 0 F cyclShift S = F
14 6 13 eqtrid φ S = 0 H = F
15 oveq2 S = 0 N S = N 0
16 1 2 3 4 crctcshlem1 φ N 0
17 16 nn0cnd φ N
18 17 subid1d φ N 0 = N
19 15 18 sylan9eqr φ S = 0 N S = N
20 19 breq2d φ S = 0 x N S x N
21 20 adantr φ S = 0 x 0 N x N S x N
22 oveq2 S = 0 x + S = x + 0
23 22 adantl φ S = 0 x + S = x + 0
24 elfzelz x 0 N x
25 24 zcnd x 0 N x
26 25 addridd x 0 N x + 0 = x
27 23 26 sylan9eq φ S = 0 x 0 N x + S = x
28 27 fveq2d φ S = 0 x 0 N P x + S = P x
29 27 fvoveq1d φ S = 0 x 0 N P x + S - N = P x N
30 21 28 29 ifbieq12d φ S = 0 x 0 N if x N S P x + S P x + S - N = if x N P x P x N
31 30 mpteq2dva φ S = 0 x 0 N if x N S P x + S P x + S - N = x 0 N if x N P x P x N
32 elfzle2 x 0 N x N
33 32 adantl φ x 0 N x N
34 33 iftrued φ x 0 N if x N P x P x N = P x
35 34 mpteq2dva φ x 0 N if x N P x P x N = x 0 N P x
36 1 wlkp F Walks G P P : 0 F V
37 3 9 36 3syl φ P : 0 F V
38 ffn P : 0 F V P Fn 0 F
39 4 eqcomi F = N
40 39 oveq2i 0 F = 0 N
41 40 fneq2i P Fn 0 F P Fn 0 N
42 38 41 sylib P : 0 F V P Fn 0 N
43 42 adantl φ P : 0 F V P Fn 0 N
44 dffn5 P Fn 0 N P = x 0 N P x
45 43 44 sylib φ P : 0 F V P = x 0 N P x
46 45 eqcomd φ P : 0 F V x 0 N P x = P
47 37 46 mpdan φ x 0 N P x = P
48 35 47 eqtrd φ x 0 N if x N P x P x N = P
49 48 adantr φ S = 0 x 0 N if x N P x P x N = P
50 31 49 eqtrd φ S = 0 x 0 N if x N S P x + S P x + S - N = P
51 7 50 eqtrid φ S = 0 Q = P
52 14 51 jca φ S = 0 H = F Q = P