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

Theorem efgsp1 18078
Description: If 𝐹 is an extension sequence and 𝐴 is an extension of the last element of 𝐹, then 𝐹 + ⟨“𝐴”⟩ is an extension sequence. (Contributed by Mario Carneiro, 1-Oct-2015.)
Hypotheses
Ref Expression
efgval.w 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
efgval.r = ( ~FG𝐼)
efgval2.m 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
efgval2.t 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
efgred.d 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
efgred.s 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1)))
Assertion
Ref Expression
efgsp1 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ dom 𝑆)
Distinct variable groups:   𝑦,𝑧   𝑡,𝑛,𝑣,𝑤,𝑦,𝑧,𝑚,𝑥   𝑚,𝑀   𝑥,𝑛,𝑀,𝑡,𝑣,𝑤   𝑘,𝑚,𝑡,𝑥,𝑇   𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥   ,𝑚,𝑡,𝑥,𝑦,𝑧   𝑚,𝐼,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝐷,𝑚,𝑡
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛)   (𝑤,𝑣,𝑘,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑇(𝑦,𝑧,𝑤,𝑣,𝑛)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐼(𝑘)   𝑀(𝑦,𝑧,𝑘)

Proof of Theorem efgsp1
Dummy variables 𝑎 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efgval.w . . . . . . . 8 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
2 efgval.r . . . . . . . 8 = ( ~FG𝐼)
3 efgval2.m . . . . . . . 8 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
4 efgval2.t . . . . . . . 8 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
5 efgred.d . . . . . . . 8 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
6 efgred.s . . . . . . . 8 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1)))
71, 2, 3, 4, 5, 6efgsdm 18071 . . . . . . 7 (𝐹 ∈ dom 𝑆 ↔ (𝐹 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐹‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
87simp1bi 1074 . . . . . 6 (𝐹 ∈ dom 𝑆𝐹 ∈ (Word 𝑊 ∖ {∅}))
98adantr 481 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐹 ∈ (Word 𝑊 ∖ {∅}))
109eldifad 3571 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐹 ∈ Word 𝑊)
111, 2, 3, 4, 5, 6efgsf 18070 . . . . . . . . . . . 12 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
1211fdmi 6014 . . . . . . . . . . . . 13 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
1312feq2i 5999 . . . . . . . . . . . 12 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
1411, 13mpbir 221 . . . . . . . . . . 11 𝑆:dom 𝑆𝑊
1514ffvelrni 6319 . . . . . . . . . 10 (𝐹 ∈ dom 𝑆 → (𝑆𝐹) ∈ 𝑊)
1615adantr 481 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑆𝐹) ∈ 𝑊)
171, 2, 3, 4efgtf 18063 . . . . . . . . 9 ((𝑆𝐹) ∈ 𝑊 → ((𝑇‘(𝑆𝐹)) = (𝑎 ∈ (0...(#‘(𝑆𝐹))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐹) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐹)):((0...(#‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊))
1816, 17syl 17 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝑇‘(𝑆𝐹)) = (𝑎 ∈ (0...(#‘(𝑆𝐹))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐹) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐹)):((0...(#‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊))
1918simprd 479 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑇‘(𝑆𝐹)):((0...(#‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊)
20 frn 6015 . . . . . . 7 ((𝑇‘(𝑆𝐹)):((0...(#‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊 → ran (𝑇‘(𝑆𝐹)) ⊆ 𝑊)
2119, 20syl 17 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ran (𝑇‘(𝑆𝐹)) ⊆ 𝑊)
22 simpr 477 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐴 ∈ ran (𝑇‘(𝑆𝐹)))
2321, 22sseldd 3588 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐴𝑊)
2423s1cld 13329 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ⟨“𝐴”⟩ ∈ Word 𝑊)
25 ccatcl 13305 . . . 4 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) → (𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊)
2610, 24, 25syl2anc 692 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊)
27 ccatlen 13306 . . . . . . 7 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) → (#‘(𝐹 ++ ⟨“𝐴”⟩)) = ((#‘𝐹) + (#‘⟨“𝐴”⟩)))
2810, 24, 27syl2anc 692 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (#‘(𝐹 ++ ⟨“𝐴”⟩)) = ((#‘𝐹) + (#‘⟨“𝐴”⟩)))
29 s1len 13331 . . . . . . 7 (#‘⟨“𝐴”⟩) = 1
3029oveq2i 6621 . . . . . 6 ((#‘𝐹) + (#‘⟨“𝐴”⟩)) = ((#‘𝐹) + 1)
3128, 30syl6eq 2671 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (#‘(𝐹 ++ ⟨“𝐴”⟩)) = ((#‘𝐹) + 1))
32 lencl 13270 . . . . . 6 (𝐹 ∈ Word 𝑊 → (#‘𝐹) ∈ ℕ0)
33 nn0p1nn 11283 . . . . . 6 ((#‘𝐹) ∈ ℕ0 → ((#‘𝐹) + 1) ∈ ℕ)
3410, 32, 333syl 18 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((#‘𝐹) + 1) ∈ ℕ)
3531, 34eqeltrd 2698 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (#‘(𝐹 ++ ⟨“𝐴”⟩)) ∈ ℕ)
36 wrdfin 13269 . . . . 5 ((𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊 → (𝐹 ++ ⟨“𝐴”⟩) ∈ Fin)
37 hashnncl 13104 . . . . 5 ((𝐹 ++ ⟨“𝐴”⟩) ∈ Fin → ((#‘(𝐹 ++ ⟨“𝐴”⟩)) ∈ ℕ ↔ (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅))
3826, 36, 373syl 18 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((#‘(𝐹 ++ ⟨“𝐴”⟩)) ∈ ℕ ↔ (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅))
3935, 38mpbid 222 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅)
40 eldifsn 4292 . . 3 ((𝐹 ++ ⟨“𝐴”⟩) ∈ (Word 𝑊 ∖ {∅}) ↔ ((𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊 ∧ (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅))
4126, 39, 40sylanbrc 697 . 2 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ (Word 𝑊 ∖ {∅}))
42 eldifsni 4294 . . . . . . 7 (𝐹 ∈ (Word 𝑊 ∖ {∅}) → 𝐹 ≠ ∅)
439, 42syl 17 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐹 ≠ ∅)
44 wrdfin 13269 . . . . . . 7 (𝐹 ∈ Word 𝑊𝐹 ∈ Fin)
45 hashnncl 13104 . . . . . . 7 (𝐹 ∈ Fin → ((#‘𝐹) ∈ ℕ ↔ 𝐹 ≠ ∅))
4610, 44, 453syl 18 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((#‘𝐹) ∈ ℕ ↔ 𝐹 ≠ ∅))
4743, 46mpbird 247 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (#‘𝐹) ∈ ℕ)
48 lbfzo0 12455 . . . . 5 (0 ∈ (0..^(#‘𝐹)) ↔ (#‘𝐹) ∈ ℕ)
4947, 48sylibr 224 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 0 ∈ (0..^(#‘𝐹)))
50 ccatval1 13307 . . . 4 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ 0 ∈ (0..^(#‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘0) = (𝐹‘0))
5110, 24, 49, 50syl3anc 1323 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘0) = (𝐹‘0))
527simp2bi 1075 . . . 4 (𝐹 ∈ dom 𝑆 → (𝐹‘0) ∈ 𝐷)
5352adantr 481 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹‘0) ∈ 𝐷)
5451, 53eqeltrd 2698 . 2 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘0) ∈ 𝐷)
557simp3bi 1076 . . . . . 6 (𝐹 ∈ dom 𝑆 → ∀𝑖 ∈ (1..^(#‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))
5655adantr 481 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ (1..^(#‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))
57 fzo0ss1 12446 . . . . . . . . . . 11 (1..^(#‘𝐹)) ⊆ (0..^(#‘𝐹))
5857sseli 3583 . . . . . . . . . 10 (𝑖 ∈ (1..^(#‘𝐹)) → 𝑖 ∈ (0..^(#‘𝐹)))
59 ccatval1 13307 . . . . . . . . . 10 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (0..^(#‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) = (𝐹𝑖))
6058, 59syl3an3 1358 . . . . . . . . 9 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(#‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) = (𝐹𝑖))
61 elfzoel2 12417 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1..^(#‘𝐹)) → (#‘𝐹) ∈ ℤ)
62 peano2zm 11371 . . . . . . . . . . . . . . . 16 ((#‘𝐹) ∈ ℤ → ((#‘𝐹) − 1) ∈ ℤ)
6361, 62syl 17 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1..^(#‘𝐹)) → ((#‘𝐹) − 1) ∈ ℤ)
6461zred 11433 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1..^(#‘𝐹)) → (#‘𝐹) ∈ ℝ)
6564lem1d 10908 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1..^(#‘𝐹)) → ((#‘𝐹) − 1) ≤ (#‘𝐹))
66 eluz2 11644 . . . . . . . . . . . . . . 15 ((#‘𝐹) ∈ (ℤ‘((#‘𝐹) − 1)) ↔ (((#‘𝐹) − 1) ∈ ℤ ∧ (#‘𝐹) ∈ ℤ ∧ ((#‘𝐹) − 1) ≤ (#‘𝐹)))
6763, 61, 65, 66syl3anbrc 1244 . . . . . . . . . . . . . 14 (𝑖 ∈ (1..^(#‘𝐹)) → (#‘𝐹) ∈ (ℤ‘((#‘𝐹) − 1)))
68 fzoss2 12444 . . . . . . . . . . . . . 14 ((#‘𝐹) ∈ (ℤ‘((#‘𝐹) − 1)) → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹)))
6967, 68syl 17 . . . . . . . . . . . . 13 (𝑖 ∈ (1..^(#‘𝐹)) → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹)))
70 elfzoelz 12418 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1..^(#‘𝐹)) → 𝑖 ∈ ℤ)
71 elfzom1b 12515 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℤ ∧ (#‘𝐹) ∈ ℤ) → (𝑖 ∈ (1..^(#‘𝐹)) ↔ (𝑖 − 1) ∈ (0..^((#‘𝐹) − 1))))
7270, 61, 71syl2anc 692 . . . . . . . . . . . . . 14 (𝑖 ∈ (1..^(#‘𝐹)) → (𝑖 ∈ (1..^(#‘𝐹)) ↔ (𝑖 − 1) ∈ (0..^((#‘𝐹) − 1))))
7372ibi 256 . . . . . . . . . . . . 13 (𝑖 ∈ (1..^(#‘𝐹)) → (𝑖 − 1) ∈ (0..^((#‘𝐹) − 1)))
7469, 73sseldd 3588 . . . . . . . . . . . 12 (𝑖 ∈ (1..^(#‘𝐹)) → (𝑖 − 1) ∈ (0..^(#‘𝐹)))
75 ccatval1 13307 . . . . . . . . . . . 12 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ (𝑖 − 1) ∈ (0..^(#‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)) = (𝐹‘(𝑖 − 1)))
7674, 75syl3an3 1358 . . . . . . . . . . 11 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(#‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)) = (𝐹‘(𝑖 − 1)))
7776fveq2d 6157 . . . . . . . . . 10 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(#‘𝐹))) → (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = (𝑇‘(𝐹‘(𝑖 − 1))))
7877rneqd 5318 . . . . . . . . 9 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(#‘𝐹))) → ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = ran (𝑇‘(𝐹‘(𝑖 − 1))))
7960, 78eleq12d 2692 . . . . . . . 8 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(#‘𝐹))) → (((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ (𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
80793expa 1262 . . . . . . 7 (((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) ∧ 𝑖 ∈ (1..^(#‘𝐹))) → (((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ (𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
8180ralbidva 2980 . . . . . 6 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) → (∀𝑖 ∈ (1..^(#‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ (1..^(#‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
8210, 24, 81syl2anc 692 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (∀𝑖 ∈ (1..^(#‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ (1..^(#‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
8356, 82mpbird 247 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ (1..^(#‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
8410, 32syl 17 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (#‘𝐹) ∈ ℕ0)
8584nn0cnd 11304 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (#‘𝐹) ∈ ℂ)
8685addid2d 10188 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (0 + (#‘𝐹)) = (#‘𝐹))
8786fveq2d 6157 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(0 + (#‘𝐹))) = ((𝐹 ++ ⟨“𝐴”⟩)‘(#‘𝐹)))
88 1nn 10982 . . . . . . . . . . 11 1 ∈ ℕ
8929, 88eqeltri 2694 . . . . . . . . . 10 (#‘⟨“𝐴”⟩) ∈ ℕ
9089a1i 11 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (#‘⟨“𝐴”⟩) ∈ ℕ)
91 lbfzo0 12455 . . . . . . . . 9 (0 ∈ (0..^(#‘⟨“𝐴”⟩)) ↔ (#‘⟨“𝐴”⟩) ∈ ℕ)
9290, 91sylibr 224 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 0 ∈ (0..^(#‘⟨“𝐴”⟩)))
93 ccatval3 13309 . . . . . . . 8 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ 0 ∈ (0..^(#‘⟨“𝐴”⟩))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(0 + (#‘𝐹))) = (⟨“𝐴”⟩‘0))
9410, 24, 92, 93syl3anc 1323 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(0 + (#‘𝐹))) = (⟨“𝐴”⟩‘0))
9587, 94eqtr3d 2657 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(#‘𝐹)) = (⟨“𝐴”⟩‘0))
96 s1fv 13336 . . . . . . . 8 (𝐴 ∈ ran (𝑇‘(𝑆𝐹)) → (⟨“𝐴”⟩‘0) = 𝐴)
9796adantl 482 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (⟨“𝐴”⟩‘0) = 𝐴)
98 fzo0end 12508 . . . . . . . . . . . 12 ((#‘𝐹) ∈ ℕ → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹)))
9947, 98syl 17 . . . . . . . . . . 11 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹)))
100 ccatval1 13307 . . . . . . . . . . 11 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘((#‘𝐹) − 1)) = (𝐹‘((#‘𝐹) − 1)))
10110, 24, 99, 100syl3anc 1323 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘((#‘𝐹) − 1)) = (𝐹‘((#‘𝐹) − 1)))
1021, 2, 3, 4, 5, 6efgsval 18072 . . . . . . . . . . 11 (𝐹 ∈ dom 𝑆 → (𝑆𝐹) = (𝐹‘((#‘𝐹) − 1)))
103102adantr 481 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑆𝐹) = (𝐹‘((#‘𝐹) − 1)))
104101, 103eqtr4d 2658 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘((#‘𝐹) − 1)) = (𝑆𝐹))
105104fveq2d 6157 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((#‘𝐹) − 1))) = (𝑇‘(𝑆𝐹)))
106105rneqd 5318 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((#‘𝐹) − 1))) = ran (𝑇‘(𝑆𝐹)))
10722, 97, 1063eltr4d 2713 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (⟨“𝐴”⟩‘0) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((#‘𝐹) − 1))))
10895, 107eqeltrd 2698 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(#‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((#‘𝐹) − 1))))
109 fvex 6163 . . . . . 6 (#‘𝐹) ∈ V
110 fveq2 6153 . . . . . . 7 (𝑖 = (#‘𝐹) → ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) = ((𝐹 ++ ⟨“𝐴”⟩)‘(#‘𝐹)))
111 oveq1 6617 . . . . . . . . . 10 (𝑖 = (#‘𝐹) → (𝑖 − 1) = ((#‘𝐹) − 1))
112111fveq2d 6157 . . . . . . . . 9 (𝑖 = (#‘𝐹) → ((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)) = ((𝐹 ++ ⟨“𝐴”⟩)‘((#‘𝐹) − 1)))
113112fveq2d 6157 . . . . . . . 8 (𝑖 = (#‘𝐹) → (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((#‘𝐹) − 1))))
114113rneqd 5318 . . . . . . 7 (𝑖 = (#‘𝐹) → ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((#‘𝐹) − 1))))
115110, 114eleq12d 2692 . . . . . 6 (𝑖 = (#‘𝐹) → (((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ((𝐹 ++ ⟨“𝐴”⟩)‘(#‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((#‘𝐹) − 1)))))
116109, 115ralsn 4198 . . . . 5 (∀𝑖 ∈ {(#‘𝐹)} ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ((𝐹 ++ ⟨“𝐴”⟩)‘(#‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((#‘𝐹) − 1))))
117108, 116sylibr 224 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ {(#‘𝐹)} ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
118 ralunb 3777 . . . 4 (∀𝑖 ∈ ((1..^(#‘𝐹)) ∪ {(#‘𝐹)})((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ (∀𝑖 ∈ (1..^(#‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ∧ ∀𝑖 ∈ {(#‘𝐹)} ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)))))
11983, 117, 118sylanbrc 697 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ ((1..^(#‘𝐹)) ∪ {(#‘𝐹)})((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
12031oveq2d 6626 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (1..^(#‘(𝐹 ++ ⟨“𝐴”⟩))) = (1..^((#‘𝐹) + 1)))
121 nnuz 11674 . . . . . . 7 ℕ = (ℤ‘1)
12247, 121syl6eleq 2708 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (#‘𝐹) ∈ (ℤ‘1))
123 fzosplitsn 12524 . . . . . 6 ((#‘𝐹) ∈ (ℤ‘1) → (1..^((#‘𝐹) + 1)) = ((1..^(#‘𝐹)) ∪ {(#‘𝐹)}))
124122, 123syl 17 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (1..^((#‘𝐹) + 1)) = ((1..^(#‘𝐹)) ∪ {(#‘𝐹)}))
125120, 124eqtrd 2655 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (1..^(#‘(𝐹 ++ ⟨“𝐴”⟩))) = ((1..^(#‘𝐹)) ∪ {(#‘𝐹)}))
126125raleqdv 3136 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (∀𝑖 ∈ (1..^(#‘(𝐹 ++ ⟨“𝐴”⟩)))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ ((1..^(#‘𝐹)) ∪ {(#‘𝐹)})((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)))))
127119, 126mpbird 247 . 2 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ (1..^(#‘(𝐹 ++ ⟨“𝐴”⟩)))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
1281, 2, 3, 4, 5, 6efgsdm 18071 . 2 ((𝐹 ++ ⟨“𝐴”⟩) ∈ dom 𝑆 ↔ ((𝐹 ++ ⟨“𝐴”⟩) ∈ (Word 𝑊 ∖ {∅}) ∧ ((𝐹 ++ ⟨“𝐴”⟩)‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘(𝐹 ++ ⟨“𝐴”⟩)))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)))))
12941, 54, 127, 128syl3anbrc 1244 1 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ dom 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  {crab 2911  cdif 3556  cun 3557  wss 3559  c0 3896  {csn 4153  cop 4159  cotp 4161   ciun 4490   class class class wbr 4618  cmpt 4678   I cid 4989   × cxp 5077  dom cdm 5079  ran crn 5080  wf 5848  cfv 5852  (class class class)co 6610  cmpt2 6612  1𝑜c1o 7505  2𝑜c2o 7506  Fincfn 7906  0cc0 9887  1c1 9888   + caddc 9890  cle 10026  cmin 10217  cn 10971  0cn0 11243  cz 11328  cuz 11638  ...cfz 12275  ..^cfzo 12413  #chash 13064  Word cword 13237   ++ cconcat 13239  ⟨“cs1 13240   splice csplice 13242  ⟨“cs2 13530   ~FG cefg 18047
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 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964
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 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-ot 4162  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 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-card 8716  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-nn 10972  df-n0 11244  df-z 11329  df-uz 11639  df-fz 12276  df-fzo 12414  df-hash 13065  df-word 13245  df-concat 13247  df-s1 13248  df-substr 13249  df-splice 13250  df-s2 13537
This theorem is referenced by:  efgsfo  18080  efgredlemd  18085  efgrelexlemb  18091
  Copyright terms: Public domain W3C validator