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

Theorem eucrctshift 30271
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 29852 . . . 4 (𝜑𝐻(Trails‘𝐺)𝑄)
9 simpr 484 . . . . 5 ((𝜑𝐻(Trails‘𝐺)𝑄) → 𝐻(Trails‘𝐺)𝑄)
10 eucrctshift.e . . . . . . . 8 (𝜑𝐹(EulerPaths‘𝐺)𝑃)
112eupthf1o 30232 . . . . . . . 8 (𝐹(EulerPaths‘𝐺)𝑃𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼)
1210, 11syl 17 . . . . . . 7 (𝜑𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼)
1312adantr 480 . . . . . 6 ((𝜑𝐻(Trails‘𝐺)𝑄) → 𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼)
14 trliswlk 29729 . . . . . . . 8 (𝐻(Trails‘𝐺)𝑄𝐻(Walks‘𝐺)𝑄)
152wlkf 29646 . . . . . . . 8 (𝐻(Walks‘𝐺)𝑄𝐻 ∈ Word dom 𝐼)
16 wrdf 14553 . . . . . . . 8 (𝐻 ∈ Word dom 𝐼𝐻:(0..^(♯‘𝐻))⟶dom 𝐼)
17 df-f1o 6569 . . . . . . . . . 10 (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼 ↔ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼))
18 dffo3 7121 . . . . . . . . . . 11 (𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼 ↔ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦)))
19 crctiswlk 29828 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹(Circuits‘𝐺)𝑃𝐹(Walks‘𝐺)𝑃)
202wlkf 29646 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹(Walks‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
21 lencl 14567 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 ∈ Word dom 𝐼 → (♯‘𝐹) ∈ ℕ0)
224oveq2i 7441 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0..^𝑁) = (0..^(♯‘𝐹))
2322eleq2i 2830 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑆 ∈ (0..^𝑁) ↔ 𝑆 ∈ (0..^(♯‘𝐹)))
24 elfzonn0 13743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑆 ∈ ℕ0)
2524adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → 𝑆 ∈ ℕ0)
26 elfzonn0 13743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 ∈ (0..^(♯‘𝐹)) → 𝑦 ∈ ℕ0)
27 nn0sub 12573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑆 ∈ ℕ0𝑦 ∈ ℕ0) → (𝑆𝑦 ↔ (𝑦𝑆) ∈ ℕ0))
2825, 26, 27syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑆𝑦 ↔ (𝑦𝑆) ∈ ℕ0))
2928biimpac 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦𝑆) ∈ ℕ0)
30 elfzo0 13736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 ∈ (0..^(♯‘𝐹)) ↔ (𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)))
31 simp2 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (♯‘𝐹) ∈ ℕ)
3230, 31sylbi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℕ)
3332ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (♯‘𝐹) ∈ ℕ)
34 nn0re 12532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑦 ∈ ℕ0𝑦 ∈ ℝ)
3534ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → 𝑦 ∈ ℝ)
36 nnre 12270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((♯‘𝐹) ∈ ℕ → (♯‘𝐹) ∈ ℝ)
3736adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) → (♯‘𝐹) ∈ ℝ)
3837adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ∈ ℝ)
39 elfzoelz 13695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑆 ∈ ℤ)
4039zred 12719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑆 ∈ ℝ)
41 readdcl 11235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((♯‘𝐹) ∈ ℝ ∧ 𝑆 ∈ ℝ) → ((♯‘𝐹) + 𝑆) ∈ ℝ)
4237, 40, 41syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → ((♯‘𝐹) + 𝑆) ∈ ℝ)
4335, 38, 423jca 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦 ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ ∧ ((♯‘𝐹) + 𝑆) ∈ ℝ))
44 elfzole1 13703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑆 ∈ (0..^(♯‘𝐹)) → 0 ≤ 𝑆)
4544adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → 0 ≤ 𝑆)
46 addge01 11770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((♯‘𝐹) ∈ ℝ ∧ 𝑆 ∈ ℝ) → (0 ≤ 𝑆 ↔ (♯‘𝐹) ≤ ((♯‘𝐹) + 𝑆)))
4737, 40, 46syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (0 ≤ 𝑆 ↔ (♯‘𝐹) ≤ ((♯‘𝐹) + 𝑆)))
4845, 47mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ≤ ((♯‘𝐹) + 𝑆))
4943, 48lelttrdi 11420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦 < (♯‘𝐹) → 𝑦 < ((♯‘𝐹) + 𝑆)))
5049ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) → (𝑆 ∈ (0..^(♯‘𝐹)) → (𝑦 < (♯‘𝐹) → 𝑦 < ((♯‘𝐹) + 𝑆))))
5150com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) → (𝑦 < (♯‘𝐹) → (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑦 < ((♯‘𝐹) + 𝑆))))
52513impia 1116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑦 < ((♯‘𝐹) + 𝑆)))
5352adantld 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → 𝑦 < ((♯‘𝐹) + 𝑆)))
5453imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → 𝑦 < ((♯‘𝐹) + 𝑆))
55343ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → 𝑦 ∈ ℝ)
5655adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → 𝑦 ∈ ℝ)
5740ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → 𝑆 ∈ ℝ)
58 elfzoel2 13694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑆 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℤ)
5958zred 12719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑆 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℝ)
6059ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → (♯‘𝐹) ∈ ℝ)
6156, 57, 60ltsubaddd 11856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → ((𝑦𝑆) < (♯‘𝐹) ↔ 𝑦 < ((♯‘𝐹) + 𝑆)))
6254, 61mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) ∧ ((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹)))) → (𝑦𝑆) < (♯‘𝐹))
6362ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦𝑆) < (♯‘𝐹)))
6430, 63sylbi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 ∈ (0..^(♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦𝑆) < (♯‘𝐹)))
6564impcom 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑦𝑆) < (♯‘𝐹))
6665adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦𝑆) < (♯‘𝐹))
67 elfzo0 13736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑦𝑆) ∈ (0..^(♯‘𝐹)) ↔ ((𝑦𝑆) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑦𝑆) < (♯‘𝐹)))
6829, 33, 66, 67syl3anbrc 1342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦𝑆) ∈ (0..^(♯‘𝐹)))
69 oveq1 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = (𝑦𝑆) → (𝑧 + 𝑆) = ((𝑦𝑆) + 𝑆))
7069oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = (𝑦𝑆) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = (((𝑦𝑆) + 𝑆) mod (♯‘𝐹)))
7139zcnd 12720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑆 ∈ (0..^(♯‘𝐹)) → 𝑆 ∈ ℂ)
7271adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → 𝑆 ∈ ℂ)
73 elfzoelz 13695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 ∈ (0..^(♯‘𝐹)) → 𝑦 ∈ ℤ)
7473zcnd 12720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ (0..^(♯‘𝐹)) → 𝑦 ∈ ℂ)
7572, 74anim12ci 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ))
7675adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ))
77 npcan 11514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ) → ((𝑦𝑆) + 𝑆) = 𝑦)
7876, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((𝑦𝑆) + 𝑆) = 𝑦)
7978oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((𝑦𝑆) + 𝑆) mod (♯‘𝐹)) = (𝑦 mod (♯‘𝐹)))
80 zmodidfzoimp 13937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 ∈ (0..^(♯‘𝐹)) → (𝑦 mod (♯‘𝐹)) = 𝑦)
8180ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦 mod (♯‘𝐹)) = 𝑦)
8279, 81eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((𝑦𝑆) + 𝑆) mod (♯‘𝐹)) = 𝑦)
8370, 82sylan9eqr 2796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ 𝑧 = (𝑦𝑆)) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = 𝑦)
8483eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ 𝑧 = (𝑦𝑆)) → 𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
8568, 84rspcedeq2vd 3629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
86 elfzo0 13736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑆 ∈ (0..^(♯‘𝐹)) ↔ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)))
87 nn0cn 12533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑦 ∈ ℕ0𝑦 ∈ ℂ)
8887ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → 𝑦 ∈ ℂ)
89 nn0cn 12533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑆 ∈ ℕ0𝑆 ∈ ℂ)
90893ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → 𝑆 ∈ ℂ)
9190adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → 𝑆 ∈ ℂ)
92 nncn 12271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((♯‘𝐹) ∈ ℕ → (♯‘𝐹) ∈ ℂ)
93923ad2ant2 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (♯‘𝐹) ∈ ℂ)
9493adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (♯‘𝐹) ∈ ℂ)
9588, 91, 94subadd23d 11639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((𝑦𝑆) + (♯‘𝐹)) = (𝑦 + ((♯‘𝐹) − 𝑆)))
96 simpll 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → 𝑦 ∈ ℕ0)
97 nn0z 12635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑆 ∈ ℕ0𝑆 ∈ ℤ)
98 nnz 12631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((♯‘𝐹) ∈ ℕ → (♯‘𝐹) ∈ ℤ)
99 znnsub 12660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑆 ∈ ℤ ∧ (♯‘𝐹) ∈ ℤ) → (𝑆 < (♯‘𝐹) ↔ ((♯‘𝐹) − 𝑆) ∈ ℕ))
10097, 98, 99syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ) → (𝑆 < (♯‘𝐹) ↔ ((♯‘𝐹) − 𝑆) ∈ ℕ))
101100biimp3a 1468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → ((♯‘𝐹) − 𝑆) ∈ ℕ)
102101adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((♯‘𝐹) − 𝑆) ∈ ℕ)
103102nnnn0d 12584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((♯‘𝐹) − 𝑆) ∈ ℕ0)
10496, 103nn0addcld 12588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (𝑦 + ((♯‘𝐹) − 𝑆)) ∈ ℕ0)
10595, 104eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0)
106105adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0)
107 simplr2 1215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → (♯‘𝐹) ∈ ℕ)
10887adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) → 𝑦 ∈ ℂ)
109 subcl 11504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑦𝑆) ∈ ℂ)
110108, 90, 109syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (𝑦𝑆) ∈ ℂ)
11194, 110jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((♯‘𝐹) ∈ ℂ ∧ (𝑦𝑆) ∈ ℂ))
112111adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((♯‘𝐹) ∈ ℂ ∧ (𝑦𝑆) ∈ ℂ))
113 addcom 11444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((♯‘𝐹) ∈ ℂ ∧ (𝑦𝑆) ∈ ℂ) → ((♯‘𝐹) + (𝑦𝑆)) = ((𝑦𝑆) + (♯‘𝐹)))
114112, 113syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((♯‘𝐹) + (𝑦𝑆)) = ((𝑦𝑆) + (♯‘𝐹)))
11534adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) → 𝑦 ∈ ℝ)
116 nn0re 12532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑆 ∈ ℕ0𝑆 ∈ ℝ)
1171163ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → 𝑆 ∈ ℝ)
118 ltnle 11337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦 < 𝑆 ↔ ¬ 𝑆𝑦))
119 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → 𝑦 ∈ ℝ)
120 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ ℝ)
121119, 120sublt0d 11886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → ((𝑦𝑆) < 0 ↔ 𝑦 < 𝑆))
122121biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦 < 𝑆 → (𝑦𝑆) < 0))
123118, 122sylbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (¬ 𝑆𝑦 → (𝑦𝑆) < 0))
124115, 117, 123syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (¬ 𝑆𝑦 → (𝑦𝑆) < 0))
125124imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → (𝑦𝑆) < 0)
126 resubcl 11570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦𝑆) ∈ ℝ)
127115, 117, 126syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (𝑦𝑆) ∈ ℝ)
128363ad2ant2 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (♯‘𝐹) ∈ ℝ)
129128adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (♯‘𝐹) ∈ ℝ)
130127, 129jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((𝑦𝑆) ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ))
131130adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((𝑦𝑆) ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ))
132 ltaddneg 11474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑦𝑆) ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ) → ((𝑦𝑆) < 0 ↔ ((♯‘𝐹) + (𝑦𝑆)) < (♯‘𝐹)))
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((𝑦𝑆) < 0 ↔ ((♯‘𝐹) + (𝑦𝑆)) < (♯‘𝐹)))
134125, 133mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((♯‘𝐹) + (𝑦𝑆)) < (♯‘𝐹))
135114, 134eqbrtrrd 5171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹))
136106, 107, 1353jca 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆𝑦) → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))
137136exp31 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑦 ∈ ℕ0𝑦 < (♯‘𝐹)) → ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
1381373adant2 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → ((𝑆 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
13986, 138biimtrid 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (𝑆 ∈ (0..^(♯‘𝐹)) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
140139adantld 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
14130, 140sylbi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 ∈ (0..^(♯‘𝐹)) → (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))))
142141impcom 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (¬ 𝑆𝑦 → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹))))
143142impcom 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))
144 elfzo0 13736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑦𝑆) + (♯‘𝐹)) ∈ (0..^(♯‘𝐹)) ↔ (((𝑦𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ ((𝑦𝑆) + (♯‘𝐹)) < (♯‘𝐹)))
145143, 144sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((𝑦𝑆) + (♯‘𝐹)) ∈ (0..^(♯‘𝐹)))
146 oveq1 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = ((𝑦𝑆) + (♯‘𝐹)) → (𝑧 + 𝑆) = (((𝑦𝑆) + (♯‘𝐹)) + 𝑆))
147146oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = ((𝑦𝑆) + (♯‘𝐹)) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = ((((𝑦𝑆) + (♯‘𝐹)) + 𝑆) mod (♯‘𝐹)))
14872adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑆 ∈ ℂ)
14974adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑦 ∈ ℂ)
150 nn0cn 12533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((♯‘𝐹) ∈ ℕ0 → (♯‘𝐹) ∈ ℂ)
151150ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ∈ ℂ)
152148, 149, 1513jca 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ))
153152adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ))
154 simp2 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → 𝑦 ∈ ℂ)
155 simp3 1137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → (♯‘𝐹) ∈ ℂ)
156 simp1 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → 𝑆 ∈ ℂ)
157154, 156, 155nppcand 11642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → (((𝑦𝑆) + (♯‘𝐹)) + 𝑆) = (𝑦 + (♯‘𝐹)))
158154, 155, 157comraddd 11472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈ ℂ) → (((𝑦𝑆) + (♯‘𝐹)) + 𝑆) = ((♯‘𝐹) + 𝑦))
159153, 158syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((𝑦𝑆) + (♯‘𝐹)) + 𝑆) = ((♯‘𝐹) + 𝑦))
160159oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((((𝑦𝑆) + (♯‘𝐹)) + 𝑆) mod (♯‘𝐹)) = (((♯‘𝐹) + 𝑦) mod (♯‘𝐹)))
16130biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (0..^(♯‘𝐹)) → (𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)))
162161ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)))
163 addmodid 13956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦 ∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹)) → (((♯‘𝐹) + 𝑦) mod (♯‘𝐹)) = 𝑦)
164162, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (((♯‘𝐹) + 𝑦) mod (♯‘𝐹)) = 𝑦)
165160, 164eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((((𝑦𝑆) + (♯‘𝐹)) + 𝑆) mod (♯‘𝐹)) = 𝑦)
166147, 165sylan9eqr 2796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ 𝑧 = ((𝑦𝑆) + (♯‘𝐹))) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = 𝑦)
167166eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ 𝑧 = ((𝑦𝑆) + (♯‘𝐹))) → 𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
168145, 167rspcedeq2vd 3629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((¬ 𝑆𝑦 ∧ (((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
16985, 168pm2.61ian 812 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
17022rexeqi 3322 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)) ↔ ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
171169, 170sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((♯‘𝐹) ∈ ℕ0𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
172171exp31 419 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((♯‘𝐹) ∈ ℕ0 → (𝑆 ∈ (0..^(♯‘𝐹)) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))))
17323, 172biimtrid 242 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((♯‘𝐹) ∈ ℕ0 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))))
17419, 20, 21, 1734syl 19 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹(Circuits‘𝐺)𝑃 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))))
1753, 5, 174sylc 65 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))))
176175adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ dom 𝐼) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))))
177176imp 406 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
178177adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))
179 fveq2 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)) → (𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
180179reximi 3081 . . . . . . . . . . . . . . . . . . . 20 (∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
181178, 180syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
1823, 19, 203syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹 ∈ Word dom 𝐼)
183182ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → 𝐹 ∈ Word dom 𝐼)
184 elfzoelz 13695 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ)
1855, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑆 ∈ ℤ)
186185ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → 𝑆 ∈ ℤ)
18722eleq2i 2830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (0..^𝑁) ↔ 𝑧 ∈ (0..^(♯‘𝐹)))
188187biimpi 216 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (0..^𝑁) → 𝑧 ∈ (0..^(♯‘𝐹)))
189 cshwidxmod 14837 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ Word dom 𝐼𝑆 ∈ ℤ ∧ 𝑧 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑧) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
190183, 186, 188, 189syl2an3an 1421 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) ∧ 𝑧 ∈ (0..^𝑁)) → ((𝐹 cyclShift 𝑆)‘𝑧) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))
191190eqeq2d 2745 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) ∧ 𝑧 ∈ (0..^𝑁)) → ((𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧) ↔ (𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹)))))
192191rexbidva 3174 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧) ↔ ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹)))))
193181, 192mpbird 257 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧))
1941, 2, 3, 4, 5, 6crctcshlem2 29847 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (♯‘𝐻) = 𝑁)
195194oveq2d 7446 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁))
196195ad3antrrr 730 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (0..^(♯‘𝐻)) = (0..^𝑁))
197 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → 𝑖 = (𝐹𝑦))
1986fveq1i 6907 . . . . . . . . . . . . . . . . . . . . 21 (𝐻𝑧) = ((𝐹 cyclShift 𝑆)‘𝑧)
199198a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (𝐻𝑧) = ((𝐹 cyclShift 𝑆)‘𝑧))
200197, 199eqeq12d 2750 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (𝑖 = (𝐻𝑧) ↔ (𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧)))
201196, 200rexeqbidv 3344 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → (∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧) ↔ ∃𝑧 ∈ (0..^𝑁)(𝐹𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧)))
202193, 201mpbird 257 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹𝑦)) → ∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧))
203202rexlimdva2 3154 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ dom 𝐼) → (∃𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) → ∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
204203ralimdva 3164 . . . . . . . . . . . . . . 15 (𝜑 → (∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) → ∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
205204impcom 407 . . . . . . . . . . . . . 14 ((∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) ∧ 𝜑) → ∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧))
206205anim1ci 616 . . . . . . . . . . . . 13 (((∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) ∧ 𝜑) ∧ 𝐻:(0..^(♯‘𝐻))⟶dom 𝐼) → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
207 dffo3 7121 . . . . . . . . . . . . 13 (𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼 ↔ (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻𝑧)))
208206, 207sylibr 234 . . . . . . . . . . . 12 (((∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) ∧ 𝜑) ∧ 𝐻:(0..^(♯‘𝐻))⟶dom 𝐼) → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)
209208exp31 419 . . . . . . . . . . 11 (∀𝑖 ∈ dom 𝐼𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹𝑦) → (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
21018, 209simplbiim 504 . . . . . . . . . 10 (𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼 → (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
21117, 210simplbiim 504 . . . . . . . . 9 (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼 → (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
212211com13 88 . . . . . . . 8 (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 → (𝜑 → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
21314, 15, 16, 2124syl 19 . . . . . . 7 (𝐻(Trails‘𝐺)𝑄 → (𝜑 → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)))
214213impcom 407 . . . . . 6 ((𝜑𝐻(Trails‘𝐺)𝑄) → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))
21513, 214mpd 15 . . . . 5 ((𝜑𝐻(Trails‘𝐺)𝑄) → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)
2169, 215jca 511 . . . 4 ((𝜑𝐻(Trails‘𝐺)𝑄) → (𝐻(Trails‘𝐺)𝑄𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))
2178, 216mpdan 687 . . 3 (𝜑 → (𝐻(Trails‘𝐺)𝑄𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))
2182iseupth 30229 . . 3 (𝐻(EulerPaths‘𝐺)𝑄 ↔ (𝐻(Trails‘𝐺)𝑄𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))
219217, 218sylibr 234 . 2 (𝜑𝐻(EulerPaths‘𝐺)𝑄)
2201, 2, 3, 4, 5, 6, 7crctcsh 29853 . 2 (𝜑𝐻(Circuits‘𝐺)𝑄)
221219, 220jca 511 1 (𝜑 → (𝐻(EulerPaths‘𝐺)𝑄𝐻(Circuits‘𝐺)𝑄))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wral 3058  wrex 3067  ifcif 4530   class class class wbr 5147  cmpt 5230  dom cdm 5688  wf 6558  1-1wf1 6559  ontowfo 6560  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  cc 11150  cr 11151  0cc0 11152   + caddc 11155   < clt 11292  cle 11293  cmin 11489  cn 12263  0cn0 12523  cz 12610  ...cfz 13543  ..^cfzo 13690   mod cmo 13905  chash 14365  Word cword 14548   cyclShift ccsh 14822  Vtxcvtx 29027  iEdgciedg 29028  Walkscwlks 29628  Trailsctrls 29722  Circuitsccrcts 29816  EulerPathsceupth 30225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ifp 1063  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-ico 13389  df-fz 13544  df-fzo 13691  df-fl 13828  df-mod 13906  df-hash 14366  df-word 14549  df-concat 14605  df-substr 14675  df-pfx 14705  df-csh 14823  df-wlks 29631  df-trls 29724  df-crcts 29818  df-eupth 30226
This theorem is referenced by:  eucrct2eupth  30273
  Copyright terms: Public domain W3C validator