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

Theorem eucrctshift 27415
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 26943 . . . 4 (𝜑𝐻(Trails‘𝐺)𝑄)
9 simpr 473 . . . . 5 ((𝜑𝐻(Trails‘𝐺)𝑄) → 𝐻(Trails‘𝐺)𝑄)
10 eucrctshift.e . . . . . . . 8 (𝜑𝐹(EulerPaths‘𝐺)𝑃)
112eupthf1o 27376 . . . . . . . 8 (𝐹(EulerPaths‘𝐺)𝑃𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼)
1210, 11syl 17 . . . . . . 7 (𝜑𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼)
1312adantr 468 . . . . . 6 ((𝜑𝐻(Trails‘𝐺)𝑄) → 𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼)
14 trliswlk 26821 . . . . . . . . 9 (𝐻(Trails‘𝐺)𝑄𝐻(Walks‘𝐺)𝑄)
152wlkf 26737 . . . . . . . . 9 (𝐻(Walks‘𝐺)𝑄𝐻 ∈ Word dom 𝐼)
16 wrdf 13517 . . . . . . . . 9 (𝐻 ∈ Word dom 𝐼𝐻:(0..^(♯‘𝐻))⟶dom 𝐼)
1714, 15, 163syl 18 . . . . . . . 8 (𝐻(Trails‘𝐺)𝑄𝐻:(0..^(♯‘𝐻))⟶dom 𝐼)
18 df-f1o 6104 . . . . . . . . . 10 (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼 ↔ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼))
19 dffo3 6592 . . . . . . . . . . 11 (𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼 ↔ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦)))
20 crctiswlk 26919 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹(Circuits‘𝐺)𝑃𝐹(Walks‘𝐺)𝑃)
212wlkf 26737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹(Walks‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
22 lencl 13531 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹 ∈ Word dom 𝐼 → (♯‘𝐹) ∈ ℕ0)
234oveq2i 6881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0..^𝑁) = (0..^(♯‘𝐹))
2423eleq2i 2877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑆 ∈ (0..^𝑁) ↔ 𝑆 ∈ (0..^(♯‘𝐹)))
25 elfzonn0 12733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑆 ∈ ℕ0)
2625adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → 𝑆 ∈ ℕ0)
27 elfzonn0 12733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (0..^(♯‘𝐹)) → 𝑦 ∈ ℕ0)
28 nn0sub 11605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑆 ∈ ℕ0𝑦 ∈ ℕ0) → (𝑆𝑦 ↔ (𝑦𝑆) ∈ ℕ0))
2926, 27, 28syl2an 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑆𝑦 ↔ (𝑦𝑆) ∈ ℕ0))
3029biimpac 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦𝑆) ∈ ℕ0)
31 elfzo0 12729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (0..^(♯‘𝐹)) ↔ (𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)))
32 simp2 1160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (♯‘𝐹) ∈ ℕ)
3331, 32sylbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℕ)
3433ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (♯‘𝐹) ∈ ℕ)
35 nn0re 11564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑦 ∈ ℕ0𝑦 ∈ ℝ)
3635ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → 𝑦 ∈ ℝ)
37 nnre 11308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((♯‘𝐹) ∈ ℕ → (♯‘𝐹) ∈ ℝ)
3837adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) → (♯‘𝐹) ∈ ℝ)
3938adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ∈ ℝ)
40 elfzoelz 12690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑆 ∈ ℤ)
4140zred 11744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑆 ∈ ℝ)
42 readdcl 10300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((♯‘𝐹) ∈ ℝ ∧ 𝑆 ∈ ℝ) → ((♯‘𝐹) + 𝑆) ∈ ℝ)
4338, 41, 42syl2an 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → ((♯‘𝐹) + 𝑆) ∈ ℝ)
4436, 39, 433jca 1151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦 ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ ∧ ((♯‘𝐹) + 𝑆) ∈ ℝ))
45 elfzole1 12698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑆 ∈ (0..^(♯‘𝐹)) → 0 ≤ 𝑆)
4645adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → 0 ≤ 𝑆)
47 addge01 10819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((♯‘𝐹) ∈ ℝ ∧ 𝑆 ∈ ℝ) → (0 ≤ 𝑆 ↔ (♯‘𝐹) ≤ ((♯‘𝐹) + 𝑆)))
4838, 41, 47syl2an 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (0 ≤ 𝑆 ↔ (♯‘𝐹) ≤ ((♯‘𝐹) + 𝑆)))
4946, 48mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ≤ ((♯‘𝐹) + 𝑆))
5044, 49lelttrdi 10480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦 < (♯‘𝐹) → 𝑦 < ((♯‘𝐹) + 𝑆)))
5150ex 399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) → (𝑆 ∈ (0..^(♯‘𝐹)) → (𝑦 < (♯‘𝐹) → 𝑦 < ((♯‘𝐹) + 𝑆))))
5251com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) → (𝑦 < (♯‘𝐹) → (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑦 < ((♯‘𝐹) + 𝑆))))
53523impia 1138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑦 < ((♯‘𝐹) + 𝑆)))
5453adantld 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → 𝑦 < ((♯‘𝐹) + 𝑆)))
5554imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → 𝑦 < ((♯‘𝐹) + 𝑆))
56353ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → 𝑦 ∈ ℝ)
5756adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → 𝑦 ∈ ℝ)
5841ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → 𝑆 ∈ ℝ)
59 elfzoel2 12689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑆 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℤ)
6059zred 11744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑆 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℝ)
6160ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → (♯‘𝐹) ∈ ℝ)
6257, 58, 61ltsubaddd 10904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → ((𝑦𝑆) < (♯‘𝐹) ↔ 𝑦 < ((♯‘𝐹) + 𝑆)))
6355, 62mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → (𝑦𝑆) < (♯‘𝐹))
6463ex 399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦𝑆) < (♯‘𝐹)))
6531, 64sylbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (0..^(♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦𝑆) < (♯‘𝐹)))
6665impcom 396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑦𝑆) < (♯‘𝐹))
6766adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦𝑆) < (♯‘𝐹))
68 elfzo0 12729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦𝑆) ∈ (0..^(♯‘𝐹)) ↔ ((𝑦𝑆) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑦𝑆) < (♯‘𝐹)))
6930, 34, 67, 68syl3anbrc 1436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦𝑆) ∈ (0..^(♯‘𝐹)))
70 oveq1 6877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 = (𝑦𝑆) → (𝑧 + 𝑆) = ((𝑦𝑆) + 𝑆))
7170oveq1d 6885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 = (𝑦𝑆) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = (((𝑦𝑆) + 𝑆) mod (♯‘𝐹)))
7240zcnd 11745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑆 ∈ ℂ)
7372adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → 𝑆 ∈ ℂ)
74 elfzoelz 12690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 ∈ (0..^(♯‘𝐹)) → 𝑦 ∈ ℤ)
7574zcnd 11745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 ∈ (0..^(♯‘𝐹)) → 𝑦 ∈ ℂ)
7673, 75anim12ci 603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ))
7776adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ))
78 npcan 10571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ) → ((𝑦𝑆) + 𝑆) = 𝑦)
7977, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((𝑦𝑆) + 𝑆) = 𝑦)
8079oveq1d 6885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((𝑦𝑆) + 𝑆) mod (♯‘𝐹)) = (𝑦 mod (♯‘𝐹)))
81 zmodidfzoimp 12920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ (0..^(♯‘𝐹)) → (𝑦 mod (♯‘𝐹)) = 𝑦)
8281ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦 mod (♯‘𝐹)) = 𝑦)
8380, 82eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((𝑦𝑆) + 𝑆) mod (♯‘𝐹)) = 𝑦)
8471, 83sylan9eqr 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ 𝑧 = (𝑦𝑆)) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = 𝑦)
8584eqcomd 2812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ 𝑧 = (𝑦𝑆)) → 𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
8669, 85rspcedeq2vd 3512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
87 elfzo0 12729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑆 ∈ (0..^(♯‘𝐹)) ↔ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)))
88 nn0cn 11565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑦 ∈ ℕ0𝑦 ∈ ℂ)
8988ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → 𝑦 ∈ ℂ)
90 nn0cn 11565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑆 ∈ ℕ0𝑆 ∈ ℂ)
91903ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → 𝑆 ∈ ℂ)
9291adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → 𝑆 ∈ ℂ)
93 nncn 11309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((♯‘𝐹) ∈ ℕ → (♯‘𝐹) ∈ ℂ)
94933ad2ant2 1157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (♯‘𝐹) ∈ ℂ)
9594adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (♯‘𝐹) ∈ ℂ)
9689, 92, 95subadd23d 10695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((𝑦𝑆) + (♯‘𝐹)) = (𝑦 + ((♯‘𝐹) − 𝑆)))
97 simpll 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → 𝑦 ∈ ℕ0)
98 nn0z 11662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑆 ∈ ℕ0𝑆 ∈ ℤ)
99 nnz 11661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((♯‘𝐹) ∈ ℕ → (♯‘𝐹) ∈ ℤ)
100 znnsub 11685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((𝑆 ∈ ℤ ∧ (♯‘𝐹) ∈ ℤ) → (𝑆 < (♯‘𝐹) ↔ ((♯‘𝐹) − 𝑆) ∈ ℕ))
10198, 99, 100syl2an 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) → (𝑆 < (♯‘𝐹) ↔ ((♯‘𝐹) − 𝑆) ∈ ℕ))
102101biimp3a 1586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → ((♯‘𝐹) − 𝑆) ∈ ℕ)
103102adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((♯‘𝐹) − 𝑆) ∈ ℕ)
104103nnnn0d 11613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((♯‘𝐹) − 𝑆) ∈ ℕ0)
10597, 104nn0addcld 11617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (𝑦 + ((♯‘𝐹) − 𝑆)) ∈ ℕ0)
10696, 105eqeltrd 2885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0)
107106adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0)
108 simplr2 1270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → (♯‘𝐹) ∈ ℕ)
10988adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) → 𝑦 ∈ ℂ)
110 subcl 10561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑦𝑆) ∈ ℂ)
111109, 91, 110syl2an 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (𝑦𝑆) ∈ ℂ)
11295, 111jca 503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((♯‘𝐹) ∈ ℂ ∧ (𝑦𝑆) ∈ ℂ))
113112adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((♯‘𝐹) ∈ ℂ ∧ (𝑦𝑆) ∈ ℂ))
114 addcom 10503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((♯‘𝐹) ∈ ℂ ∧ (𝑦𝑆) ∈ ℂ) → ((♯‘𝐹) + (𝑦𝑆)) = ((𝑦𝑆) + (♯‘𝐹)))
115113, 114syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((♯‘𝐹) + (𝑦𝑆)) = ((𝑦𝑆) + (♯‘𝐹)))
11635adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) → 𝑦 ∈ ℝ)
117 nn0re 11564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑆 ∈ ℕ0𝑆 ∈ ℝ)
1181173ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → 𝑆 ∈ ℝ)
119 ltnle 10398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦 < 𝑆 ↔ ¬ 𝑆𝑦))
120 simpl 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → 𝑦 ∈ ℝ)
121 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ ℝ)
122120, 121sublt0d 10934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → ((𝑦𝑆) < 0 ↔ 𝑦 < 𝑆))
123122biimprd 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦 < 𝑆 → (𝑦𝑆) < 0))
124119, 123sylbird 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (¬ 𝑆𝑦 → (𝑦𝑆) < 0))
125116, 118, 124syl2an 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (¬ 𝑆𝑦 → (𝑦𝑆) < 0))
126125imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → (𝑦𝑆) < 0)
127 resubcl 10626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦𝑆) ∈ ℝ)
128116, 118, 127syl2an 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (𝑦𝑆) ∈ ℝ)
129373ad2ant2 1157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (♯‘𝐹) ∈ ℝ)
130129adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (♯‘𝐹) ∈ ℝ)
131128, 130jca 503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((𝑦𝑆) ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ))
132131adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((𝑦𝑆) ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ))
133 ltaddneg 10532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((𝑦𝑆) ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ) → ((𝑦𝑆) < 0 ↔ ((♯‘𝐹) + (𝑦𝑆)) < (♯‘𝐹)))
134132, 133syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((𝑦𝑆) < 0 ↔ ((♯‘𝐹) + (𝑦𝑆)) < (♯‘𝐹)))
135126, 134mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((♯‘𝐹) + (𝑦𝑆)) < (♯‘𝐹))
136115, 135eqbrtrrd 4868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹))
137107, 108, 1363jca 1151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))
138137exp31 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) → ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
1391383adant2 1154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
14087, 139syl5bi 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (𝑆 ∈ (0..^(♯‘𝐹)) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
141140adantld 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
14231, 141sylbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (0..^(♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
143142impcom 396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹))))
144143impcom 396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))
145 elfzo0 12729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑦𝑆) + (♯‘𝐹)) ∈ (0..^(♯‘𝐹)) ↔ (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))
146144, 145sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((𝑦𝑆) + (♯‘𝐹)) ∈ (0..^(♯‘𝐹)))
147 oveq1 6877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 = ((𝑦𝑆) + (♯‘𝐹)) → (𝑧 + 𝑆) = (((𝑦𝑆) + (♯‘𝐹)) + 𝑆))
148147oveq1d 6885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 = ((𝑦𝑆) + (♯‘𝐹)) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = ((((𝑦𝑆) + (♯‘𝐹)) + 𝑆) mod (♯‘𝐹)))
14973adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑆 ∈ ℂ)
15075adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑦 ∈ ℂ)
151 nn0cn 11565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((♯‘𝐹) ∈ ℕ0 → (♯‘𝐹) ∈ ℂ)
152151ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ∈ ℂ)
153149, 150, 1523jca 1151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ))
154153adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ))
155 simp2 1160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → 𝑦 ∈ ℂ)
156 simp3 1161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → (♯‘𝐹) ∈ ℂ)
157 simp1 1159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → 𝑆 ∈ ℂ)
158155, 157, 156nppcand 10698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → (((𝑦𝑆) + (♯‘𝐹)) + 𝑆) = (𝑦 + (♯‘𝐹)))
159155, 156, 158comraddd 10531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → (((𝑦𝑆) + (♯‘𝐹)) + 𝑆) = ((♯‘𝐹) + 𝑦))
160154, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((𝑦𝑆) + (♯‘𝐹)) + 𝑆) = ((♯‘𝐹) + 𝑦))
161160oveq1d 6885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((((𝑦𝑆) + (♯‘𝐹)) + 𝑆) mod (♯‘𝐹)) = (((♯‘𝐹) + 𝑦) mod (♯‘𝐹)))
16231biimpi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 ∈ (0..^(♯‘𝐹)) → (𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)))
163162ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)))
164 addmodid 12938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (((♯‘𝐹) + 𝑦) mod (♯‘𝐹)) = 𝑦)
165163, 164syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((♯‘𝐹) + 𝑦) mod (♯‘𝐹)) = 𝑦)
166161, 165eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((((𝑦𝑆) + (♯‘𝐹)) + 𝑆) mod (♯‘𝐹)) = 𝑦)
167148, 166sylan9eqr 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ 𝑧 = ((𝑦𝑆) + (♯‘𝐹))) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = 𝑦)
168167eqcomd 2812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ 𝑧 = ((𝑦𝑆) + (♯‘𝐹))) → 𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
169146, 168rspcedeq2vd 3512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
17086, 169pm2.61ian 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
17123rexeqi 3332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)) ↔ ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
172170, 171sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
173172exp31 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((♯‘𝐹) ∈ ℕ0 → (𝑆 ∈ (0..^(♯‘𝐹)) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))))
17424, 173syl5bi 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((♯‘𝐹) ∈ ℕ0 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))))
17522, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 ∈ Word dom 𝐼 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))))
17620, 21, 1753syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹(Circuits‘𝐺)𝑃 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))))
1773, 5, 176sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))))
178177adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ dom 𝐼) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))))
179178imp 395 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
180179adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
181 fveq2 6404 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)) → (𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
182181reximi 3198 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
183180, 182syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
1843, 20, 213syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 ∈ Word dom 𝐼)
185184ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → 𝐹 ∈ Word dom 𝐼)
186 elfzoelz 12690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ)
1875, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑆 ∈ ℤ)
188187ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → 𝑆 ∈ ℤ)
18923eleq2i 2877 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ (0..^𝑁) ↔ 𝑧 ∈ (0..^(♯‘𝐹)))
190189biimpi 207 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ (0..^𝑁) → 𝑧 ∈ (0..^(♯‘𝐹)))
191 cshwidxmod 13769 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ Word dom 𝐼𝑆 ∈ ℤ ∧ 𝑧 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑧) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
192185, 188, 190, 191syl2an3an 1538 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) ∧ 𝑧 ∈ (0..^𝑁)) → ((𝐹 cyclShift 𝑆)‘𝑧) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
193192eqeq2d 2816 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) ∧ 𝑧 ∈ (0..^𝑁)) → ((𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧) ↔ (𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹)))))
194193rexbidva 3237 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧) ↔ ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹)))))
195183, 194mpbird 248 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧))
1961, 2, 3, 4, 5, 6crctcshlem2 26938 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (♯‘𝐻) = 𝑁)
197196oveq2d 6886 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁))
198197ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (0..^(♯‘𝐻)) = (0..^𝑁))
199 simpr 473 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → 𝑖 = (𝐹𝑦))
2006fveq1i 6405 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻𝑧) = ((𝐹 cyclShift 𝑆)‘𝑧)
201200a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (𝐻𝑧) = ((𝐹 cyclShift 𝑆)‘𝑧))
202199, 201eqeq12d 2821 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (𝑖 = (𝐻𝑧) ↔ (𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧)))
203198, 202rexeqbidv 3342 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧) ↔ ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧)))
204195, 203mpbird 248 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → ∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧))
205204ex 399 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑖 = (𝐹𝑦) → ∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
206205rexlimdva 3219 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ dom 𝐼) → (∃𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) → ∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
207206ralimdva 3150 . . . . . . . . . . . . . . . 16 (𝜑 → (∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) → ∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
208207impcom 396 . . . . . . . . . . . . . . 15 ((∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) ∧ 𝜑) → ∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧))
209208anim1i 604 . . . . . . . . . . . . . 14 (((∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) ∧ 𝜑) ∧ 𝐻:(0..^(♯‘𝐻))⟶dom 𝐼) → (∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧) ∧ 𝐻:(0..^(♯‘𝐻))⟶dom 𝐼))
210209ancomd 451 . . . . . . . . . . . . 13 (((∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) ∧ 𝜑) ∧ 𝐻:(0..^(♯‘𝐻))⟶dom 𝐼) → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
211 dffo3 6592 . . . . . . . . . . . . 13 (𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼 ↔ (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
212210, 211sylibr 225 . . . . . . . . . . . 12 (((∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) ∧ 𝜑) ∧ 𝐻:(0..^(♯‘𝐻))⟶dom 𝐼) → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)
213212exp31 408 . . . . . . . . . . 11 (∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) → (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
21419, 213simplbiim 495 . . . . . . . . . 10 (𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼 → (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
21518, 214simplbiim 495 . . . . . . . . 9 (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼 → (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
216215com13 88 . . . . . . . 8 (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 → (𝜑 → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
21717, 216syl 17 . . . . . . 7 (𝐻(Trails‘𝐺)𝑄 → (𝜑 → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
218217impcom 396 . . . . . 6 ((𝜑𝐻(Trails‘𝐺)𝑄) → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))
21913, 218mpd 15 . . . . 5 ((𝜑𝐻(Trails‘𝐺)𝑄) → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)
2209, 219jca 503 . . . 4 ((𝜑𝐻(Trails‘𝐺)𝑄) → (𝐻(Trails‘𝐺)𝑄𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))
2218, 220mpdan 670 . . 3 (𝜑 → (𝐻(Trails‘𝐺)𝑄𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))
2222iseupth 27373 . . 3 (𝐻(EulerPaths‘𝐺)𝑄 ↔ (𝐻(Trails‘𝐺)𝑄𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))
223221, 222sylibr 225 . 2 (𝜑𝐻(EulerPaths‘𝐺)𝑄)
2241, 2, 3, 4, 5, 6, 7crctcsh 26944 . 2 (𝜑𝐻(Circuits‘𝐺)𝑄)
225223, 224jca 503 1 (𝜑 → (𝐻(EulerPaths‘𝐺)𝑄𝐻(Circuits‘𝐺)𝑄))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wral 3096  wrex 3097  ifcif 4279   class class class wbr 4844  cmpt 4923  dom cdm 5311  wf 6093  1-1wf1 6094  ontowfo 6095  1-1-ontowf1o 6096  cfv 6097  (class class class)co 6870  cc 10215  cr 10216  0cc0 10217   + caddc 10220   < clt 10355  cle 10356  cmin 10547  cn 11301  0cn0 11555  cz 11639  ...cfz 12545  ..^cfzo 12685   mod cmo 12888  chash 13333  Word cword 13498   cyclShift ccsh 13754  Vtxcvtx 26087  iEdgciedg 26088  Walkscwlks 26719  Trailsctrls 26814  Circuitsccrcts 26907  EulerPathsceupth 27369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294  ax-pre-sup 10295
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-ifp 1079  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-1st 7394  df-2nd 7395  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-oadd 7796  df-er 7975  df-map 8090  df-pm 8091  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-sup 8583  df-inf 8584  df-card 9044  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-div 10966  df-nn 11302  df-2 11360  df-n0 11556  df-z 11640  df-uz 11901  df-rp 12043  df-ico 12395  df-fz 12546  df-fzo 12686  df-fl 12813  df-mod 12889  df-hash 13334  df-word 13506  df-concat 13508  df-substr 13510  df-csh 13755  df-wlks 26722  df-trls 26816  df-crcts 26909  df-eupth 27370
This theorem is referenced by:  eucrct2eupth  27417
  Copyright terms: Public domain W3C validator