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

Theorem wrdind 13409
Description: Perform induction over the structure of a word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
Hypotheses
Ref Expression
wrdind.1 (𝑥 = ∅ → (𝜑𝜓))
wrdind.2 (𝑥 = 𝑦 → (𝜑𝜒))
wrdind.3 (𝑥 = (𝑦 ++ ⟨“𝑧”⟩) → (𝜑𝜃))
wrdind.4 (𝑥 = 𝐴 → (𝜑𝜏))
wrdind.5 𝜓
wrdind.6 ((𝑦 ∈ Word 𝐵𝑧𝐵) → (𝜒𝜃))
Assertion
Ref Expression
wrdind (𝐴 ∈ Word 𝐵𝜏)
Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝑧,𝐵   𝜒,𝑥   𝜑,𝑦,𝑧   𝜏,𝑥   𝜃,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥,𝑦,𝑧)   𝜒(𝑦,𝑧)   𝜃(𝑦,𝑧)   𝜏(𝑦,𝑧)   𝐴(𝑦,𝑧)

Proof of Theorem wrdind
Dummy variables 𝑛 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lencl 13258 . . 3 (𝐴 ∈ Word 𝐵 → (#‘𝐴) ∈ ℕ0)
2 eqeq2 2637 . . . . . 6 (𝑛 = 0 → ((#‘𝑥) = 𝑛 ↔ (#‘𝑥) = 0))
32imbi1d 331 . . . . 5 (𝑛 = 0 → (((#‘𝑥) = 𝑛𝜑) ↔ ((#‘𝑥) = 0 → 𝜑)))
43ralbidv 2985 . . . 4 (𝑛 = 0 → (∀𝑥 ∈ Word 𝐵((#‘𝑥) = 𝑛𝜑) ↔ ∀𝑥 ∈ Word 𝐵((#‘𝑥) = 0 → 𝜑)))
5 eqeq2 2637 . . . . . 6 (𝑛 = 𝑚 → ((#‘𝑥) = 𝑛 ↔ (#‘𝑥) = 𝑚))
65imbi1d 331 . . . . 5 (𝑛 = 𝑚 → (((#‘𝑥) = 𝑛𝜑) ↔ ((#‘𝑥) = 𝑚𝜑)))
76ralbidv 2985 . . . 4 (𝑛 = 𝑚 → (∀𝑥 ∈ Word 𝐵((#‘𝑥) = 𝑛𝜑) ↔ ∀𝑥 ∈ Word 𝐵((#‘𝑥) = 𝑚𝜑)))
8 eqeq2 2637 . . . . . 6 (𝑛 = (𝑚 + 1) → ((#‘𝑥) = 𝑛 ↔ (#‘𝑥) = (𝑚 + 1)))
98imbi1d 331 . . . . 5 (𝑛 = (𝑚 + 1) → (((#‘𝑥) = 𝑛𝜑) ↔ ((#‘𝑥) = (𝑚 + 1) → 𝜑)))
109ralbidv 2985 . . . 4 (𝑛 = (𝑚 + 1) → (∀𝑥 ∈ Word 𝐵((#‘𝑥) = 𝑛𝜑) ↔ ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (𝑚 + 1) → 𝜑)))
11 eqeq2 2637 . . . . . 6 (𝑛 = (#‘𝐴) → ((#‘𝑥) = 𝑛 ↔ (#‘𝑥) = (#‘𝐴)))
1211imbi1d 331 . . . . 5 (𝑛 = (#‘𝐴) → (((#‘𝑥) = 𝑛𝜑) ↔ ((#‘𝑥) = (#‘𝐴) → 𝜑)))
1312ralbidv 2985 . . . 4 (𝑛 = (#‘𝐴) → (∀𝑥 ∈ Word 𝐵((#‘𝑥) = 𝑛𝜑) ↔ ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (#‘𝐴) → 𝜑)))
14 hasheq0 13091 . . . . . 6 (𝑥 ∈ Word 𝐵 → ((#‘𝑥) = 0 ↔ 𝑥 = ∅))
15 wrdind.5 . . . . . . 7 𝜓
16 wrdind.1 . . . . . . 7 (𝑥 = ∅ → (𝜑𝜓))
1715, 16mpbiri 248 . . . . . 6 (𝑥 = ∅ → 𝜑)
1814, 17syl6bi 243 . . . . 5 (𝑥 ∈ Word 𝐵 → ((#‘𝑥) = 0 → 𝜑))
1918rgen 2922 . . . 4 𝑥 ∈ Word 𝐵((#‘𝑥) = 0 → 𝜑)
20 fveq2 6150 . . . . . . . 8 (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦))
2120eqeq1d 2628 . . . . . . 7 (𝑥 = 𝑦 → ((#‘𝑥) = 𝑚 ↔ (#‘𝑦) = 𝑚))
22 wrdind.2 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜒))
2321, 22imbi12d 334 . . . . . 6 (𝑥 = 𝑦 → (((#‘𝑥) = 𝑚𝜑) ↔ ((#‘𝑦) = 𝑚𝜒)))
2423cbvralv 3164 . . . . 5 (∀𝑥 ∈ Word 𝐵((#‘𝑥) = 𝑚𝜑) ↔ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒))
25 swrdcl 13352 . . . . . . . . . . . 12 (𝑥 ∈ Word 𝐵 → (𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ∈ Word 𝐵)
2625ad2antrl 763 . . . . . . . . . . 11 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ∈ Word 𝐵)
27 simplr 791 . . . . . . . . . . 11 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒))
28 simprl 793 . . . . . . . . . . . . 13 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝑥 ∈ Word 𝐵)
29 fzossfz 12426 . . . . . . . . . . . . . 14 (0..^(#‘𝑥)) ⊆ (0...(#‘𝑥))
30 simprr 795 . . . . . . . . . . . . . . . 16 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (#‘𝑥) = (𝑚 + 1))
31 nn0p1nn 11277 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ0 → (𝑚 + 1) ∈ ℕ)
3231ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (𝑚 + 1) ∈ ℕ)
3330, 32eqeltrd 2704 . . . . . . . . . . . . . . 15 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (#‘𝑥) ∈ ℕ)
34 fzo0end 12498 . . . . . . . . . . . . . . 15 ((#‘𝑥) ∈ ℕ → ((#‘𝑥) − 1) ∈ (0..^(#‘𝑥)))
3533, 34syl 17 . . . . . . . . . . . . . 14 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ((#‘𝑥) − 1) ∈ (0..^(#‘𝑥)))
3629, 35sseldi 3586 . . . . . . . . . . . . 13 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ((#‘𝑥) − 1) ∈ (0...(#‘𝑥)))
37 swrd0len 13355 . . . . . . . . . . . . 13 ((𝑥 ∈ Word 𝐵 ∧ ((#‘𝑥) − 1) ∈ (0...(#‘𝑥))) → (#‘(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩)) = ((#‘𝑥) − 1))
3828, 36, 37syl2anc 692 . . . . . . . . . . . 12 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (#‘(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩)) = ((#‘𝑥) − 1))
3930oveq1d 6620 . . . . . . . . . . . 12 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ((#‘𝑥) − 1) = ((𝑚 + 1) − 1))
40 nn0cn 11247 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0𝑚 ∈ ℂ)
4140ad2antrr 761 . . . . . . . . . . . . 13 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝑚 ∈ ℂ)
42 ax-1cn 9939 . . . . . . . . . . . . 13 1 ∈ ℂ
43 pncan 10232 . . . . . . . . . . . . 13 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
4441, 42, 43sylancl 693 . . . . . . . . . . . 12 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ((𝑚 + 1) − 1) = 𝑚)
4538, 39, 443eqtrd 2664 . . . . . . . . . . 11 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (#‘(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩)) = 𝑚)
46 fveq2 6150 . . . . . . . . . . . . . 14 (𝑦 = (𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) → (#‘𝑦) = (#‘(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩)))
4746eqeq1d 2628 . . . . . . . . . . . . 13 (𝑦 = (𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) → ((#‘𝑦) = 𝑚 ↔ (#‘(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩)) = 𝑚))
48 vex 3194 . . . . . . . . . . . . . . 15 𝑦 ∈ V
4948, 22sbcie 3457 . . . . . . . . . . . . . 14 ([𝑦 / 𝑥]𝜑𝜒)
50 dfsbcq 3424 . . . . . . . . . . . . . 14 (𝑦 = (𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) → ([𝑦 / 𝑥]𝜑[(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) / 𝑥]𝜑))
5149, 50syl5bbr 274 . . . . . . . . . . . . 13 (𝑦 = (𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) → (𝜒[(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) / 𝑥]𝜑))
5247, 51imbi12d 334 . . . . . . . . . . . 12 (𝑦 = (𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) → (((#‘𝑦) = 𝑚𝜒) ↔ ((#‘(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩)) = 𝑚[(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) / 𝑥]𝜑)))
5352rspcv 3296 . . . . . . . . . . 11 ((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ∈ Word 𝐵 → (∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒) → ((#‘(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩)) = 𝑚[(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) / 𝑥]𝜑)))
5426, 27, 45, 53syl3c 66 . . . . . . . . . 10 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → [(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) / 𝑥]𝜑)
5533nnge1d 11008 . . . . . . . . . . . . 13 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 1 ≤ (#‘𝑥))
56 wrdlenge1n0 13274 . . . . . . . . . . . . . 14 (𝑥 ∈ Word 𝐵 → (𝑥 ≠ ∅ ↔ 1 ≤ (#‘𝑥)))
5756ad2antrl 763 . . . . . . . . . . . . 13 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (𝑥 ≠ ∅ ↔ 1 ≤ (#‘𝑥)))
5855, 57mpbird 247 . . . . . . . . . . . 12 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝑥 ≠ ∅)
59 lswcl 13289 . . . . . . . . . . . 12 ((𝑥 ∈ Word 𝐵𝑥 ≠ ∅) → ( lastS ‘𝑥) ∈ 𝐵)
6028, 58, 59syl2anc 692 . . . . . . . . . . 11 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ( lastS ‘𝑥) ∈ 𝐵)
61 oveq1 6612 . . . . . . . . . . . . . 14 (𝑦 = (𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) → (𝑦 ++ ⟨“𝑧”⟩) = ((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“𝑧”⟩))
6261sbceq1d 3427 . . . . . . . . . . . . 13 (𝑦 = (𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) → ([(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑[((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“𝑧”⟩) / 𝑥]𝜑))
6350, 62imbi12d 334 . . . . . . . . . . . 12 (𝑦 = (𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) → (([𝑦 / 𝑥]𝜑[(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑) ↔ ([(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) / 𝑥]𝜑[((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“𝑧”⟩) / 𝑥]𝜑)))
64 s1eq 13314 . . . . . . . . . . . . . . 15 (𝑧 = ( lastS ‘𝑥) → ⟨“𝑧”⟩ = ⟨“( lastS ‘𝑥)”⟩)
6564oveq2d 6621 . . . . . . . . . . . . . 14 (𝑧 = ( lastS ‘𝑥) → ((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“𝑧”⟩) = ((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“( lastS ‘𝑥)”⟩))
6665sbceq1d 3427 . . . . . . . . . . . . 13 (𝑧 = ( lastS ‘𝑥) → ([((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“𝑧”⟩) / 𝑥]𝜑[((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“( lastS ‘𝑥)”⟩) / 𝑥]𝜑))
6766imbi2d 330 . . . . . . . . . . . 12 (𝑧 = ( lastS ‘𝑥) → (([(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) / 𝑥]𝜑[((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“𝑧”⟩) / 𝑥]𝜑) ↔ ([(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) / 𝑥]𝜑[((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“( lastS ‘𝑥)”⟩) / 𝑥]𝜑)))
68 wrdind.6 . . . . . . . . . . . . 13 ((𝑦 ∈ Word 𝐵𝑧𝐵) → (𝜒𝜃))
69 ovex 6633 . . . . . . . . . . . . . 14 (𝑦 ++ ⟨“𝑧”⟩) ∈ V
70 wrdind.3 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 ++ ⟨“𝑧”⟩) → (𝜑𝜃))
7169, 70sbcie 3457 . . . . . . . . . . . . 13 ([(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑𝜃)
7268, 49, 713imtr4g 285 . . . . . . . . . . . 12 ((𝑦 ∈ Word 𝐵𝑧𝐵) → ([𝑦 / 𝑥]𝜑[(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑))
7363, 67, 72vtocl2ga 3265 . . . . . . . . . . 11 (((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ∈ Word 𝐵 ∧ ( lastS ‘𝑥) ∈ 𝐵) → ([(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) / 𝑥]𝜑[((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“( lastS ‘𝑥)”⟩) / 𝑥]𝜑))
7426, 60, 73syl2anc 692 . . . . . . . . . 10 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ([(𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) / 𝑥]𝜑[((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“( lastS ‘𝑥)”⟩) / 𝑥]𝜑))
7554, 74mpd 15 . . . . . . . . 9 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → [((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“( lastS ‘𝑥)”⟩) / 𝑥]𝜑)
76 wrdfin 13257 . . . . . . . . . . . . . 14 (𝑥 ∈ Word 𝐵𝑥 ∈ Fin)
7776ad2antrl 763 . . . . . . . . . . . . 13 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝑥 ∈ Fin)
78 hashnncl 13094 . . . . . . . . . . . . 13 (𝑥 ∈ Fin → ((#‘𝑥) ∈ ℕ ↔ 𝑥 ≠ ∅))
7977, 78syl 17 . . . . . . . . . . . 12 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → ((#‘𝑥) ∈ ℕ ↔ 𝑥 ≠ ∅))
8033, 79mpbid 222 . . . . . . . . . . 11 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝑥 ≠ ∅)
81 swrdccatwrd 13401 . . . . . . . . . . . 12 ((𝑥 ∈ Word 𝐵𝑥 ≠ ∅) → ((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“( lastS ‘𝑥)”⟩) = 𝑥)
8281eqcomd 2632 . . . . . . . . . . 11 ((𝑥 ∈ Word 𝐵𝑥 ≠ ∅) → 𝑥 = ((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“( lastS ‘𝑥)”⟩))
8328, 80, 82syl2anc 692 . . . . . . . . . 10 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝑥 = ((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“( lastS ‘𝑥)”⟩))
84 sbceq1a 3433 . . . . . . . . . 10 (𝑥 = ((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“( lastS ‘𝑥)”⟩) → (𝜑[((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“( lastS ‘𝑥)”⟩) / 𝑥]𝜑))
8583, 84syl 17 . . . . . . . . 9 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → (𝜑[((𝑥 substr ⟨0, ((#‘𝑥) − 1)⟩) ++ ⟨“( lastS ‘𝑥)”⟩) / 𝑥]𝜑))
8675, 85mpbird 247 . . . . . . . 8 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (#‘𝑥) = (𝑚 + 1))) → 𝜑)
8786expr 642 . . . . . . 7 (((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) ∧ 𝑥 ∈ Word 𝐵) → ((#‘𝑥) = (𝑚 + 1) → 𝜑))
8887ralrimiva 2965 . . . . . 6 ((𝑚 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒)) → ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (𝑚 + 1) → 𝜑))
8988ex 450 . . . . 5 (𝑚 ∈ ℕ0 → (∀𝑦 ∈ Word 𝐵((#‘𝑦) = 𝑚𝜒) → ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (𝑚 + 1) → 𝜑)))
9024, 89syl5bi 232 . . . 4 (𝑚 ∈ ℕ0 → (∀𝑥 ∈ Word 𝐵((#‘𝑥) = 𝑚𝜑) → ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (𝑚 + 1) → 𝜑)))
914, 7, 10, 13, 19, 90nn0ind 11416 . . 3 ((#‘𝐴) ∈ ℕ0 → ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (#‘𝐴) → 𝜑))
921, 91syl 17 . 2 (𝐴 ∈ Word 𝐵 → ∀𝑥 ∈ Word 𝐵((#‘𝑥) = (#‘𝐴) → 𝜑))
93 eqidd 2627 . 2 (𝐴 ∈ Word 𝐵 → (#‘𝐴) = (#‘𝐴))
94 fveq2 6150 . . . . 5 (𝑥 = 𝐴 → (#‘𝑥) = (#‘𝐴))
9594eqeq1d 2628 . . . 4 (𝑥 = 𝐴 → ((#‘𝑥) = (#‘𝐴) ↔ (#‘𝐴) = (#‘𝐴)))
96 wrdind.4 . . . 4 (𝑥 = 𝐴 → (𝜑𝜏))
9795, 96imbi12d 334 . . 3 (𝑥 = 𝐴 → (((#‘𝑥) = (#‘𝐴) → 𝜑) ↔ ((#‘𝐴) = (#‘𝐴) → 𝜏)))
9897rspcv 3296 . 2 (𝐴 ∈ Word 𝐵 → (∀𝑥 ∈ Word 𝐵((#‘𝑥) = (#‘𝐴) → 𝜑) → ((#‘𝐴) = (#‘𝐴) → 𝜏)))
9992, 93, 98mp2d 49 1 (𝐴 ∈ Word 𝐵𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1992  wne 2796  wral 2912  [wsbc 3422  c0 3896  cop 4159   class class class wbr 4618  cfv 5850  (class class class)co 6605  Fincfn 7900  cc 9879  0cc0 9881  1c1 9882   + caddc 9884  cle 10020  cmin 10211  cn 10965  0cn0 11237  ...cfz 12265  ..^cfzo 12403  #chash 13054  Word cword 13225   lastS clsw 13226   ++ cconcat 13227  ⟨“cs1 13228   substr csubstr 13229
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-oadd 7510  df-er 7688  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-card 8710  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-nn 10966  df-n0 11238  df-xnn0 11309  df-z 11323  df-uz 11632  df-fz 12266  df-fzo 12404  df-hash 13055  df-word 13233  df-lsw 13234  df-concat 13235  df-s1 13236  df-substr 13237
This theorem is referenced by:  frmdgsum  17315  gsumwrev  17712  gsmsymgrfix  17764  efginvrel2  18056  signstfvneq0  30421  signstfvc  30423  mrsubvrs  31119
  Copyright terms: Public domain W3C validator