MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eucrctshift Structured version   Visualization version   GIF version

Theorem eucrctshift 27939
Description: Cyclically shifting the indices of an Eulerian circuit 𝐹, 𝑃 results in an Eulerian circuit 𝐻, 𝑄. (Contributed by AV, 15-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.)
Hypotheses
Ref Expression
eucrctshift.v 𝑉 = (Vtx‘𝐺)
eucrctshift.i 𝐼 = (iEdg‘𝐺)
eucrctshift.c (𝜑𝐹(Circuits‘𝐺)𝑃)
eucrctshift.n 𝑁 = (♯‘𝐹)
eucrctshift.s (𝜑𝑆 ∈ (0..^𝑁))
eucrctshift.h 𝐻 = (𝐹 cyclShift 𝑆)
eucrctshift.q 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
eucrctshift.e (𝜑𝐹(EulerPaths‘𝐺)𝑃)
Assertion
Ref Expression
eucrctshift (𝜑 → (𝐻(EulerPaths‘𝐺)𝑄𝐻(Circuits‘𝐺)𝑄))
Distinct variable groups:   𝑥,𝐹   𝑥,𝐻   𝑥,𝐼   𝑥,𝑁   𝑥,𝑃   𝑥,𝑆   𝑥,𝑉   𝜑,𝑥
Allowed substitution hints:   𝑄(𝑥)   𝐺(𝑥)

Proof of Theorem eucrctshift
Dummy variables 𝑖 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eucrctshift.v . . . . 5 𝑉 = (Vtx‘𝐺)
2 eucrctshift.i . . . . 5 𝐼 = (iEdg‘𝐺)
3 eucrctshift.c . . . . 5 (𝜑𝐹(Circuits‘𝐺)𝑃)
4 eucrctshift.n . . . . 5 𝑁 = (♯‘𝐹)
5 eucrctshift.s . . . . 5 (𝜑𝑆 ∈ (0..^𝑁))
6 eucrctshift.h . . . . 5 𝐻 = (𝐹 cyclShift 𝑆)
7 eucrctshift.q . . . . 5 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
81, 2, 3, 4, 5, 6, 7crctcshtrl 27518 . . . 4 (𝜑𝐻(Trails‘𝐺)𝑄)
9 simpr 485 . . . . 5 ((𝜑𝐻(Trails‘𝐺)𝑄) → 𝐻(Trails‘𝐺)𝑄)
10 eucrctshift.e . . . . . . . 8 (𝜑𝐹(EulerPaths‘𝐺)𝑃)
112eupthf1o 27900 . . . . . . . 8 (𝐹(EulerPaths‘𝐺)𝑃𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼)
1210, 11syl 17 . . . . . . 7 (𝜑𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼)
1312adantr 481 . . . . . 6 ((𝜑𝐻(Trails‘𝐺)𝑄) → 𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼)
14 trliswlk 27396 . . . . . . . . 9 (𝐻(Trails‘𝐺)𝑄𝐻(Walks‘𝐺)𝑄)
152wlkf 27313 . . . . . . . . 9 (𝐻(Walks‘𝐺)𝑄𝐻 ∈ Word dom 𝐼)
16 wrdf 13859 . . . . . . . . 9 (𝐻 ∈ Word dom 𝐼𝐻:(0..^(♯‘𝐻))⟶dom 𝐼)
1714, 15, 163syl 18 . . . . . . . 8 (𝐻(Trails‘𝐺)𝑄𝐻:(0..^(♯‘𝐻))⟶dom 𝐼)
18 df-f1o 6358 . . . . . . . . . 10 (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼 ↔ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼))
19 dffo3 6863 . . . . . . . . . . 11 (𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼 ↔ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦)))
20 crctiswlk 27494 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹(Circuits‘𝐺)𝑃𝐹(Walks‘𝐺)𝑃)
212wlkf 27313 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹(Walks‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
22 lencl 13876 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹 ∈ Word dom 𝐼 → (♯‘𝐹) ∈ ℕ0)
234oveq2i 7162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0..^𝑁) = (0..^(♯‘𝐹))
2423eleq2i 2908 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑆 ∈ (0..^𝑁) ↔ 𝑆 ∈ (0..^(♯‘𝐹)))
25 elfzonn0 13075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑆 ∈ ℕ0)
2625adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → 𝑆 ∈ ℕ0)
27 elfzonn0 13075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 ∈ (0..^(♯‘𝐹)) → 𝑦 ∈ ℕ0)
28 nn0sub 11939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑆 ∈ ℕ0𝑦 ∈ ℕ0) → (𝑆𝑦 ↔ (𝑦𝑆) ∈ ℕ0))
2926, 27, 28syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑆𝑦 ↔ (𝑦𝑆) ∈ ℕ0))
3029biimpac 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦𝑆) ∈ ℕ0)
31 elfzo0 13071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 ∈ (0..^(♯‘𝐹)) ↔ (𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)))
32 simp2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (♯‘𝐹) ∈ ℕ)
3331, 32sylbi 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℕ)
3433ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (♯‘𝐹) ∈ ℕ)
35 nn0re 11898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑦 ∈ ℕ0𝑦 ∈ ℝ)
3635ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → 𝑦 ∈ ℝ)
37 nnre 11637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((♯‘𝐹) ∈ ℕ → (♯‘𝐹) ∈ ℝ)
3837adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) → (♯‘𝐹) ∈ ℝ)
3938adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ∈ ℝ)
40 elfzoelz 13031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑆 ∈ ℤ)
4140zred 12079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑆 ∈ ℝ)
42 readdcl 10612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((♯‘𝐹) ∈ ℝ ∧ 𝑆 ∈ ℝ) → ((♯‘𝐹) + 𝑆) ∈ ℝ)
4338, 41, 42syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → ((♯‘𝐹) + 𝑆) ∈ ℝ)
4436, 39, 433jca 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦 ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ ∧ ((♯‘𝐹) + 𝑆) ∈ ℝ))
45 elfzole1 13039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑆 ∈ (0..^(♯‘𝐹)) → 0 ≤ 𝑆)
4645adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → 0 ≤ 𝑆)
47 addge01 11142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((♯‘𝐹) ∈ ℝ ∧ 𝑆 ∈ ℝ) → (0 ≤ 𝑆 ↔ (♯‘𝐹) ≤ ((♯‘𝐹) + 𝑆)))
4838, 41, 47syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (0 ≤ 𝑆 ↔ (♯‘𝐹) ≤ ((♯‘𝐹) + 𝑆)))
4946, 48mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ≤ ((♯‘𝐹) + 𝑆))
5044, 49lelttrdi 10794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦 < (♯‘𝐹) → 𝑦 < ((♯‘𝐹) + 𝑆)))
5150ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) → (𝑆 ∈ (0..^(♯‘𝐹)) → (𝑦 < (♯‘𝐹) → 𝑦 < ((♯‘𝐹) + 𝑆))))
5251com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) → (𝑦 < (♯‘𝐹) → (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑦 < ((♯‘𝐹) + 𝑆))))
53523impia 1111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑦 < ((♯‘𝐹) + 𝑆)))
5453adantld 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → 𝑦 < ((♯‘𝐹) + 𝑆)))
5554imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → 𝑦 < ((♯‘𝐹) + 𝑆))
56353ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → 𝑦 ∈ ℝ)
5756adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → 𝑦 ∈ ℝ)
5841ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → 𝑆 ∈ ℝ)
59 elfzoel2 13030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑆 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℤ)
6059zred 12079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑆 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℝ)
6160ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → (♯‘𝐹) ∈ ℝ)
6257, 58, 61ltsubaddd 11228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → ((𝑦𝑆) < (♯‘𝐹) ↔ 𝑦 < ((♯‘𝐹) + 𝑆)))
6355, 62mpbird 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → (𝑦𝑆) < (♯‘𝐹))
6463ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦𝑆) < (♯‘𝐹)))
6531, 64sylbi 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 ∈ (0..^(♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦𝑆) < (♯‘𝐹)))
6665impcom 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑦𝑆) < (♯‘𝐹))
6766adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦𝑆) < (♯‘𝐹))
68 elfzo0 13071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑦𝑆) ∈ (0..^(♯‘𝐹)) ↔ ((𝑦𝑆) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑦𝑆) < (♯‘𝐹)))
6930, 34, 67, 68syl3anbrc 1337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦𝑆) ∈ (0..^(♯‘𝐹)))
70 oveq1 7158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑦𝑆) → (𝑧 + 𝑆) = ((𝑦𝑆) + 𝑆))
7170oveq1d 7166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = (𝑦𝑆) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = (((𝑦𝑆) + 𝑆) mod (♯‘𝐹)))
7240zcnd 12080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑆 ∈ ℂ)
7372adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → 𝑆 ∈ ℂ)
74 elfzoelz 13031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 ∈ (0..^(♯‘𝐹)) → 𝑦 ∈ ℤ)
7574zcnd 12080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 ∈ (0..^(♯‘𝐹)) → 𝑦 ∈ ℂ)
7673, 75anim12ci 613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ))
7776adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ))
78 npcan 10887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ) → ((𝑦𝑆) + 𝑆) = 𝑦)
7977, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((𝑦𝑆) + 𝑆) = 𝑦)
8079oveq1d 7166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((𝑦𝑆) + 𝑆) mod (♯‘𝐹)) = (𝑦 mod (♯‘𝐹)))
81 zmodidfzoimp 13262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (0..^(♯‘𝐹)) → (𝑦 mod (♯‘𝐹)) = 𝑦)
8281ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦 mod (♯‘𝐹)) = 𝑦)
8380, 82eqtrd 2860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((𝑦𝑆) + 𝑆) mod (♯‘𝐹)) = 𝑦)
8471, 83sylan9eqr 2882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ 𝑧 = (𝑦𝑆)) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = 𝑦)
8584eqcomd 2831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ 𝑧 = (𝑦𝑆)) → 𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
8669, 85rspcedeq2vd 3633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
87 elfzo0 13071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑆 ∈ (0..^(♯‘𝐹)) ↔ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)))
88 nn0cn 11899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑦 ∈ ℕ0𝑦 ∈ ℂ)
8988ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → 𝑦 ∈ ℂ)
90 nn0cn 11899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑆 ∈ ℕ0𝑆 ∈ ℂ)
91903ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → 𝑆 ∈ ℂ)
9291adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → 𝑆 ∈ ℂ)
93 nncn 11638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((♯‘𝐹) ∈ ℕ → (♯‘𝐹) ∈ ℂ)
94933ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (♯‘𝐹) ∈ ℂ)
9594adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (♯‘𝐹) ∈ ℂ)
9689, 92, 95subadd23d 11011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((𝑦𝑆) + (♯‘𝐹)) = (𝑦 + ((♯‘𝐹) − 𝑆)))
97 simpll 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → 𝑦 ∈ ℕ0)
98 nn0z 11997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑆 ∈ ℕ0𝑆 ∈ ℤ)
99 nnz 11996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((♯‘𝐹) ∈ ℕ → (♯‘𝐹) ∈ ℤ)
100 znnsub 12020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑆 ∈ ℤ ∧ (♯‘𝐹) ∈ ℤ) → (𝑆 < (♯‘𝐹) ↔ ((♯‘𝐹) − 𝑆) ∈ ℕ))
10198, 99, 100syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) → (𝑆 < (♯‘𝐹) ↔ ((♯‘𝐹) − 𝑆) ∈ ℕ))
102101biimp3a 1462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → ((♯‘𝐹) − 𝑆) ∈ ℕ)
103102adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((♯‘𝐹) − 𝑆) ∈ ℕ)
104103nnnn0d 11947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((♯‘𝐹) − 𝑆) ∈ ℕ0)
10597, 104nn0addcld 11951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (𝑦 + ((♯‘𝐹) − 𝑆)) ∈ ℕ0)
10696, 105eqeltrd 2917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0)
107106adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0)
108 simplr2 1210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → (♯‘𝐹) ∈ ℕ)
10988adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) → 𝑦 ∈ ℂ)
110 subcl 10877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑦𝑆) ∈ ℂ)
111109, 91, 110syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (𝑦𝑆) ∈ ℂ)
11295, 111jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((♯‘𝐹) ∈ ℂ ∧ (𝑦𝑆) ∈ ℂ))
113112adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((♯‘𝐹) ∈ ℂ ∧ (𝑦𝑆) ∈ ℂ))
114 addcom 10818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((♯‘𝐹) ∈ ℂ ∧ (𝑦𝑆) ∈ ℂ) → ((♯‘𝐹) + (𝑦𝑆)) = ((𝑦𝑆) + (♯‘𝐹)))
115113, 114syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((♯‘𝐹) + (𝑦𝑆)) = ((𝑦𝑆) + (♯‘𝐹)))
11635adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) → 𝑦 ∈ ℝ)
117 nn0re 11898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑆 ∈ ℕ0𝑆 ∈ ℝ)
1181173ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → 𝑆 ∈ ℝ)
119 ltnle 10712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦 < 𝑆 ↔ ¬ 𝑆𝑦))
120 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → 𝑦 ∈ ℝ)
121 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ ℝ)
122120, 121sublt0d 11258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → ((𝑦𝑆) < 0 ↔ 𝑦 < 𝑆))
123122biimprd 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦 < 𝑆 → (𝑦𝑆) < 0))
124119, 123sylbird 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (¬ 𝑆𝑦 → (𝑦𝑆) < 0))
125116, 118, 124syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (¬ 𝑆𝑦 → (𝑦𝑆) < 0))
126125imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → (𝑦𝑆) < 0)
127 resubcl 10942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦𝑆) ∈ ℝ)
128116, 118, 127syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (𝑦𝑆) ∈ ℝ)
129373ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (♯‘𝐹) ∈ ℝ)
130129adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (♯‘𝐹) ∈ ℝ)
131128, 130jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((𝑦𝑆) ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ))
132131adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((𝑦𝑆) ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ))
133 ltaddneg 10847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦𝑆) ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ) → ((𝑦𝑆) < 0 ↔ ((♯‘𝐹) + (𝑦𝑆)) < (♯‘𝐹)))
134132, 133syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((𝑦𝑆) < 0 ↔ ((♯‘𝐹) + (𝑦𝑆)) < (♯‘𝐹)))
135126, 134mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((♯‘𝐹) + (𝑦𝑆)) < (♯‘𝐹))
136115, 135eqbrtrrd 5086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹))
137107, 108, 1363jca 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))
138137exp31 420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) → ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
1391383adant2 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
14087, 139syl5bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (𝑆 ∈ (0..^(♯‘𝐹)) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
141140adantld 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
14231, 141sylbi 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 ∈ (0..^(♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
143142impcom 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹))))
144143impcom 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))
145 elfzo0 13071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦𝑆) + (♯‘𝐹)) ∈ (0..^(♯‘𝐹)) ↔ (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))
146144, 145sylibr 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((𝑦𝑆) + (♯‘𝐹)) ∈ (0..^(♯‘𝐹)))
147 oveq1 7158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = ((𝑦𝑆) + (♯‘𝐹)) → (𝑧 + 𝑆) = (((𝑦𝑆) + (♯‘𝐹)) + 𝑆))
148147oveq1d 7166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = ((𝑦𝑆) + (♯‘𝐹)) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = ((((𝑦𝑆) + (♯‘𝐹)) + 𝑆) mod (♯‘𝐹)))
14973adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑆 ∈ ℂ)
15075adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑦 ∈ ℂ)
151 nn0cn 11899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((♯‘𝐹) ∈ ℕ0 → (♯‘𝐹) ∈ ℂ)
152151ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ∈ ℂ)
153149, 150, 1523jca 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ))
154153adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ))
155 simp2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → 𝑦 ∈ ℂ)
156 simp3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → (♯‘𝐹) ∈ ℂ)
157 simp1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → 𝑆 ∈ ℂ)
158155, 157, 156nppcand 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → (((𝑦𝑆) + (♯‘𝐹)) + 𝑆) = (𝑦 + (♯‘𝐹)))
159155, 156, 158comraddd 10846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → (((𝑦𝑆) + (♯‘𝐹)) + 𝑆) = ((♯‘𝐹) + 𝑦))
160154, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((𝑦𝑆) + (♯‘𝐹)) + 𝑆) = ((♯‘𝐹) + 𝑦))
161160oveq1d 7166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((((𝑦𝑆) + (♯‘𝐹)) + 𝑆) mod (♯‘𝐹)) = (((♯‘𝐹) + 𝑦) mod (♯‘𝐹)))
16231biimpi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (0..^(♯‘𝐹)) → (𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)))
163162ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)))
164 addmodid 13280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (((♯‘𝐹) + 𝑦) mod (♯‘𝐹)) = 𝑦)
165163, 164syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((♯‘𝐹) + 𝑦) mod (♯‘𝐹)) = 𝑦)
166161, 165eqtrd 2860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((((𝑦𝑆) + (♯‘𝐹)) + 𝑆) mod (♯‘𝐹)) = 𝑦)
167148, 166sylan9eqr 2882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ 𝑧 = ((𝑦𝑆) + (♯‘𝐹))) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = 𝑦)
168167eqcomd 2831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ 𝑧 = ((𝑦𝑆) + (♯‘𝐹))) → 𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
169146, 168rspcedeq2vd 3633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
17086, 169pm2.61ian 808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
17123rexeqi 3419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)) ↔ ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
172170, 171sylibr 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
173172exp31 420 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((♯‘𝐹) ∈ ℕ0 → (𝑆 ∈ (0..^(♯‘𝐹)) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))))
17424, 173syl5bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((♯‘𝐹) ∈ ℕ0 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))))
17522, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 ∈ Word dom 𝐼 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))))
17620, 21, 1753syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹(Circuits‘𝐺)𝑃 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))))
1773, 5, 176sylc 65 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))))
178177adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ dom 𝐼) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))))
179178imp 407 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
180179adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
181 fveq2 6666 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)) → (𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
182181reximi 3247 . . . . . . . . . . . . . . . . . . . 20 (∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
183180, 182syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
1843, 20, 213syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹 ∈ Word dom 𝐼)
185184ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → 𝐹 ∈ Word dom 𝐼)
186 elfzoelz 13031 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ)
1875, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑆 ∈ ℤ)
188187ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → 𝑆 ∈ ℤ)
18923eleq2i 2908 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (0..^𝑁) ↔ 𝑧 ∈ (0..^(♯‘𝐹)))
190189biimpi 217 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (0..^𝑁) → 𝑧 ∈ (0..^(♯‘𝐹)))
191 cshwidxmod 14158 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ Word dom 𝐼𝑆 ∈ ℤ ∧ 𝑧 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑧) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
192185, 188, 190, 191syl2an3an 1416 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) ∧ 𝑧 ∈ (0..^𝑁)) → ((𝐹 cyclShift 𝑆)‘𝑧) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
193192eqeq2d 2836 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) ∧ 𝑧 ∈ (0..^𝑁)) → ((𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧) ↔ (𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹)))))
194193rexbidva 3300 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧) ↔ ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹)))))
195183, 194mpbird 258 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧))
1961, 2, 3, 4, 5, 6crctcshlem2 27513 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (♯‘𝐻) = 𝑁)
197196oveq2d 7167 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁))
198197ad3antrrr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (0..^(♯‘𝐻)) = (0..^𝑁))
199 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → 𝑖 = (𝐹𝑦))
2006fveq1i 6667 . . . . . . . . . . . . . . . . . . . . 21 (𝐻𝑧) = ((𝐹 cyclShift 𝑆)‘𝑧)
201200a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (𝐻𝑧) = ((𝐹 cyclShift 𝑆)‘𝑧))
202199, 201eqeq12d 2841 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (𝑖 = (𝐻𝑧) ↔ (𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧)))
203198, 202rexeqbidv 3407 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧) ↔ ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧)))
204195, 203mpbird 258 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → ∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧))
205204rexlimdva2 3291 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ dom 𝐼) → (∃𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) → ∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
206205ralimdva 3181 . . . . . . . . . . . . . . 15 (𝜑 → (∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) → ∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
207206impcom 408 . . . . . . . . . . . . . 14 ((∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) ∧ 𝜑) → ∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧))
208207anim1ci 615 . . . . . . . . . . . . 13 (((∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) ∧ 𝜑) ∧ 𝐻:(0..^(♯‘𝐻))⟶dom 𝐼) → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
209 dffo3 6863 . . . . . . . . . . . . 13 (𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼 ↔ (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
210208, 209sylibr 235 . . . . . . . . . . . 12 (((∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) ∧ 𝜑) ∧ 𝐻:(0..^(♯‘𝐻))⟶dom 𝐼) → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)
211210exp31 420 . . . . . . . . . . 11 (∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) → (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
21219, 211simplbiim 505 . . . . . . . . . 10 (𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼 → (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
21318, 212simplbiim 505 . . . . . . . . 9 (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼 → (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
214213com13 88 . . . . . . . 8 (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 → (𝜑 → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
21517, 214syl 17 . . . . . . 7 (𝐻(Trails‘𝐺)𝑄 → (𝜑 → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
216215impcom 408 . . . . . 6 ((𝜑𝐻(Trails‘𝐺)𝑄) → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))
21713, 216mpd 15 . . . . 5 ((𝜑𝐻(Trails‘𝐺)𝑄) → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)
2189, 217jca 512 . . . 4 ((𝜑𝐻(Trails‘𝐺)𝑄) → (𝐻(Trails‘𝐺)𝑄𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))
2198, 218mpdan 683 . . 3 (𝜑 → (𝐻(Trails‘𝐺)𝑄𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))
2202iseupth 27897 . . 3 (𝐻(EulerPaths‘𝐺)𝑄 ↔ (𝐻(Trails‘𝐺)𝑄𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))
221219, 220sylibr 235 . 2 (𝜑𝐻(EulerPaths‘𝐺)𝑄)
2221, 2, 3, 4, 5, 6, 7crctcsh 27519 . 2 (𝜑𝐻(Circuits‘𝐺)𝑄)
223221, 222jca 512 1 (𝜑 → (𝐻(EulerPaths‘𝐺)𝑄𝐻(Circuits‘𝐺)𝑄))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  wral 3142  wrex 3143  ifcif 4469   class class class wbr 5062  cmpt 5142  dom cdm 5553  wf 6347  1-1wf1 6348  ontowfo 6349  1-1-ontowf1o 6350  cfv 6351  (class class class)co 7151  cc 10527  cr 10528  0cc0 10529   + caddc 10532   < clt 10667  cle 10668  cmin 10862  cn 11630  0cn0 11889  cz 11973  ...cfz 12885  ..^cfzo 13026   mod cmo 13230  chash 13683  Word cword 13854   cyclShift ccsh 14143  Vtxcvtx 26698  iEdgciedg 26699  Walkscwlks 27295  Trailsctrls 27389  Circuitsccrcts 27482  EulerPathsceupth 27893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-ifp 1057  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8282  df-map 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-sup 8898  df-inf 8899  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-n0 11890  df-z 11974  df-uz 12236  df-rp 12383  df-ico 12737  df-fz 12886  df-fzo 13027  df-fl 13155  df-mod 13231  df-hash 13684  df-word 13855  df-concat 13916  df-substr 13996  df-pfx 14026  df-csh 14144  df-wlks 27298  df-trls 27391  df-crcts 27484  df-eupth 27894
This theorem is referenced by:  eucrct2eupth  27941
  Copyright terms: Public domain W3C validator