Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  1arithidomlem2 Structured version   Visualization version   GIF version

Theorem 1arithidomlem2 33543
Description: Lemma for 1arithidom 33544: induction step. (Contributed by Thierry Arnoux, 27-May-2025.)
Hypotheses
Ref Expression
1arithidom.u 𝑈 = (Unit‘𝑅)
1arithidom.i 𝑃 = (RPrime‘𝑅)
1arithidom.m 𝑀 = (mulGrp‘𝑅)
1arithidom.t · = (.r𝑅)
1arithidom.j 𝐽 = (0..^(♯‘𝐹))
1arithidom.r (𝜑𝑅 ∈ IDomn)
1arithidom.f (𝜑𝐹 ∈ Word 𝑃)
1arithidom.g (𝜑𝐺 ∈ Word 𝑃)
1arithidom.1 (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg 𝐺))
1arithidomlem.1 (𝜑𝑄𝑃)
1arithidomlem.2 (𝜑 → ∀𝑔 ∈ Word 𝑃(∃𝑘𝑈 (𝑀 Σg 𝐹) = (𝑘 · (𝑀 Σg 𝑔)) → ∃𝑤𝑢 ∈ (𝑈m (0..^(♯‘𝐹)))(𝑤:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) ∧ 𝑔 = (𝑢f · (𝐹𝑤)))))
1arithidomlem.3 (𝜑𝐻 ∈ Word 𝑃)
1arithidomlem.4 (𝜑 → ∃𝑘𝑈 (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑘 · (𝑀 Σg 𝐻)))
1arithidomlem.5 (𝜑𝐾 ∈ (0..^(♯‘𝐻)))
1arithidomlem.6 (𝜑𝑄(∥r𝑅)(𝐻𝐾))
1arithidomlem.7 (𝜑𝑇𝑈)
1arithidomlem.8 (𝜑 → (𝑇 · 𝑄) = (𝐻𝐾))
1arithidomlem.9 (𝜑𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)))
1arithidomlem.10 (𝜑 → (𝐻𝑆) = (((𝐻𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻𝐾)”⟩))
1arithidomlem.11 (𝜑𝑁𝑈)
1arithidomlem.12 (𝜑 → (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑁 · (𝑀 Σg 𝐻)))
1arithidomlem.13 (𝜑𝐷 ∈ (𝑈m (0..^(♯‘𝐹))))
1arithidomlem.14 (𝜑𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)))
1arithidomlem.15 (𝜑 → ((𝐻𝑆) prefix ((♯‘𝐻) − 1)) = (𝐷f · (𝐹𝐶)))
Assertion
Ref Expression
1arithidomlem2 (𝜑 → (((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆):(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩)))–1-1-onto→(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))) ∧ 𝐻 = (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆)))))
Distinct variable groups:   · ,𝑔,𝑘,𝑢,𝑤   𝑢,𝐶   𝑔,𝐹,𝑘,𝑢,𝑤   𝑔,𝐻,𝑢,𝑤,𝑘   𝑘,𝐾,𝑢,𝑤   𝑔,𝑀,𝑢,𝑘   𝑢,𝑁,𝑤   𝑃,𝑔,𝑢,𝑘   𝑅,𝑔,𝑢,𝑘   𝑆,𝑔,𝑢,𝑤,𝑘   𝑢,𝑇,𝑤   𝑈,𝑔,𝑢,𝑤,𝑘   𝑄,𝑔,𝑢,𝑤,𝑘
Allowed substitution hints:   𝜑(𝑤,𝑢,𝑔,𝑘)   𝐶(𝑤,𝑔,𝑘)   𝐷(𝑤,𝑢,𝑔,𝑘)   𝑃(𝑤)   𝑅(𝑤)   𝑇(𝑔,𝑘)   𝐺(𝑤,𝑢,𝑔,𝑘)   𝐽(𝑤,𝑢,𝑔,𝑘)   𝐾(𝑔)   𝑀(𝑤)   𝑁(𝑔,𝑘)

Proof of Theorem 1arithidomlem2
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1arithidom.f . . . . . 6 (𝜑𝐹 ∈ Word 𝑃)
2 ccatws1len 14654 . . . . . 6 (𝐹 ∈ Word 𝑃 → (♯‘(𝐹 ++ ⟨“𝑄”⟩)) = ((♯‘𝐹) + 1))
31, 2syl 17 . . . . 5 (𝜑 → (♯‘(𝐹 ++ ⟨“𝑄”⟩)) = ((♯‘𝐹) + 1))
4 1arithidomlem.15 . . . . . . . . . 10 (𝜑 → ((𝐻𝑆) prefix ((♯‘𝐻) − 1)) = (𝐷f · (𝐹𝐶)))
54dmeqd 5918 . . . . . . . . 9 (𝜑 → dom ((𝐻𝑆) prefix ((♯‘𝐻) − 1)) = dom (𝐷f · (𝐹𝐶)))
6 1arithidomlem.9 . . . . . . . . . . . . 13 (𝜑𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)))
7 f1of 6848 . . . . . . . . . . . . 13 (𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)) → 𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)))
8 iswrdi 14552 . . . . . . . . . . . . 13 (𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)) → 𝑆 ∈ Word (0..^(♯‘𝐻)))
96, 7, 83syl 18 . . . . . . . . . . . 12 (𝜑𝑆 ∈ Word (0..^(♯‘𝐻)))
10 eqidd 2735 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐻) = (♯‘𝐻))
11 1arithidomlem.3 . . . . . . . . . . . . 13 (𝜑𝐻 ∈ Word 𝑃)
1210, 11wrdfd 32902 . . . . . . . . . . . 12 (𝜑𝐻:(0..^(♯‘𝐻))⟶𝑃)
13 wrdco 14866 . . . . . . . . . . . 12 ((𝑆 ∈ Word (0..^(♯‘𝐻)) ∧ 𝐻:(0..^(♯‘𝐻))⟶𝑃) → (𝐻𝑆) ∈ Word 𝑃)
149, 12, 13syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝐻𝑆) ∈ Word 𝑃)
15 1arithidomlem.5 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ (0..^(♯‘𝐻)))
16 elfzo0 13736 . . . . . . . . . . . . . 14 (𝐾 ∈ (0..^(♯‘𝐻)) ↔ (𝐾 ∈ ℕ0 ∧ (♯‘𝐻) ∈ ℕ ∧ 𝐾 < (♯‘𝐻)))
1716simp2bi 1145 . . . . . . . . . . . . 13 (𝐾 ∈ (0..^(♯‘𝐻)) → (♯‘𝐻) ∈ ℕ)
18 nnm1nn0 12564 . . . . . . . . . . . . 13 ((♯‘𝐻) ∈ ℕ → ((♯‘𝐻) − 1) ∈ ℕ0)
1915, 17, 183syl 18 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ0)
20 lenco 14867 . . . . . . . . . . . . . 14 ((𝑆 ∈ Word (0..^(♯‘𝐻)) ∧ 𝐻:(0..^(♯‘𝐻))⟶𝑃) → (♯‘(𝐻𝑆)) = (♯‘𝑆))
219, 12, 20syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐻𝑆)) = (♯‘𝑆))
22 lencl 14567 . . . . . . . . . . . . . 14 (𝑆 ∈ Word (0..^(♯‘𝐻)) → (♯‘𝑆) ∈ ℕ0)
239, 22syl 17 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝑆) ∈ ℕ0)
2421, 23eqeltrd 2838 . . . . . . . . . . . 12 (𝜑 → (♯‘(𝐻𝑆)) ∈ ℕ0)
25 lencl 14567 . . . . . . . . . . . . . . . 16 (𝐻 ∈ Word 𝑃 → (♯‘𝐻) ∈ ℕ0)
2611, 25syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘𝐻) ∈ ℕ0)
2726nn0red 12585 . . . . . . . . . . . . . 14 (𝜑 → (♯‘𝐻) ∈ ℝ)
2827lem1d 12198 . . . . . . . . . . . . 13 (𝜑 → ((♯‘𝐻) − 1) ≤ (♯‘𝐻))
296, 7syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)))
30 ffn 6736 . . . . . . . . . . . . . . 15 (𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)) → 𝑆 Fn (0..^(♯‘𝐻)))
31 hashfn 14410 . . . . . . . . . . . . . . 15 (𝑆 Fn (0..^(♯‘𝐻)) → (♯‘𝑆) = (♯‘(0..^(♯‘𝐻))))
3229, 30, 313syl 18 . . . . . . . . . . . . . 14 (𝜑 → (♯‘𝑆) = (♯‘(0..^(♯‘𝐻))))
33 hashfzo0 14465 . . . . . . . . . . . . . . 15 ((♯‘𝐻) ∈ ℕ0 → (♯‘(0..^(♯‘𝐻))) = (♯‘𝐻))
3411, 25, 333syl 18 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(0..^(♯‘𝐻))) = (♯‘𝐻))
3521, 32, 343eqtrrd 2779 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐻) = (♯‘(𝐻𝑆)))
3628, 35breqtrd 5173 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝐻) − 1) ≤ (♯‘(𝐻𝑆)))
37 elfz2nn0 13654 . . . . . . . . . . . 12 (((♯‘𝐻) − 1) ∈ (0...(♯‘(𝐻𝑆))) ↔ (((♯‘𝐻) − 1) ∈ ℕ0 ∧ (♯‘(𝐻𝑆)) ∈ ℕ0 ∧ ((♯‘𝐻) − 1) ≤ (♯‘(𝐻𝑆))))
3819, 24, 36, 37syl3anbrc 1342 . . . . . . . . . . 11 (𝜑 → ((♯‘𝐻) − 1) ∈ (0...(♯‘(𝐻𝑆))))
39 pfxfn 14715 . . . . . . . . . . 11 (((𝐻𝑆) ∈ Word 𝑃 ∧ ((♯‘𝐻) − 1) ∈ (0...(♯‘(𝐻𝑆)))) → ((𝐻𝑆) prefix ((♯‘𝐻) − 1)) Fn (0..^((♯‘𝐻) − 1)))
4014, 38, 39syl2anc 584 . . . . . . . . . 10 (𝜑 → ((𝐻𝑆) prefix ((♯‘𝐻) − 1)) Fn (0..^((♯‘𝐻) − 1)))
4140fndmd 6673 . . . . . . . . 9 (𝜑 → dom ((𝐻𝑆) prefix ((♯‘𝐻) − 1)) = (0..^((♯‘𝐻) − 1)))
42 eqid 2734 . . . . . . . . . . . 12 (Base‘𝑅) = (Base‘𝑅)
43 1arithidom.t . . . . . . . . . . . 12 · = (.r𝑅)
44 1arithidom.r . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ IDomn)
4544idomringd 20744 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ Ring)
4645adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑈𝑦𝑃)) → 𝑅 ∈ Ring)
47 1arithidom.u . . . . . . . . . . . . . 14 𝑈 = (Unit‘𝑅)
4842, 47unitcl 20391 . . . . . . . . . . . . 13 (𝑥𝑈𝑥 ∈ (Base‘𝑅))
4948ad2antrl 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑈𝑦𝑃)) → 𝑥 ∈ (Base‘𝑅))
50 1arithidom.i . . . . . . . . . . . . 13 𝑃 = (RPrime‘𝑅)
5144adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑈𝑦𝑃)) → 𝑅 ∈ IDomn)
52 simprr 773 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑈𝑦𝑃)) → 𝑦𝑃)
5342, 50, 51, 52rprmcl 33525 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑈𝑦𝑃)) → 𝑦 ∈ (Base‘𝑅))
5442, 43, 46, 49, 53ringcld 20276 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑈𝑦𝑃)) → (𝑥 · 𝑦) ∈ (Base‘𝑅))
55 1arithidomlem.13 . . . . . . . . . . . 12 (𝜑𝐷 ∈ (𝑈m (0..^(♯‘𝐹))))
56 elmapi 8887 . . . . . . . . . . . 12 (𝐷 ∈ (𝑈m (0..^(♯‘𝐹))) → 𝐷:(0..^(♯‘𝐹))⟶𝑈)
5755, 56syl 17 . . . . . . . . . . 11 (𝜑𝐷:(0..^(♯‘𝐹))⟶𝑈)
58 eqidd 2735 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐹) = (♯‘𝐹))
5958, 1wrdfd 32902 . . . . . . . . . . . 12 (𝜑𝐹:(0..^(♯‘𝐹))⟶𝑃)
60 1arithidomlem.14 . . . . . . . . . . . . 13 (𝜑𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)))
61 f1of 6848 . . . . . . . . . . . . 13 (𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) → 𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐹)))
6260, 61syl 17 . . . . . . . . . . . 12 (𝜑𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐹)))
6359, 62fcod 6761 . . . . . . . . . . 11 (𝜑 → (𝐹𝐶):(0..^(♯‘𝐹))⟶𝑃)
64 ovexd 7465 . . . . . . . . . . 11 (𝜑 → (0..^(♯‘𝐹)) ∈ V)
65 inidm 4234 . . . . . . . . . . 11 ((0..^(♯‘𝐹)) ∩ (0..^(♯‘𝐹))) = (0..^(♯‘𝐹))
6654, 57, 63, 64, 64, 65off 7714 . . . . . . . . . 10 (𝜑 → (𝐷f · (𝐹𝐶)):(0..^(♯‘𝐹))⟶(Base‘𝑅))
6766fdmd 6746 . . . . . . . . 9 (𝜑 → dom (𝐷f · (𝐹𝐶)) = (0..^(♯‘𝐹)))
685, 41, 673eqtr3d 2782 . . . . . . . 8 (𝜑 → (0..^((♯‘𝐻) − 1)) = (0..^(♯‘𝐹)))
69 lencl 14567 . . . . . . . . . 10 (𝐹 ∈ Word 𝑃 → (♯‘𝐹) ∈ ℕ0)
701, 69syl 17 . . . . . . . . 9 (𝜑 → (♯‘𝐹) ∈ ℕ0)
7119, 70fzo0opth 32812 . . . . . . . 8 (𝜑 → ((0..^((♯‘𝐻) − 1)) = (0..^(♯‘𝐹)) ↔ ((♯‘𝐻) − 1) = (♯‘𝐹)))
7268, 71mpbid 232 . . . . . . 7 (𝜑 → ((♯‘𝐻) − 1) = (♯‘𝐹))
7372oveq1d 7445 . . . . . 6 (𝜑 → (((♯‘𝐻) − 1) + 1) = ((♯‘𝐹) + 1))
7415, 17syl 17 . . . . . . . 8 (𝜑 → (♯‘𝐻) ∈ ℕ)
7574nncnd 12279 . . . . . . 7 (𝜑 → (♯‘𝐻) ∈ ℂ)
76 npcan1 11685 . . . . . . 7 ((♯‘𝐻) ∈ ℂ → (((♯‘𝐻) − 1) + 1) = (♯‘𝐻))
7775, 76syl 17 . . . . . 6 (𝜑 → (((♯‘𝐻) − 1) + 1) = (♯‘𝐻))
7873, 77eqtr3d 2776 . . . . 5 (𝜑 → ((♯‘𝐹) + 1) = (♯‘𝐻))
793, 78eqtrd 2774 . . . 4 (𝜑 → (♯‘(𝐹 ++ ⟨“𝑄”⟩)) = (♯‘𝐻))
8079oveq2d 7446 . . 3 (𝜑 → (0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))) = (0..^(♯‘𝐻)))
81 eqid 2734 . . . . . 6 (♯‘𝐶) = (♯‘𝐶)
82 eqid 2734 . . . . . 6 (0..^((♯‘𝐶) + 1)) = (0..^((♯‘𝐶) + 1))
83 f1ofn 6849 . . . . . . . . . 10 (𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) → 𝐶 Fn (0..^(♯‘𝐹)))
84 hashfn 14410 . . . . . . . . . 10 (𝐶 Fn (0..^(♯‘𝐹)) → (♯‘𝐶) = (♯‘(0..^(♯‘𝐹))))
8560, 83, 843syl 18 . . . . . . . . 9 (𝜑 → (♯‘𝐶) = (♯‘(0..^(♯‘𝐹))))
86 hashfzo0 14465 . . . . . . . . . 10 ((♯‘𝐹) ∈ ℕ0 → (♯‘(0..^(♯‘𝐹))) = (♯‘𝐹))
8770, 86syl 17 . . . . . . . . 9 (𝜑 → (♯‘(0..^(♯‘𝐹))) = (♯‘𝐹))
8885, 87eqtrd 2774 . . . . . . . 8 (𝜑 → (♯‘𝐶) = (♯‘𝐹))
8988oveq2d 7446 . . . . . . 7 (𝜑 → (0..^(♯‘𝐶)) = (0..^(♯‘𝐹)))
90 f1oeq23 6839 . . . . . . . 8 (((0..^(♯‘𝐶)) = (0..^(♯‘𝐹)) ∧ (0..^(♯‘𝐶)) = (0..^(♯‘𝐹))) → (𝐶:(0..^(♯‘𝐶))–1-1-onto→(0..^(♯‘𝐶)) ↔ 𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹))))
9190biimpar 477 . . . . . . 7 ((((0..^(♯‘𝐶)) = (0..^(♯‘𝐹)) ∧ (0..^(♯‘𝐶)) = (0..^(♯‘𝐹))) ∧ 𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹))) → 𝐶:(0..^(♯‘𝐶))–1-1-onto→(0..^(♯‘𝐶)))
9289, 89, 60, 91syl21anc 838 . . . . . 6 (𝜑𝐶:(0..^(♯‘𝐶))–1-1-onto→(0..^(♯‘𝐶)))
9381, 82, 92ccatws1f1o 32920 . . . . 5 (𝜑 → (𝐶 ++ ⟨“(♯‘𝐶)”⟩):(0..^((♯‘𝐶) + 1))–1-1-onto→(0..^((♯‘𝐶) + 1)))
9488s1eqd 14635 . . . . . . 7 (𝜑 → ⟨“(♯‘𝐶)”⟩ = ⟨“(♯‘𝐹)”⟩)
9594oveq2d 7446 . . . . . 6 (𝜑 → (𝐶 ++ ⟨“(♯‘𝐶)”⟩) = (𝐶 ++ ⟨“(♯‘𝐹)”⟩))
9688oveq1d 7445 . . . . . . . 8 (𝜑 → ((♯‘𝐶) + 1) = ((♯‘𝐹) + 1))
9796, 78eqtrd 2774 . . . . . . 7 (𝜑 → ((♯‘𝐶) + 1) = (♯‘𝐻))
9897oveq2d 7446 . . . . . 6 (𝜑 → (0..^((♯‘𝐶) + 1)) = (0..^(♯‘𝐻)))
9995, 98, 98f1oeq123d 6842 . . . . 5 (𝜑 → ((𝐶 ++ ⟨“(♯‘𝐶)”⟩):(0..^((♯‘𝐶) + 1))–1-1-onto→(0..^((♯‘𝐶) + 1)) ↔ (𝐶 ++ ⟨“(♯‘𝐹)”⟩):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))))
10093, 99mpbid 232 . . . 4 (𝜑 → (𝐶 ++ ⟨“(♯‘𝐹)”⟩):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)))
101 f1ocnv 6860 . . . . 5 (𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)) → 𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)))
1026, 101syl 17 . . . 4 (𝜑𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)))
103 f1oco 6871 . . . 4 (((𝐶 ++ ⟨“(♯‘𝐹)”⟩):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)) ∧ 𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) → ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)))
104100, 102, 103syl2anc 584 . . 3 (𝜑 → ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)))
105 f1oeq23 6839 . . . 4 (((0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))) = (0..^(♯‘𝐻)) ∧ (0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))) = (0..^(♯‘𝐻))) → (((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆):(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩)))–1-1-onto→(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))) ↔ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))))
106105biimpar 477 . . 3 ((((0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))) = (0..^(♯‘𝐻)) ∧ (0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))) = (0..^(♯‘𝐻))) ∧ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) → ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆):(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩)))–1-1-onto→(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))))
10780, 80, 104, 106syl21anc 838 . 2 (𝜑 → ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆):(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩)))–1-1-onto→(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))))
108 f1ofo 6855 . . . 4 (𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)) → 𝑆:(0..^(♯‘𝐻))–onto→(0..^(♯‘𝐻)))
1096, 108syl 17 . . 3 (𝜑𝑆:(0..^(♯‘𝐻))–onto→(0..^(♯‘𝐻)))
11012ffnd 6737 . . 3 (𝜑𝐻 Fn (0..^(♯‘𝐻)))
111 iswrdi 14552 . . . . . . . . . . 11 (𝐷:(0..^(♯‘𝐹))⟶𝑈𝐷 ∈ Word 𝑈)
11257, 111syl 17 . . . . . . . . . 10 (𝜑𝐷 ∈ Word 𝑈)
113 ccatws1len 14654 . . . . . . . . . 10 (𝐷 ∈ Word 𝑈 → (♯‘(𝐷 ++ ⟨“𝑇”⟩)) = ((♯‘𝐷) + 1))
114112, 113syl 17 . . . . . . . . 9 (𝜑 → (♯‘(𝐷 ++ ⟨“𝑇”⟩)) = ((♯‘𝐷) + 1))
115 elmapfn 8903 . . . . . . . . . . . 12 (𝐷 ∈ (𝑈m (0..^(♯‘𝐹))) → 𝐷 Fn (0..^(♯‘𝐹)))
116 hashfn 14410 . . . . . . . . . . . 12 (𝐷 Fn (0..^(♯‘𝐹)) → (♯‘𝐷) = (♯‘(0..^(♯‘𝐹))))
11755, 115, 1163syl 18 . . . . . . . . . . 11 (𝜑 → (♯‘𝐷) = (♯‘(0..^(♯‘𝐹))))
118117, 87eqtrd 2774 . . . . . . . . . 10 (𝜑 → (♯‘𝐷) = (♯‘𝐹))
119118oveq1d 7445 . . . . . . . . 9 (𝜑 → ((♯‘𝐷) + 1) = ((♯‘𝐹) + 1))
120114, 119, 783eqtrd 2778 . . . . . . . 8 (𝜑 → (♯‘(𝐷 ++ ⟨“𝑇”⟩)) = (♯‘𝐻))
121120oveq2d 7446 . . . . . . 7 (𝜑 → (0..^(♯‘(𝐷 ++ ⟨“𝑇”⟩))) = (0..^(♯‘𝐻)))
122 eqidd 2735 . . . . . . . 8 (𝜑 → (♯‘(𝐷 ++ ⟨“𝑇”⟩)) = (♯‘(𝐷 ++ ⟨“𝑇”⟩)))
123 1arithidomlem.7 . . . . . . . . 9 (𝜑𝑇𝑈)
124 ccatws1cl 14650 . . . . . . . . 9 ((𝐷 ∈ Word 𝑈𝑇𝑈) → (𝐷 ++ ⟨“𝑇”⟩) ∈ Word 𝑈)
125112, 123, 124syl2anc 584 . . . . . . . 8 (𝜑 → (𝐷 ++ ⟨“𝑇”⟩) ∈ Word 𝑈)
126122, 125wrdfd 32902 . . . . . . 7 (𝜑 → (𝐷 ++ ⟨“𝑇”⟩):(0..^(♯‘(𝐷 ++ ⟨“𝑇”⟩)))⟶𝑈)
127121, 126feq2dd 32639 . . . . . 6 (𝜑 → (𝐷 ++ ⟨“𝑇”⟩):(0..^(♯‘𝐻))⟶𝑈)
128127ffnd 6737 . . . . 5 (𝜑 → (𝐷 ++ ⟨“𝑇”⟩) Fn (0..^(♯‘𝐻)))
129 f1of 6848 . . . . . 6 (𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)) → 𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)))
1306, 101, 1293syl 18 . . . . 5 (𝜑𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)))
131 fnfco 6773 . . . . 5 (((𝐷 ++ ⟨“𝑇”⟩) Fn (0..^(♯‘𝐻)) ∧ 𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻))) → ((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) Fn (0..^(♯‘𝐻)))
132128, 130, 131syl2anc 584 . . . 4 (𝜑 → ((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) Fn (0..^(♯‘𝐻)))
13378oveq2d 7446 . . . . . . 7 (𝜑 → (0..^((♯‘𝐹) + 1)) = (0..^(♯‘𝐻)))
1343eqcomd 2740 . . . . . . . 8 (𝜑 → ((♯‘𝐹) + 1) = (♯‘(𝐹 ++ ⟨“𝑄”⟩)))
135 1arithidomlem.1 . . . . . . . . 9 (𝜑𝑄𝑃)
136 ccatws1cl 14650 . . . . . . . . 9 ((𝐹 ∈ Word 𝑃𝑄𝑃) → (𝐹 ++ ⟨“𝑄”⟩) ∈ Word 𝑃)
1371, 135, 136syl2anc 584 . . . . . . . 8 (𝜑 → (𝐹 ++ ⟨“𝑄”⟩) ∈ Word 𝑃)
138134, 137wrdfd 32902 . . . . . . 7 (𝜑 → (𝐹 ++ ⟨“𝑄”⟩):(0..^((♯‘𝐹) + 1))⟶𝑃)
139133, 138feq2dd 32639 . . . . . 6 (𝜑 → (𝐹 ++ ⟨“𝑄”⟩):(0..^(♯‘𝐻))⟶𝑃)
140139ffnd 6737 . . . . 5 (𝜑 → (𝐹 ++ ⟨“𝑄”⟩) Fn (0..^(♯‘𝐻)))
141 fzossfzop1 13778 . . . . . . . . . . . 12 ((♯‘𝐹) ∈ ℕ0 → (0..^(♯‘𝐹)) ⊆ (0..^((♯‘𝐹) + 1)))
14270, 141syl 17 . . . . . . . . . . 11 (𝜑 → (0..^(♯‘𝐹)) ⊆ (0..^((♯‘𝐹) + 1)))
143 sswrd 14556 . . . . . . . . . . 11 ((0..^(♯‘𝐹)) ⊆ (0..^((♯‘𝐹) + 1)) → Word (0..^(♯‘𝐹)) ⊆ Word (0..^((♯‘𝐹) + 1)))
144142, 143syl 17 . . . . . . . . . 10 (𝜑 → Word (0..^(♯‘𝐹)) ⊆ Word (0..^((♯‘𝐹) + 1)))
145 iswrdi 14552 . . . . . . . . . . 11 (𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐹)) → 𝐶 ∈ Word (0..^(♯‘𝐹)))
14662, 145syl 17 . . . . . . . . . 10 (𝜑𝐶 ∈ Word (0..^(♯‘𝐹)))
147144, 146sseldd 3995 . . . . . . . . 9 (𝜑𝐶 ∈ Word (0..^((♯‘𝐹) + 1)))
148 ccatws1len 14654 . . . . . . . . 9 (𝐶 ∈ Word (0..^((♯‘𝐹) + 1)) → (♯‘(𝐶 ++ ⟨“(♯‘𝐹)”⟩)) = ((♯‘𝐶) + 1))
149147, 148syl 17 . . . . . . . 8 (𝜑 → (♯‘(𝐶 ++ ⟨“(♯‘𝐹)”⟩)) = ((♯‘𝐶) + 1))
150149, 96, 783eqtrrd 2779 . . . . . . 7 (𝜑 → (♯‘𝐻) = (♯‘(𝐶 ++ ⟨“(♯‘𝐹)”⟩)))
151142, 133sseqtrd 4035 . . . . . . . . . 10 (𝜑 → (0..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐻)))
15262, 151fssd 6753 . . . . . . . . 9 (𝜑𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐻)))
153 iswrdi 14552 . . . . . . . . 9 (𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐻)) → 𝐶 ∈ Word (0..^(♯‘𝐻)))
154152, 153syl 17 . . . . . . . 8 (𝜑𝐶 ∈ Word (0..^(♯‘𝐻)))
155 fzonn0p1 13777 . . . . . . . . . 10 ((♯‘𝐹) ∈ ℕ0 → (♯‘𝐹) ∈ (0..^((♯‘𝐹) + 1)))
15670, 155syl 17 . . . . . . . . 9 (𝜑 → (♯‘𝐹) ∈ (0..^((♯‘𝐹) + 1)))
157156, 133eleqtrd 2840 . . . . . . . 8 (𝜑 → (♯‘𝐹) ∈ (0..^(♯‘𝐻)))
158 ccatws1cl 14650 . . . . . . . 8 ((𝐶 ∈ Word (0..^(♯‘𝐻)) ∧ (♯‘𝐹) ∈ (0..^(♯‘𝐻))) → (𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∈ Word (0..^(♯‘𝐻)))
159154, 157, 158syl2anc 584 . . . . . . 7 (𝜑 → (𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∈ Word (0..^(♯‘𝐻)))
160150, 159wrdfd 32902 . . . . . 6 (𝜑 → (𝐶 ++ ⟨“(♯‘𝐹)”⟩):(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)))
161160, 130fcod 6761 . . . . 5 (𝜑 → ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆):(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)))
162 fnfco 6773 . . . . 5 (((𝐹 ++ ⟨“𝑄”⟩) Fn (0..^(♯‘𝐻)) ∧ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆):(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻))) → ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆)) Fn (0..^(♯‘𝐻)))
163140, 161, 162syl2anc 584 . . . 4 (𝜑 → ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆)) Fn (0..^(♯‘𝐻)))
164 ovexd 7465 . . . 4 (𝜑 → (0..^(♯‘𝐻)) ∈ V)
165 inidm 4234 . . . 4 ((0..^(♯‘𝐻)) ∩ (0..^(♯‘𝐻))) = (0..^(♯‘𝐻))
166132, 163, 164, 164, 165offn 7709 . . 3 (𝜑 → (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))) Fn (0..^(♯‘𝐻)))
167 1arithidomlem.10 . . . 4 (𝜑 → (𝐻𝑆) = (((𝐻𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻𝐾)”⟩))
168 eqid 2734 . . . . . . . . 9 (♯‘𝐹) = (♯‘𝐹)
169168, 1, 135, 60ccatws1f1olast 32921 . . . . . . . 8 (𝜑 → ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) = ((𝐹𝐶) ++ ⟨“𝑄”⟩))
170169oveq2d 7446 . . . . . . 7 (𝜑 → ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) = ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹𝐶) ++ ⟨“𝑄”⟩)))
171123s1cld 14637 . . . . . . . 8 (𝜑 → ⟨“𝑇”⟩ ∈ Word 𝑈)
172 iswrdi 14552 . . . . . . . . 9 ((𝐹𝐶):(0..^(♯‘𝐹))⟶𝑃 → (𝐹𝐶) ∈ Word 𝑃)
17363, 172syl 17 . . . . . . . 8 (𝜑 → (𝐹𝐶) ∈ Word 𝑃)
174135s1cld 14637 . . . . . . . 8 (𝜑 → ⟨“𝑄”⟩ ∈ Word 𝑃)
175 lenco 14867 . . . . . . . . . 10 ((𝐶 ∈ Word (0..^(♯‘𝐹)) ∧ 𝐹:(0..^(♯‘𝐹))⟶𝑃) → (♯‘(𝐹𝐶)) = (♯‘𝐶))
176146, 59, 175syl2anc 584 . . . . . . . . 9 (𝜑 → (♯‘(𝐹𝐶)) = (♯‘𝐶))
17785, 176, 1173eqtr4rd 2785 . . . . . . . 8 (𝜑 → (♯‘𝐷) = (♯‘(𝐹𝐶)))
178 s1len 14640 . . . . . . . . . 10 (♯‘⟨“𝑇”⟩) = 1
179 s1len 14640 . . . . . . . . . 10 (♯‘⟨“𝑄”⟩) = 1
180178, 179eqtr4i 2765 . . . . . . . . 9 (♯‘⟨“𝑇”⟩) = (♯‘⟨“𝑄”⟩)
181180a1i 11 . . . . . . . 8 (𝜑 → (♯‘⟨“𝑇”⟩) = (♯‘⟨“𝑄”⟩))
182112, 171, 173, 174, 177, 181ofccat 15004 . . . . . . 7 (𝜑 → ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹𝐶) ++ ⟨“𝑄”⟩)) = ((𝐷f · (𝐹𝐶)) ++ (⟨“𝑇”⟩ ∘f · ⟨“𝑄”⟩)))
183170, 182eqtrd 2774 . . . . . 6 (𝜑 → ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) = ((𝐷f · (𝐹𝐶)) ++ (⟨“𝑇”⟩ ∘f · ⟨“𝑄”⟩)))
184139, 160fcod 6761 . . . . . . . . . . 11 (𝜑 → ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)):(0..^(♯‘𝐻))⟶𝑃)
185184ffnd 6737 . . . . . . . . . 10 (𝜑 → ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) Fn (0..^(♯‘𝐻)))
186128, 185, 130, 164, 164, 164, 165ofco 7721 . . . . . . . . 9 (𝜑 → (((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ 𝑆) = (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)))
187186coeq1d 5874 . . . . . . . 8 (𝜑 → ((((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ 𝑆) ∘ 𝑆) = ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)) ∘ 𝑆))
188 coass 6286 . . . . . . . 8 ((((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ 𝑆) ∘ 𝑆) = (((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ (𝑆𝑆))
189187, 188eqtr3di 2789 . . . . . . 7 (𝜑 → ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)) ∘ 𝑆) = (((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ (𝑆𝑆)))
190 f1of1 6847 . . . . . . . . . 10 (𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)) → 𝑆:(0..^(♯‘𝐻))–1-1→(0..^(♯‘𝐻)))
1916, 190syl 17 . . . . . . . . 9 (𝜑𝑆:(0..^(♯‘𝐻))–1-1→(0..^(♯‘𝐻)))
192 f1cocnv1 6878 . . . . . . . . 9 (𝑆:(0..^(♯‘𝐻))–1-1→(0..^(♯‘𝐻)) → (𝑆𝑆) = ( I ↾ (0..^(♯‘𝐻))))
193191, 192syl 17 . . . . . . . 8 (𝜑 → (𝑆𝑆) = ( I ↾ (0..^(♯‘𝐻))))
194193coeq2d 5875 . . . . . . 7 (𝜑 → (((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ (𝑆𝑆)) = (((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ ( I ↾ (0..^(♯‘𝐻)))))
19554, 127, 184, 164, 164, 165off 7714 . . . . . . . 8 (𝜑 → ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))):(0..^(♯‘𝐻))⟶(Base‘𝑅))
196 fcoi1 6782 . . . . . . . 8 (((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))):(0..^(♯‘𝐻))⟶(Base‘𝑅) → (((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ ( I ↾ (0..^(♯‘𝐻)))) = ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))))
197195, 196syl 17 . . . . . . 7 (𝜑 → (((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ ( I ↾ (0..^(♯‘𝐻)))) = ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))))
198189, 194, 1973eqtrd 2778 . . . . . 6 (𝜑 → ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)) ∘ 𝑆) = ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))))
199 ofs1 15005 . . . . . . . . 9 ((𝑇𝑈𝑄𝑃) → (⟨“𝑇”⟩ ∘f · ⟨“𝑄”⟩) = ⟨“(𝑇 · 𝑄)”⟩)
200123, 135, 199syl2anc 584 . . . . . . . 8 (𝜑 → (⟨“𝑇”⟩ ∘f · ⟨“𝑄”⟩) = ⟨“(𝑇 · 𝑄)”⟩)
201 1arithidomlem.8 . . . . . . . . 9 (𝜑 → (𝑇 · 𝑄) = (𝐻𝐾))
202201s1eqd 14635 . . . . . . . 8 (𝜑 → ⟨“(𝑇 · 𝑄)”⟩ = ⟨“(𝐻𝐾)”⟩)
203200, 202eqtr2d 2775 . . . . . . 7 (𝜑 → ⟨“(𝐻𝐾)”⟩ = (⟨“𝑇”⟩ ∘f · ⟨“𝑄”⟩))
2044, 203oveq12d 7448 . . . . . 6 (𝜑 → (((𝐻𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻𝐾)”⟩) = ((𝐷f · (𝐹𝐶)) ++ (⟨“𝑇”⟩ ∘f · ⟨“𝑄”⟩)))
205183, 198, 2043eqtr4rd 2785 . . . . 5 (𝜑 → (((𝐻𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻𝐾)”⟩) = ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)) ∘ 𝑆))
206 coass 6286 . . . . . . 7 (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆) = ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))
207206oveq2i 7441 . . . . . 6 (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)) = (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆)))
208207coeq1i 5872 . . . . 5 ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)) ∘ 𝑆) = ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))) ∘ 𝑆)
209205, 208eqtrdi 2790 . . . 4 (𝜑 → (((𝐻𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻𝐾)”⟩) = ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))) ∘ 𝑆))
210167, 209eqtrd 2774 . . 3 (𝜑 → (𝐻𝑆) = ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))) ∘ 𝑆))
211 cocan2 7311 . . . 4 ((𝑆:(0..^(♯‘𝐻))–onto→(0..^(♯‘𝐻)) ∧ 𝐻 Fn (0..^(♯‘𝐻)) ∧ (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))) Fn (0..^(♯‘𝐻))) → ((𝐻𝑆) = ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))) ∘ 𝑆) ↔ 𝐻 = (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆)))))
212211biimpa 476 . . 3 (((𝑆:(0..^(♯‘𝐻))–onto→(0..^(♯‘𝐻)) ∧ 𝐻 Fn (0..^(♯‘𝐻)) ∧ (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))) Fn (0..^(♯‘𝐻))) ∧ (𝐻𝑆) = ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))) ∘ 𝑆)) → 𝐻 = (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))))
213109, 110, 166, 210, 212syl31anc 1372 . 2 (𝜑𝐻 = (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))))
214107, 213jca 511 1 (𝜑 → (((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆):(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩)))–1-1-onto→(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))) ∧ 𝐻 = (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086   = wceq 1536  wex 1775  wcel 2105  wral 3058  wrex 3067  Vcvv 3477  wss 3962   class class class wbr 5147   I cid 5581  ccnv 5687  dom cdm 5688  cres 5690  ccom 5692   Fn wfn 6557  wf 6558  1-1wf1 6559  ontowfo 6560  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  f cof 7694  m cmap 8864  cc 11150  0cc0 11152  1c1 11153   + caddc 11155   < clt 11292  cle 11293  cmin 11489  cn 12263  0cn0 12523  ...cfz 13543  ..^cfzo 13690  chash 14365  Word cword 14548   ++ cconcat 14604  ⟨“cs1 14629   prefix cpfx 14704  Basecbs 17244  .rcmulr 17298   Σg cgsu 17486  mulGrpcmgp 20151  Ringcrg 20250  rcdsr 20370  Unitcui 20371  RPrimecrpm 20448  IDomncidom 20709
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
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  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-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-of 7696  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-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-n0 12524  df-z 12611  df-uz 12876  df-fz 13544  df-fzo 13691  df-hash 14366  df-word 14549  df-concat 14605  df-s1 14630  df-substr 14675  df-pfx 14705  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-plusg 17310  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-mgp 20152  df-ring 20252  df-cring 20253  df-dvdsr 20373  df-unit 20374  df-rprm 20449  df-idom 20712
This theorem is referenced by:  1arithidom  33544
  Copyright terms: Public domain W3C validator