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

Metamath Proof Explorer

Theorem crctcshlem4

Description: Lemma for crctcsh . (Contributed by AV, 10-Mar-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 crctcshlem4 ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝐻 = 𝐹 ∧ 𝑄 = 𝑃 ) )

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 oveq2 ⊢ ( 𝑆 = 0 → ( 𝐹 cyclShift 𝑆 ) = ( 𝐹 cyclShift 0 ) )
9 crctiswlk ⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
10 2 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
11 cshw0 ⊢ ( 𝐹 ∈ Word dom 𝐼 → ( 𝐹 cyclShift 0 ) = 𝐹 )
12 3 9 10 11 4syl ⊢ ( 𝜑 → ( 𝐹 cyclShift 0 ) = 𝐹 )
13 8 12 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝐹 cyclShift 𝑆 ) = 𝐹 )
14 6 13 eqtrid ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → 𝐻 = 𝐹 )
15 oveq2 ⊢ ( 𝑆 = 0 → ( 𝑁 − 𝑆 ) = ( 𝑁 − 0 ) )
16 1 2 3 4 crctcshlem1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
17 16 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
18 17 subid1d ⊢ ( 𝜑 → ( 𝑁 − 0 ) = 𝑁 )
19 15 18 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝑁 − 𝑆 ) = 𝑁 )
20 19 breq2d ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝑥 ≤ ( 𝑁 − 𝑆 ) ↔ 𝑥 ≤ 𝑁 ) )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑆 = 0 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 ≤ ( 𝑁 − 𝑆 ) ↔ 𝑥 ≤ 𝑁 ) )
22 oveq2 ⊢ ( 𝑆 = 0 → ( 𝑥 + 𝑆 ) = ( 𝑥 + 0 ) )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝑥 + 𝑆 ) = ( 𝑥 + 0 ) )
24 elfzelz ⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑥 ∈ ℤ )
25 24 zcnd ⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑥 ∈ ℂ )
26 25 addridd ⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → ( 𝑥 + 0 ) = 𝑥 )
27 23 26 sylan9eq ⊢ ( ( ( 𝜑 ∧ 𝑆 = 0 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 + 𝑆 ) = 𝑥 )
28 27 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑆 = 0 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) = ( 𝑃 ‘ 𝑥 ) )
29 27 fvoveq1d ⊢ ( ( ( 𝜑 ∧ 𝑆 = 0 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) = ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) )
30 21 28 29 ifbieq12d ⊢ ( ( ( 𝜑 ∧ 𝑆 = 0 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) = if ( 𝑥 ≤ 𝑁 , ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) ) )
31 30 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ) = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ 𝑁 , ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) ) ) )
32 elfzle2 ⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑥 ≤ 𝑁 )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → 𝑥 ≤ 𝑁 )
34 33 iftrued ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → if ( 𝑥 ≤ 𝑁 , ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) ) = ( 𝑃 ‘ 𝑥 ) )
35 34 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ 𝑁 , ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) ) ) = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ‘ 𝑥 ) ) )
36 1 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
37 3 9 36 3syl ⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
38 ffn ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) )
39 4 eqcomi ⊢ ( ♯ ‘ 𝐹 ) = 𝑁
40 39 oveq2i ⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 𝑁 )
41 40 fneq2i ⊢ ( 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) ↔ 𝑃 Fn ( 0 ... 𝑁 ) )
42 38 41 sylib ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → 𝑃 Fn ( 0 ... 𝑁 ) )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → 𝑃 Fn ( 0 ... 𝑁 ) )
44 dffn5 ⊢ ( 𝑃 Fn ( 0 ... 𝑁 ) ↔ 𝑃 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ‘ 𝑥 ) ) )
45 43 44 sylib ⊢ ( ( 𝜑 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → 𝑃 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ‘ 𝑥 ) ) )
46 45 eqcomd ⊢ ( ( 𝜑 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ‘ 𝑥 ) ) = 𝑃 )
47 37 46 mpdan ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ‘ 𝑥 ) ) = 𝑃 )
48 35 47 eqtrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ 𝑁 , ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) ) ) = 𝑃 )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ 𝑁 , ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 − 𝑁 ) ) ) ) = 𝑃 )
50 31 49 eqtrd ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ) = 𝑃 )
51 7 50 eqtrid ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → 𝑄 = 𝑃 )
52 14 51 jca ⊢ ( ( 𝜑 ∧ 𝑆 = 0 ) → ( 𝐻 = 𝐹 ∧ 𝑄 = 𝑃 ) )