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

Theorem efgcpbllemb 18089
Description: Lemma for efgrelex 18085. Show that 𝐿 is an equivalence relation containing all direct extensions of a word, so is closed under . (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)))
efgcpbllem.1 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ((𝐴 ++ 𝑗) ++ 𝐵))}
Assertion
Ref Expression
efgcpbllemb ((𝐴𝑊𝐵𝑊) → 𝐿)
Distinct variable groups:   𝑖,𝑗,𝐴   𝑦,𝑧   𝑡,𝑛,𝑣,𝑤,𝑦,𝑧   𝑖,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑀,𝑗   𝑖,𝑘,𝑇,𝑗,𝑚,𝑡,𝑥   𝑦,𝑖,𝑧,𝑊,𝑗   𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥   ,𝑖,𝑗,𝑚,𝑡,𝑥,𝑦,𝑧   𝐵,𝑖,𝑗   𝑆,𝑖,𝑗   𝑖,𝐼,𝑗,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝐷,𝑖,𝑗,𝑚,𝑡
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛)   (𝑤,𝑣,𝑘,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑇(𝑦,𝑧,𝑤,𝑣,𝑛)   𝐼(𝑘)   𝐿(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑖,𝑗,𝑘,𝑚,𝑛)   𝑀(𝑦,𝑧,𝑘)

Proof of Theorem efgcpbllemb
Dummy variables 𝑎 𝑏 𝑐 𝑓 𝑔 𝑟 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efgval.w . . 3 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
2 efgval.r . . 3 = ( ~FG𝐼)
3 efgval2.m . . 3 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
4 efgval2.t . . 3 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
51, 2, 3, 4efgval2 18058 . 2 = {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)}
6 efgcpbllem.1 . . . . . . 7 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ((𝐴 ++ 𝑗) ++ 𝐵))}
76relopabi 5205 . . . . . 6 Rel 𝐿
87a1i 11 . . . . 5 ((𝐴𝑊𝐵𝑊) → Rel 𝐿)
9 efgred.d . . . . . . . . 9 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
10 efgred.s . . . . . . . . 9 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1)))
111, 2, 3, 4, 9, 10, 6efgcpbllema 18088 . . . . . . . 8 (𝑓𝐿𝑔 ↔ (𝑓𝑊𝑔𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑔) ++ 𝐵)))
1211simp2bi 1075 . . . . . . 7 (𝑓𝐿𝑔𝑔𝑊)
1312adantl 482 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝐿𝑔) → 𝑔𝑊)
1411simp1bi 1074 . . . . . . 7 (𝑓𝐿𝑔𝑓𝑊)
1514adantl 482 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝐿𝑔) → 𝑓𝑊)
161, 2efger 18052 . . . . . . . 8 Er 𝑊
1716a1i 11 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝐿𝑔) → Er 𝑊)
1811simp3bi 1076 . . . . . . . 8 (𝑓𝐿𝑔 → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑔) ++ 𝐵))
1918adantl 482 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑔) ++ 𝐵))
2017, 19ersym 7699 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑔) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵))
211, 2, 3, 4, 9, 10, 6efgcpbllema 18088 . . . . . 6 (𝑔𝐿𝑓 ↔ (𝑔𝑊𝑓𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)))
2213, 15, 20, 21syl3anbrc 1244 . . . . 5 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝐿𝑔) → 𝑔𝐿𝑓)
2314ad2antrl 763 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → 𝑓𝑊)
241, 2, 3, 4, 9, 10, 6efgcpbllema 18088 . . . . . . . 8 (𝑔𝐿 ↔ (𝑔𝑊𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ((𝐴 ++ ) ++ 𝐵)))
2524simp2bi 1075 . . . . . . 7 (𝑔𝐿𝑊)
2625ad2antll 764 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → 𝑊)
2716a1i 11 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → Er 𝑊)
2818ad2antrl 763 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑔) ++ 𝐵))
2924simp3bi 1076 . . . . . . . 8 (𝑔𝐿 → ((𝐴 ++ 𝑔) ++ 𝐵) ((𝐴 ++ ) ++ 𝐵))
3029ad2antll 764 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → ((𝐴 ++ 𝑔) ++ 𝐵) ((𝐴 ++ ) ++ 𝐵))
3127, 28, 30ertrd 7703 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ ) ++ 𝐵))
321, 2, 3, 4, 9, 10, 6efgcpbllema 18088 . . . . . 6 (𝑓𝐿 ↔ (𝑓𝑊𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ ) ++ 𝐵)))
3323, 26, 31, 32syl3anbrc 1244 . . . . 5 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → 𝑓𝐿)
3416a1i 11 . . . . . . . . 9 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → Er 𝑊)
35 fviss 6213 . . . . . . . . . . . . . 14 ( I ‘Word (𝐼 × 2𝑜)) ⊆ Word (𝐼 × 2𝑜)
361, 35eqsstri 3614 . . . . . . . . . . . . 13 𝑊 ⊆ Word (𝐼 × 2𝑜)
37 simpll 789 . . . . . . . . . . . . 13 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝐴𝑊)
3836, 37sseldi 3581 . . . . . . . . . . . 12 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝐴 ∈ Word (𝐼 × 2𝑜))
39 simpr 477 . . . . . . . . . . . . 13 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝑓𝑊)
4036, 39sseldi 3581 . . . . . . . . . . . 12 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝑓 ∈ Word (𝐼 × 2𝑜))
41 ccatcl 13298 . . . . . . . . . . . 12 ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ 𝑓 ∈ Word (𝐼 × 2𝑜)) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2𝑜))
4238, 40, 41syl2anc 692 . . . . . . . . . . 11 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2𝑜))
43 simplr 791 . . . . . . . . . . . 12 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝐵𝑊)
4436, 43sseldi 3581 . . . . . . . . . . 11 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝐵 ∈ Word (𝐼 × 2𝑜))
45 ccatcl 13298 . . . . . . . . . . 11 (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2𝑜) ∧ 𝐵 ∈ Word (𝐼 × 2𝑜)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2𝑜))
4642, 44, 45syl2anc 692 . . . . . . . . . 10 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2𝑜))
471efgrcl 18049 . . . . . . . . . . . 12 (𝐴𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2𝑜)))
4847simprd 479 . . . . . . . . . . 11 (𝐴𝑊𝑊 = Word (𝐼 × 2𝑜))
4948ad2antrr 761 . . . . . . . . . 10 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝑊 = Word (𝐼 × 2𝑜))
5046, 49eleqtrrd 2701 . . . . . . . . 9 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊)
5134, 50erref 7707 . . . . . . . 8 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵))
5251ex 450 . . . . . . 7 ((𝐴𝑊𝐵𝑊) → (𝑓𝑊 → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)))
5352pm4.71d 665 . . . . . 6 ((𝐴𝑊𝐵𝑊) → (𝑓𝑊 ↔ (𝑓𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵))))
541, 2, 3, 4, 9, 10, 6efgcpbllema 18088 . . . . . . 7 (𝑓𝐿𝑓 ↔ (𝑓𝑊𝑓𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)))
55 df-3an 1038 . . . . . . 7 ((𝑓𝑊𝑓𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ ((𝑓𝑊𝑓𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)))
56 anidm 675 . . . . . . . 8 ((𝑓𝑊𝑓𝑊) ↔ 𝑓𝑊)
5756anbi1i 730 . . . . . . 7 (((𝑓𝑊𝑓𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ (𝑓𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)))
5854, 55, 573bitri 286 . . . . . 6 (𝑓𝐿𝑓 ↔ (𝑓𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)))
5953, 58syl6bbr 278 . . . . 5 ((𝐴𝑊𝐵𝑊) → (𝑓𝑊𝑓𝐿𝑓))
608, 22, 33, 59iserd 7713 . . . 4 ((𝐴𝑊𝐵𝑊) → 𝐿 Er 𝑊)
611, 2, 3, 4efgtf 18056 . . . . . . . . . 10 (𝑓𝑊 → ((𝑇𝑓) = (𝑎 ∈ (0...(#‘𝑓)), 𝑏 ∈ (𝐼 × 2𝑜) ↦ (𝑓 splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀𝑏)”⟩⟩)) ∧ (𝑇𝑓):((0...(#‘𝑓)) × (𝐼 × 2𝑜))⟶𝑊))
6261simprd 479 . . . . . . . . 9 (𝑓𝑊 → (𝑇𝑓):((0...(#‘𝑓)) × (𝐼 × 2𝑜))⟶𝑊)
6362adantl 482 . . . . . . . 8 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → (𝑇𝑓):((0...(#‘𝑓)) × (𝐼 × 2𝑜))⟶𝑊)
64 ffn 6002 . . . . . . . 8 ((𝑇𝑓):((0...(#‘𝑓)) × (𝐼 × 2𝑜))⟶𝑊 → (𝑇𝑓) Fn ((0...(#‘𝑓)) × (𝐼 × 2𝑜)))
65 ovelrn 6763 . . . . . . . 8 ((𝑇𝑓) Fn ((0...(#‘𝑓)) × (𝐼 × 2𝑜)) → (𝑎 ∈ ran (𝑇𝑓) ↔ ∃𝑐 ∈ (0...(#‘𝑓))∃𝑢 ∈ (𝐼 × 2𝑜)𝑎 = (𝑐(𝑇𝑓)𝑢)))
6663, 64, 653syl 18 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → (𝑎 ∈ ran (𝑇𝑓) ↔ ∃𝑐 ∈ (0...(#‘𝑓))∃𝑢 ∈ (𝐼 × 2𝑜)𝑎 = (𝑐(𝑇𝑓)𝑢)))
67 simplr 791 . . . . . . . . . 10 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 𝑓𝑊)
6862ad2antlr 762 . . . . . . . . . . 11 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝑇𝑓):((0...(#‘𝑓)) × (𝐼 × 2𝑜))⟶𝑊)
69 simprl 793 . . . . . . . . . . 11 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 𝑐 ∈ (0...(#‘𝑓)))
70 simprr 795 . . . . . . . . . . 11 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 𝑢 ∈ (𝐼 × 2𝑜))
7168, 69, 70fovrnd 6759 . . . . . . . . . 10 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝑐(𝑇𝑓)𝑢) ∈ 𝑊)
7250adantr 481 . . . . . . . . . . 11 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊)
7337adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 𝐴𝑊)
7436, 73sseldi 3581 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 𝐴 ∈ Word (𝐼 × 2𝑜))
7540adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 𝑓 ∈ Word (𝐼 × 2𝑜))
76 swrdcl 13357 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ Word (𝐼 × 2𝑜) → (𝑓 substr ⟨0, 𝑐⟩) ∈ Word (𝐼 × 2𝑜))
7775, 76syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝑓 substr ⟨0, 𝑐⟩) ∈ Word (𝐼 × 2𝑜))
78 ccatcl 13298 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr ⟨0, 𝑐⟩) ∈ Word (𝐼 × 2𝑜)) → (𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ∈ Word (𝐼 × 2𝑜))
7974, 77, 78syl2anc 692 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ∈ Word (𝐼 × 2𝑜))
803efgmf 18047 . . . . . . . . . . . . . . . . . 18 𝑀:(𝐼 × 2𝑜)⟶(𝐼 × 2𝑜)
8180ffvelrni 6314 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ (𝐼 × 2𝑜) → (𝑀𝑢) ∈ (𝐼 × 2𝑜))
8281ad2antll 764 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝑀𝑢) ∈ (𝐼 × 2𝑜))
8370, 82s2cld 13552 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ⟨“𝑢(𝑀𝑢)”⟩ ∈ Word (𝐼 × 2𝑜))
84 ccatcl 13298 . . . . . . . . . . . . . . 15 (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“𝑢(𝑀𝑢)”⟩ ∈ Word (𝐼 × 2𝑜)) → ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ∈ Word (𝐼 × 2𝑜))
8579, 83, 84syl2anc 692 . . . . . . . . . . . . . 14 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ∈ Word (𝐼 × 2𝑜))
86 swrdcl 13357 . . . . . . . . . . . . . . 15 (𝑓 ∈ Word (𝐼 × 2𝑜) → (𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ∈ Word (𝐼 × 2𝑜))
8775, 86syl 17 . . . . . . . . . . . . . 14 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ∈ Word (𝐼 × 2𝑜))
8844adantr 481 . . . . . . . . . . . . . 14 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 𝐵 ∈ Word (𝐼 × 2𝑜))
89 ccatass 13310 . . . . . . . . . . . . . 14 ((((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝐵 ∈ Word (𝐼 × 2𝑜)) → ((((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) ++ 𝐵) = (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ++ 𝐵)))
9085, 87, 88, 89syl3anc 1323 . . . . . . . . . . . . 13 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) ++ 𝐵) = (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ++ 𝐵)))
91 ccatcl 13298 . . . . . . . . . . . . . . . . 17 (((𝑓 substr ⟨0, 𝑐⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“𝑢(𝑀𝑢)”⟩ ∈ Word (𝐼 × 2𝑜)) → ((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩) ∈ Word (𝐼 × 2𝑜))
9277, 83, 91syl2anc 692 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩) ∈ Word (𝐼 × 2𝑜))
93 ccatass 13310 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ ((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩) ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ∈ Word (𝐼 × 2𝑜)) → ((𝐴 ++ ((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) = (𝐴 ++ (((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩))))
9474, 92, 87, 93syl3anc 1323 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝐴 ++ ((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) = (𝐴 ++ (((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩))))
95 ccatass 13310 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr ⟨0, 𝑐⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“𝑢(𝑀𝑢)”⟩ ∈ Word (𝐼 × 2𝑜)) → ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) = (𝐴 ++ ((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩)))
9674, 77, 83, 95syl3anc 1323 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) = (𝐴 ++ ((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩)))
9796oveq1d 6619 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) = ((𝐴 ++ ((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)))
981, 2, 3, 4efgtval 18057 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑊𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜)) → (𝑐(𝑇𝑓)𝑢) = (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀𝑢)”⟩⟩))
9967, 69, 70, 98syl3anc 1323 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝑐(𝑇𝑓)𝑢) = (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀𝑢)”⟩⟩))
100 splval 13439 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑊 ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑐 ∈ (0...(#‘𝑓)) ∧ ⟨“𝑢(𝑀𝑢)”⟩ ∈ Word (𝐼 × 2𝑜))) → (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀𝑢)”⟩⟩) = (((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)))
10167, 69, 69, 83, 100syl13anc 1325 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀𝑢)”⟩⟩) = (((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)))
10299, 101eqtrd 2655 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝑐(𝑇𝑓)𝑢) = (((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)))
103102oveq2d 6620 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝐴 ++ (𝑐(𝑇𝑓)𝑢)) = (𝐴 ++ (((𝑓 substr ⟨0, 𝑐⟩) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩))))
10494, 97, 1033eqtr4rd 2666 . . . . . . . . . . . . . 14 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝐴 ++ (𝑐(𝑇𝑓)𝑢)) = (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)))
105104oveq1d 6619 . . . . . . . . . . . . 13 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵) = ((((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) ++ 𝐵))
106 lencl 13263 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ Word (𝐼 × 2𝑜) → (#‘𝐴) ∈ ℕ0)
10774, 106syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘𝐴) ∈ ℕ0)
108 nn0uz 11666 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘0)
109107, 108syl6eleq 2708 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘𝐴) ∈ (ℤ‘0))
110 elfznn0 12374 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ (0...(#‘𝑓)) → 𝑐 ∈ ℕ0)
111110ad2antrl 763 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 𝑐 ∈ ℕ0)
112 uzaddcl 11688 . . . . . . . . . . . . . . . . 17 (((#‘𝐴) ∈ (ℤ‘0) ∧ 𝑐 ∈ ℕ0) → ((#‘𝐴) + 𝑐) ∈ (ℤ‘0))
113109, 111, 112syl2anc 692 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((#‘𝐴) + 𝑐) ∈ (ℤ‘0))
11442adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2𝑜))
115 ccatlen 13299 . . . . . . . . . . . . . . . . . 18 (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2𝑜) ∧ 𝐵 ∈ Word (𝐼 × 2𝑜)) → (#‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((#‘(𝐴 ++ 𝑓)) + (#‘𝐵)))
116114, 88, 115syl2anc 692 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((#‘(𝐴 ++ 𝑓)) + (#‘𝐵)))
117 ccatlen 13299 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ 𝑓 ∈ Word (𝐼 × 2𝑜)) → (#‘(𝐴 ++ 𝑓)) = ((#‘𝐴) + (#‘𝑓)))
11874, 75, 117syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘(𝐴 ++ 𝑓)) = ((#‘𝐴) + (#‘𝑓)))
119 elfzuz3 12281 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ (0...(#‘𝑓)) → (#‘𝑓) ∈ (ℤ𝑐))
120119ad2antrl 763 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘𝑓) ∈ (ℤ𝑐))
121107nn0zd 11424 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘𝐴) ∈ ℤ)
122 eluzadd 11660 . . . . . . . . . . . . . . . . . . . . 21 (((#‘𝑓) ∈ (ℤ𝑐) ∧ (#‘𝐴) ∈ ℤ) → ((#‘𝑓) + (#‘𝐴)) ∈ (ℤ‘(𝑐 + (#‘𝐴))))
123120, 121, 122syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((#‘𝑓) + (#‘𝐴)) ∈ (ℤ‘(𝑐 + (#‘𝐴))))
124 lencl 13263 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ Word (𝐼 × 2𝑜) → (#‘𝑓) ∈ ℕ0)
12575, 124syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘𝑓) ∈ ℕ0)
126125nn0cnd 11297 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘𝑓) ∈ ℂ)
127107nn0cnd 11297 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘𝐴) ∈ ℂ)
128126, 127addcomd 10182 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((#‘𝑓) + (#‘𝐴)) = ((#‘𝐴) + (#‘𝑓)))
129111nn0cnd 11297 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 𝑐 ∈ ℂ)
130129, 127addcomd 10182 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝑐 + (#‘𝐴)) = ((#‘𝐴) + 𝑐))
131130fveq2d 6152 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (ℤ‘(𝑐 + (#‘𝐴))) = (ℤ‘((#‘𝐴) + 𝑐)))
132123, 128, 1313eltr3d 2712 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((#‘𝐴) + (#‘𝑓)) ∈ (ℤ‘((#‘𝐴) + 𝑐)))
133118, 132eqeltrd 2698 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘(𝐴 ++ 𝑓)) ∈ (ℤ‘((#‘𝐴) + 𝑐)))
134 lencl 13263 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Word (𝐼 × 2𝑜) → (#‘𝐵) ∈ ℕ0)
13588, 134syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘𝐵) ∈ ℕ0)
136 uzaddcl 11688 . . . . . . . . . . . . . . . . . 18 (((#‘(𝐴 ++ 𝑓)) ∈ (ℤ‘((#‘𝐴) + 𝑐)) ∧ (#‘𝐵) ∈ ℕ0) → ((#‘(𝐴 ++ 𝑓)) + (#‘𝐵)) ∈ (ℤ‘((#‘𝐴) + 𝑐)))
137133, 135, 136syl2anc 692 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((#‘(𝐴 ++ 𝑓)) + (#‘𝐵)) ∈ (ℤ‘((#‘𝐴) + 𝑐)))
138116, 137eqeltrd 2698 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈ (ℤ‘((#‘𝐴) + 𝑐)))
139 elfzuzb 12278 . . . . . . . . . . . . . . . 16 (((#‘𝐴) + 𝑐) ∈ (0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) ↔ (((#‘𝐴) + 𝑐) ∈ (ℤ‘0) ∧ (#‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈ (ℤ‘((#‘𝐴) + 𝑐))))
140113, 138, 139sylanbrc 697 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((#‘𝐴) + 𝑐) ∈ (0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))))
1411, 2, 3, 4efgtval 18057 . . . . . . . . . . . . . . 15 ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((#‘𝐴) + 𝑐) ∈ (0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2𝑜)) → (((#‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((#‘𝐴) + 𝑐), ((#‘𝐴) + 𝑐), ⟨“𝑢(𝑀𝑢)”⟩⟩))
14272, 140, 70, 141syl3anc 1323 . . . . . . . . . . . . . 14 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (((#‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((#‘𝐴) + 𝑐), ((#‘𝐴) + 𝑐), ⟨“𝑢(𝑀𝑢)”⟩⟩))
143 wrd0 13269 . . . . . . . . . . . . . . . 16 ∅ ∈ Word (𝐼 × 2𝑜)
144143a1i 11 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ∅ ∈ Word (𝐼 × 2𝑜))
145 ccatcl 13298 . . . . . . . . . . . . . . . 16 (((𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝐵 ∈ Word (𝐼 × 2𝑜)) → ((𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ++ 𝐵) ∈ Word (𝐼 × 2𝑜))
14687, 88, 145syl2anc 692 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ++ 𝐵) ∈ Word (𝐼 × 2𝑜))
147 ccatrid 13309 . . . . . . . . . . . . . . . . . 18 ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ∈ Word (𝐼 × 2𝑜) → ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ∅) = (𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)))
14879, 147syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ∅) = (𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)))
149148oveq1d 6619 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ∅) ++ ((𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ++ 𝐵)) = ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ((𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ++ 𝐵)))
150 ccatass 13310 . . . . . . . . . . . . . . . . 17 (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝐵 ∈ Word (𝐼 × 2𝑜)) → (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ((𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ++ 𝐵)))
15179, 87, 88, 150syl3anc 1323 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ((𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ++ 𝐵)))
152 ccatass 13310 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr ⟨0, 𝑐⟩) ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ∈ Word (𝐼 × 2𝑜)) → ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) = (𝐴 ++ ((𝑓 substr ⟨0, 𝑐⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩))))
15374, 77, 87, 152syl3anc 1323 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) = (𝐴 ++ ((𝑓 substr ⟨0, 𝑐⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩))))
154111, 108syl6eleq 2708 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 𝑐 ∈ (ℤ‘0))
155 eluzfz1 12290 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ (ℤ‘0) → 0 ∈ (0...𝑐))
156154, 155syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 0 ∈ (0...𝑐))
157125, 108syl6eleq 2708 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘𝑓) ∈ (ℤ‘0))
158 eluzfz2 12291 . . . . . . . . . . . . . . . . . . . . . 22 ((#‘𝑓) ∈ (ℤ‘0) → (#‘𝑓) ∈ (0...(#‘𝑓)))
159157, 158syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘𝑓) ∈ (0...(#‘𝑓)))
160 ccatswrd 13394 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑐) ∧ 𝑐 ∈ (0...(#‘𝑓)) ∧ (#‘𝑓) ∈ (0...(#‘𝑓)))) → ((𝑓 substr ⟨0, 𝑐⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) = (𝑓 substr ⟨0, (#‘𝑓)⟩))
16175, 156, 69, 159, 160syl13anc 1325 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝑓 substr ⟨0, 𝑐⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) = (𝑓 substr ⟨0, (#‘𝑓)⟩))
162 swrdid 13366 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ Word (𝐼 × 2𝑜) → (𝑓 substr ⟨0, (#‘𝑓)⟩) = 𝑓)
16375, 162syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝑓 substr ⟨0, (#‘𝑓)⟩) = 𝑓)
164161, 163eqtrd 2655 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝑓 substr ⟨0, 𝑐⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) = 𝑓)
165164oveq2d 6620 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝐴 ++ ((𝑓 substr ⟨0, 𝑐⟩) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩))) = (𝐴 ++ 𝑓))
166153, 165eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) = (𝐴 ++ 𝑓))
167166oveq1d 6619 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ (𝑓 substr ⟨𝑐, (#‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ 𝑓) ++ 𝐵))
168149, 151, 1673eqtr2rd 2662 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝐴 ++ 𝑓) ++ 𝐵) = (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ∅) ++ ((𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ++ 𝐵)))
169 ccatlen 13299 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr ⟨0, 𝑐⟩) ∈ Word (𝐼 × 2𝑜)) → (#‘(𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩))) = ((#‘𝐴) + (#‘(𝑓 substr ⟨0, 𝑐⟩))))
17074, 77, 169syl2anc 692 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘(𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩))) = ((#‘𝐴) + (#‘(𝑓 substr ⟨0, 𝑐⟩))))
171 swrd0len 13360 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ Word (𝐼 × 2𝑜) ∧ 𝑐 ∈ (0...(#‘𝑓))) → (#‘(𝑓 substr ⟨0, 𝑐⟩)) = 𝑐)
17275, 69, 171syl2anc 692 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (#‘(𝑓 substr ⟨0, 𝑐⟩)) = 𝑐)
173172oveq2d 6620 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((#‘𝐴) + (#‘(𝑓 substr ⟨0, 𝑐⟩))) = ((#‘𝐴) + 𝑐))
174170, 173eqtr2d 2656 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((#‘𝐴) + 𝑐) = (#‘(𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩))))
175 hash0 13098 . . . . . . . . . . . . . . . . 17 (#‘∅) = 0
176175oveq2i 6615 . . . . . . . . . . . . . . . 16 (((#‘𝐴) + 𝑐) + (#‘∅)) = (((#‘𝐴) + 𝑐) + 0)
177107, 111nn0addcld 11299 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((#‘𝐴) + 𝑐) ∈ ℕ0)
178177nn0cnd 11297 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((#‘𝐴) + 𝑐) ∈ ℂ)
179178addid1d 10180 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (((#‘𝐴) + 𝑐) + 0) = ((#‘𝐴) + 𝑐))
180176, 179syl5req 2668 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((#‘𝐴) + 𝑐) = (((#‘𝐴) + 𝑐) + (#‘∅)))
18179, 144, 146, 83, 168, 174, 180splval2 13445 . . . . . . . . . . . . . 14 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((#‘𝐴) + 𝑐), ((#‘𝐴) + 𝑐), ⟨“𝑢(𝑀𝑢)”⟩⟩) = (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ++ 𝐵)))
182142, 181eqtrd 2655 . . . . . . . . . . . . 13 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (((#‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ (𝑓 substr ⟨0, 𝑐⟩)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (#‘𝑓)⟩) ++ 𝐵)))
18390, 105, 1823eqtr4d 2665 . . . . . . . . . . . 12 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵) = (((#‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢))
1841, 2, 3, 4efgtf 18056 . . . . . . . . . . . . . . 15 (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) = (𝑎 ∈ (0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))), 𝑏 ∈ (𝐼 × 2𝑜) ↦ (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀𝑏)”⟩⟩)) ∧ (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2𝑜))⟶𝑊))
185184simprd 479 . . . . . . . . . . . . . 14 (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2𝑜))⟶𝑊)
186 ffn 6002 . . . . . . . . . . . . . 14 ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2𝑜))⟶𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2𝑜)))
18772, 185, 1863syl 18 . . . . . . . . . . . . 13 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2𝑜)))
188 fnovrn 6762 . . . . . . . . . . . . 13 (((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2𝑜)) ∧ ((#‘𝐴) + 𝑐) ∈ (0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2𝑜)) → (((#‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
189187, 140, 70, 188syl3anc 1323 . . . . . . . . . . . 12 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (((#‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
190183, 189eqeltrd 2698 . . . . . . . . . . 11 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
1911, 2, 3, 4efgi2 18059 . . . . . . . . . . 11 ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵))
19272, 190, 191syl2anc 692 . . . . . . . . . 10 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵))
1931, 2, 3, 4, 9, 10, 6efgcpbllema 18088 . . . . . . . . . 10 (𝑓𝐿(𝑐(𝑇𝑓)𝑢) ↔ (𝑓𝑊 ∧ (𝑐(𝑇𝑓)𝑢) ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵)))
19467, 71, 192, 193syl3anbrc 1244 . . . . . . . . 9 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 𝑓𝐿(𝑐(𝑇𝑓)𝑢))
195 vex 3189 . . . . . . . . . . 11 𝑎 ∈ V
196 vex 3189 . . . . . . . . . . 11 𝑓 ∈ V
197195, 196elec 7731 . . . . . . . . . 10 (𝑎 ∈ [𝑓]𝐿𝑓𝐿𝑎)
198 breq2 4617 . . . . . . . . . 10 (𝑎 = (𝑐(𝑇𝑓)𝑢) → (𝑓𝐿𝑎𝑓𝐿(𝑐(𝑇𝑓)𝑢)))
199197, 198syl5bb 272 . . . . . . . . 9 (𝑎 = (𝑐(𝑇𝑓)𝑢) → (𝑎 ∈ [𝑓]𝐿𝑓𝐿(𝑐(𝑇𝑓)𝑢)))
200194, 199syl5ibrcom 237 . . . . . . . 8 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → (𝑎 = (𝑐(𝑇𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿))
201200rexlimdvva 3031 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → (∃𝑐 ∈ (0...(#‘𝑓))∃𝑢 ∈ (𝐼 × 2𝑜)𝑎 = (𝑐(𝑇𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿))
20266, 201sylbid 230 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → (𝑎 ∈ ran (𝑇𝑓) → 𝑎 ∈ [𝑓]𝐿))
203202ssrdv 3589 . . . . 5 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → ran (𝑇𝑓) ⊆ [𝑓]𝐿)
204203ralrimiva 2960 . . . 4 ((𝐴𝑊𝐵𝑊) → ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝐿)
205 fvex 6158 . . . . . . 7 ( I ‘Word (𝐼 × 2𝑜)) ∈ V
2061, 205eqeltri 2694 . . . . . 6 𝑊 ∈ V
207 erex 7711 . . . . . 6 (𝐿 Er 𝑊 → (𝑊 ∈ V → 𝐿 ∈ V))
20860, 206, 207mpisyl 21 . . . . 5 ((𝐴𝑊𝐵𝑊) → 𝐿 ∈ V)
209 ereq1 7694 . . . . . . 7 (𝑟 = 𝐿 → (𝑟 Er 𝑊𝐿 Er 𝑊))
210 eceq2 7729 . . . . . . . . 9 (𝑟 = 𝐿 → [𝑓]𝑟 = [𝑓]𝐿)
211210sseq2d 3612 . . . . . . . 8 (𝑟 = 𝐿 → (ran (𝑇𝑓) ⊆ [𝑓]𝑟 ↔ ran (𝑇𝑓) ⊆ [𝑓]𝐿))
212211ralbidv 2980 . . . . . . 7 (𝑟 = 𝐿 → (∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟 ↔ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝐿))
213209, 212anbi12d 746 . . . . . 6 (𝑟 = 𝐿 → ((𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟) ↔ (𝐿 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝐿)))
214213elabg 3334 . . . . 5 (𝐿 ∈ V → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝐿)))
215208, 214syl 17 . . . 4 ((𝐴𝑊𝐵𝑊) → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝐿)))
21660, 204, 215mpbir2and 956 . . 3 ((𝐴𝑊𝐵𝑊) → 𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)})
217 intss1 4457 . . 3 (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)} → {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿)
218216, 217syl 17 . 2 ((𝐴𝑊𝐵𝑊) → {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿)
2195, 218syl5eqss 3628 1 ((𝐴𝑊𝐵𝑊) → 𝐿)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  {cab 2607  wral 2907  wrex 2908  {crab 2911  Vcvv 3186  cdif 3552  wss 3555  c0 3891  {csn 4148  {cpr 4150  cop 4154  cotp 4156   cint 4440   ciun 4485   class class class wbr 4613  {copab 4672  cmpt 4673   I cid 4984   × cxp 5072  ran crn 5075  Rel wrel 5079   Fn wfn 5842  wf 5843  cfv 5847  (class class class)co 6604  cmpt2 6606  1𝑜c1o 7498  2𝑜c2o 7499   Er wer 7684  [cec 7685  0cc0 9880  1c1 9881   + caddc 9883  cmin 10210  0cn0 11236  cz 11321  cuz 11631  ...cfz 12268  ..^cfzo 12406  #chash 13057  Word cword 13230   ++ cconcat 13232   substr csubstr 13234   splice csplice 13235  ⟨“cs2 13523   ~FG cefg 18040
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 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
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 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-ot 4157  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-ec 7689  df-map 7804  df-pm 7805  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-card 8709  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-n0 11237  df-z 11322  df-uz 11632  df-fz 12269  df-fzo 12407  df-hash 13058  df-word 13238  df-concat 13240  df-s1 13241  df-substr 13242  df-splice 13243  df-s2 13530  df-efg 18043
This theorem is referenced by:  efgcpbl  18090
  Copyright terms: Public domain W3C validator