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 33564
Description: Lemma for 1arithidom 33565: 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 14658 . . . . . 6 (𝐹 ∈ Word 𝑃 → (♯‘(𝐹 ++ ⟨“𝑄”⟩)) = ((♯‘𝐹) + 1))
31, 2syl 17 . . . . 5 (𝜑 → (♯‘(𝐹 ++ ⟨“𝑄”⟩)) = ((♯‘𝐹) + 1))
4 1arithidomlem.15 . . . . . . . . . 10 (𝜑 → ((𝐻𝑆) prefix ((♯‘𝐻) − 1)) = (𝐷f · (𝐹𝐶)))
54dmeqd 5916 . . . . . . . . 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 14556 . . . . . . . . . . . . 13 (𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)) → 𝑆 ∈ Word (0..^(♯‘𝐻)))
96, 7, 83syl 18 . . . . . . . . . . . 12 (𝜑𝑆 ∈ Word (0..^(♯‘𝐻)))
10 eqidd 2738 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐻) = (♯‘𝐻))
11 1arithidomlem.3 . . . . . . . . . . . . 13 (𝜑𝐻 ∈ Word 𝑃)
1210, 11wrdfd 32918 . . . . . . . . . . . 12 (𝜑𝐻:(0..^(♯‘𝐻))⟶𝑃)
13 wrdco 14870 . . . . . . . . . . . 12 ((𝑆 ∈ Word (0..^(♯‘𝐻)) ∧ 𝐻:(0..^(♯‘𝐻))⟶𝑃) → (𝐻𝑆) ∈ Word 𝑃)
149, 12, 13syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝐻𝑆) ∈ Word 𝑃)
15 1arithidomlem.5 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ (0..^(♯‘𝐻)))
16 elfzo0 13740 . . . . . . . . . . . . . 14 (𝐾 ∈ (0..^(♯‘𝐻)) ↔ (𝐾 ∈ ℕ0 ∧ (♯‘𝐻) ∈ ℕ ∧ 𝐾 < (♯‘𝐻)))
1716simp2bi 1147 . . . . . . . . . . . . 13 (𝐾 ∈ (0..^(♯‘𝐻)) → (♯‘𝐻) ∈ ℕ)
18 nnm1nn0 12567 . . . . . . . . . . . . 13 ((♯‘𝐻) ∈ ℕ → ((♯‘𝐻) − 1) ∈ ℕ0)
1915, 17, 183syl 18 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ0)
20 lenco 14871 . . . . . . . . . . . . . 14 ((𝑆 ∈ Word (0..^(♯‘𝐻)) ∧ 𝐻:(0..^(♯‘𝐻))⟶𝑃) → (♯‘(𝐻𝑆)) = (♯‘𝑆))
219, 12, 20syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐻𝑆)) = (♯‘𝑆))
22 lencl 14571 . . . . . . . . . . . . . 14 (𝑆 ∈ Word (0..^(♯‘𝐻)) → (♯‘𝑆) ∈ ℕ0)
239, 22syl 17 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝑆) ∈ ℕ0)
2421, 23eqeltrd 2841 . . . . . . . . . . . 12 (𝜑 → (♯‘(𝐻𝑆)) ∈ ℕ0)
25 lencl 14571 . . . . . . . . . . . . . . . 16 (𝐻 ∈ Word 𝑃 → (♯‘𝐻) ∈ ℕ0)
2611, 25syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘𝐻) ∈ ℕ0)
2726nn0red 12588 . . . . . . . . . . . . . 14 (𝜑 → (♯‘𝐻) ∈ ℝ)
2827lem1d 12201 . . . . . . . . . . . . 13 (𝜑 → ((♯‘𝐻) − 1) ≤ (♯‘𝐻))
296, 7syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)))
30 ffn 6736 . . . . . . . . . . . . . . 15 (𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)) → 𝑆 Fn (0..^(♯‘𝐻)))
31 hashfn 14414 . . . . . . . . . . . . . . 15 (𝑆 Fn (0..^(♯‘𝐻)) → (♯‘𝑆) = (♯‘(0..^(♯‘𝐻))))
3229, 30, 313syl 18 . . . . . . . . . . . . . 14 (𝜑 → (♯‘𝑆) = (♯‘(0..^(♯‘𝐻))))
33 hashfzo0 14469 . . . . . . . . . . . . . . 15 ((♯‘𝐻) ∈ ℕ0 → (♯‘(0..^(♯‘𝐻))) = (♯‘𝐻))
3411, 25, 333syl 18 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(0..^(♯‘𝐻))) = (♯‘𝐻))
3521, 32, 343eqtrrd 2782 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐻) = (♯‘(𝐻𝑆)))
3628, 35breqtrd 5169 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝐻) − 1) ≤ (♯‘(𝐻𝑆)))
37 elfz2nn0 13658 . . . . . . . . . . . 12 (((♯‘𝐻) − 1) ∈ (0...(♯‘(𝐻𝑆))) ↔ (((♯‘𝐻) − 1) ∈ ℕ0 ∧ (♯‘(𝐻𝑆)) ∈ ℕ0 ∧ ((♯‘𝐻) − 1) ≤ (♯‘(𝐻𝑆))))
3819, 24, 36, 37syl3anbrc 1344 . . . . . . . . . . 11 (𝜑 → ((♯‘𝐻) − 1) ∈ (0...(♯‘(𝐻𝑆))))
39 pfxfn 14719 . . . . . . . . . . 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 2737 . . . . . . . . . . . 12 (Base‘𝑅) = (Base‘𝑅)
43 1arithidom.t . . . . . . . . . . . 12 · = (.r𝑅)
44 1arithidom.r . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ IDomn)
4544idomringd 20728 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ Ring)
4645adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑈𝑦𝑃)) → 𝑅 ∈ Ring)
47 1arithidom.u . . . . . . . . . . . . . 14 𝑈 = (Unit‘𝑅)
4842, 47unitcl 20375 . . . . . . . . . . . . 13 (𝑥𝑈𝑥 ∈ (Base‘𝑅))
4948ad2antrl 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑈𝑦𝑃)) → 𝑥 ∈ (Base‘𝑅))
50 1arithidom.i . . . . . . . . . . . . 13 𝑃 = (RPrime‘𝑅)
5144adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑈𝑦𝑃)) → 𝑅 ∈ IDomn)
52 simprr 773 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑈𝑦𝑃)) → 𝑦𝑃)
5342, 50, 51, 52rprmcl 33546 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑈𝑦𝑃)) → 𝑦 ∈ (Base‘𝑅))
5442, 43, 46, 49, 53ringcld 20257 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑈𝑦𝑃)) → (𝑥 · 𝑦) ∈ (Base‘𝑅))
55 1arithidomlem.13 . . . . . . . . . . . 12 (𝜑𝐷 ∈ (𝑈m (0..^(♯‘𝐹))))
56 elmapi 8889 . . . . . . . . . . . 12 (𝐷 ∈ (𝑈m (0..^(♯‘𝐹))) → 𝐷:(0..^(♯‘𝐹))⟶𝑈)
5755, 56syl 17 . . . . . . . . . . 11 (𝜑𝐷:(0..^(♯‘𝐹))⟶𝑈)
58 eqidd 2738 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐹) = (♯‘𝐹))
5958, 1wrdfd 32918 . . . . . . . . . . . 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 7466 . . . . . . . . . . 11 (𝜑 → (0..^(♯‘𝐹)) ∈ V)
65 inidm 4227 . . . . . . . . . . 11 ((0..^(♯‘𝐹)) ∩ (0..^(♯‘𝐹))) = (0..^(♯‘𝐹))
6654, 57, 63, 64, 64, 65off 7715 . . . . . . . . . 10 (𝜑 → (𝐷f · (𝐹𝐶)):(0..^(♯‘𝐹))⟶(Base‘𝑅))
6766fdmd 6746 . . . . . . . . 9 (𝜑 → dom (𝐷f · (𝐹𝐶)) = (0..^(♯‘𝐹)))
685, 41, 673eqtr3d 2785 . . . . . . . 8 (𝜑 → (0..^((♯‘𝐻) − 1)) = (0..^(♯‘𝐹)))
69 lencl 14571 . . . . . . . . . 10 (𝐹 ∈ Word 𝑃 → (♯‘𝐹) ∈ ℕ0)
701, 69syl 17 . . . . . . . . 9 (𝜑 → (♯‘𝐹) ∈ ℕ0)
7119, 70fzo0opth 32807 . . . . . . . 8 (𝜑 → ((0..^((♯‘𝐻) − 1)) = (0..^(♯‘𝐹)) ↔ ((♯‘𝐻) − 1) = (♯‘𝐹)))
7268, 71mpbid 232 . . . . . . 7 (𝜑 → ((♯‘𝐻) − 1) = (♯‘𝐹))
7372oveq1d 7446 . . . . . 6 (𝜑 → (((♯‘𝐻) − 1) + 1) = ((♯‘𝐹) + 1))
7415, 17syl 17 . . . . . . . 8 (𝜑 → (♯‘𝐻) ∈ ℕ)
7574nncnd 12282 . . . . . . 7 (𝜑 → (♯‘𝐻) ∈ ℂ)
76 npcan1 11688 . . . . . . 7 ((♯‘𝐻) ∈ ℂ → (((♯‘𝐻) − 1) + 1) = (♯‘𝐻))
7775, 76syl 17 . . . . . 6 (𝜑 → (((♯‘𝐻) − 1) + 1) = (♯‘𝐻))
7873, 77eqtr3d 2779 . . . . 5 (𝜑 → ((♯‘𝐹) + 1) = (♯‘𝐻))
793, 78eqtrd 2777 . . . 4 (𝜑 → (♯‘(𝐹 ++ ⟨“𝑄”⟩)) = (♯‘𝐻))
8079oveq2d 7447 . . 3 (𝜑 → (0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))) = (0..^(♯‘𝐻)))
81 eqid 2737 . . . . . 6 (♯‘𝐶) = (♯‘𝐶)
82 eqid 2737 . . . . . 6 (0..^((♯‘𝐶) + 1)) = (0..^((♯‘𝐶) + 1))
83 f1ofn 6849 . . . . . . . . . 10 (𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) → 𝐶 Fn (0..^(♯‘𝐹)))
84 hashfn 14414 . . . . . . . . . 10 (𝐶 Fn (0..^(♯‘𝐹)) → (♯‘𝐶) = (♯‘(0..^(♯‘𝐹))))
8560, 83, 843syl 18 . . . . . . . . 9 (𝜑 → (♯‘𝐶) = (♯‘(0..^(♯‘𝐹))))
86 hashfzo0 14469 . . . . . . . . . 10 ((♯‘𝐹) ∈ ℕ0 → (♯‘(0..^(♯‘𝐹))) = (♯‘𝐹))
8770, 86syl 17 . . . . . . . . 9 (𝜑 → (♯‘(0..^(♯‘𝐹))) = (♯‘𝐹))
8885, 87eqtrd 2777 . . . . . . . 8 (𝜑 → (♯‘𝐶) = (♯‘𝐹))
8988oveq2d 7447 . . . . . . 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 32936 . . . . 5 (𝜑 → (𝐶 ++ ⟨“(♯‘𝐶)”⟩):(0..^((♯‘𝐶) + 1))–1-1-onto→(0..^((♯‘𝐶) + 1)))
9488s1eqd 14639 . . . . . . 7 (𝜑 → ⟨“(♯‘𝐶)”⟩ = ⟨“(♯‘𝐹)”⟩)
9594oveq2d 7447 . . . . . 6 (𝜑 → (𝐶 ++ ⟨“(♯‘𝐶)”⟩) = (𝐶 ++ ⟨“(♯‘𝐹)”⟩))
9688oveq1d 7446 . . . . . . . 8 (𝜑 → ((♯‘𝐶) + 1) = ((♯‘𝐹) + 1))
9796, 78eqtrd 2777 . . . . . . 7 (𝜑 → ((♯‘𝐶) + 1) = (♯‘𝐻))
9897oveq2d 7447 . . . . . 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 14556 . . . . . . . . . . 11 (𝐷:(0..^(♯‘𝐹))⟶𝑈𝐷 ∈ Word 𝑈)
11257, 111syl 17 . . . . . . . . . 10 (𝜑𝐷 ∈ Word 𝑈)
113 ccatws1len 14658 . . . . . . . . . 10 (𝐷 ∈ Word 𝑈 → (♯‘(𝐷 ++ ⟨“𝑇”⟩)) = ((♯‘𝐷) + 1))
114112, 113syl 17 . . . . . . . . 9 (𝜑 → (♯‘(𝐷 ++ ⟨“𝑇”⟩)) = ((♯‘𝐷) + 1))
115 elmapfn 8905 . . . . . . . . . . . 12 (𝐷 ∈ (𝑈m (0..^(♯‘𝐹))) → 𝐷 Fn (0..^(♯‘𝐹)))
116 hashfn 14414 . . . . . . . . . . . 12 (𝐷 Fn (0..^(♯‘𝐹)) → (♯‘𝐷) = (♯‘(0..^(♯‘𝐹))))
11755, 115, 1163syl 18 . . . . . . . . . . 11 (𝜑 → (♯‘𝐷) = (♯‘(0..^(♯‘𝐹))))
118117, 87eqtrd 2777 . . . . . . . . . 10 (𝜑 → (♯‘𝐷) = (♯‘𝐹))
119118oveq1d 7446 . . . . . . . . 9 (𝜑 → ((♯‘𝐷) + 1) = ((♯‘𝐹) + 1))
120114, 119, 783eqtrd 2781 . . . . . . . 8 (𝜑 → (♯‘(𝐷 ++ ⟨“𝑇”⟩)) = (♯‘𝐻))
121120oveq2d 7447 . . . . . . 7 (𝜑 → (0..^(♯‘(𝐷 ++ ⟨“𝑇”⟩))) = (0..^(♯‘𝐻)))
122 eqidd 2738 . . . . . . . 8 (𝜑 → (♯‘(𝐷 ++ ⟨“𝑇”⟩)) = (♯‘(𝐷 ++ ⟨“𝑇”⟩)))
123 1arithidomlem.7 . . . . . . . . 9 (𝜑𝑇𝑈)
124 ccatws1cl 14654 . . . . . . . . 9 ((𝐷 ∈ Word 𝑈𝑇𝑈) → (𝐷 ++ ⟨“𝑇”⟩) ∈ Word 𝑈)
125112, 123, 124syl2anc 584 . . . . . . . 8 (𝜑 → (𝐷 ++ ⟨“𝑇”⟩) ∈ Word 𝑈)
126122, 125wrdfd 32918 . . . . . . 7 (𝜑 → (𝐷 ++ ⟨“𝑇”⟩):(0..^(♯‘(𝐷 ++ ⟨“𝑇”⟩)))⟶𝑈)
127121, 126feq2dd 32632 . . . . . 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 7447 . . . . . . 7 (𝜑 → (0..^((♯‘𝐹) + 1)) = (0..^(♯‘𝐻)))
1343eqcomd 2743 . . . . . . . 8 (𝜑 → ((♯‘𝐹) + 1) = (♯‘(𝐹 ++ ⟨“𝑄”⟩)))
135 1arithidomlem.1 . . . . . . . . 9 (𝜑𝑄𝑃)
136 ccatws1cl 14654 . . . . . . . . 9 ((𝐹 ∈ Word 𝑃𝑄𝑃) → (𝐹 ++ ⟨“𝑄”⟩) ∈ Word 𝑃)
1371, 135, 136syl2anc 584 . . . . . . . 8 (𝜑 → (𝐹 ++ ⟨“𝑄”⟩) ∈ Word 𝑃)
138134, 137wrdfd 32918 . . . . . . 7 (𝜑 → (𝐹 ++ ⟨“𝑄”⟩):(0..^((♯‘𝐹) + 1))⟶𝑃)
139133, 138feq2dd 32632 . . . . . 6 (𝜑 → (𝐹 ++ ⟨“𝑄”⟩):(0..^(♯‘𝐻))⟶𝑃)
140139ffnd 6737 . . . . 5 (𝜑 → (𝐹 ++ ⟨“𝑄”⟩) Fn (0..^(♯‘𝐻)))
141 fzossfzop1 13782 . . . . . . . . . . . 12 ((♯‘𝐹) ∈ ℕ0 → (0..^(♯‘𝐹)) ⊆ (0..^((♯‘𝐹) + 1)))
14270, 141syl 17 . . . . . . . . . . 11 (𝜑 → (0..^(♯‘𝐹)) ⊆ (0..^((♯‘𝐹) + 1)))
143 sswrd 14560 . . . . . . . . . . 11 ((0..^(♯‘𝐹)) ⊆ (0..^((♯‘𝐹) + 1)) → Word (0..^(♯‘𝐹)) ⊆ Word (0..^((♯‘𝐹) + 1)))
144142, 143syl 17 . . . . . . . . . 10 (𝜑 → Word (0..^(♯‘𝐹)) ⊆ Word (0..^((♯‘𝐹) + 1)))
145 iswrdi 14556 . . . . . . . . . . 11 (𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐹)) → 𝐶 ∈ Word (0..^(♯‘𝐹)))
14662, 145syl 17 . . . . . . . . . 10 (𝜑𝐶 ∈ Word (0..^(♯‘𝐹)))
147144, 146sseldd 3984 . . . . . . . . 9 (𝜑𝐶 ∈ Word (0..^((♯‘𝐹) + 1)))
148 ccatws1len 14658 . . . . . . . . 9 (𝐶 ∈ Word (0..^((♯‘𝐹) + 1)) → (♯‘(𝐶 ++ ⟨“(♯‘𝐹)”⟩)) = ((♯‘𝐶) + 1))
149147, 148syl 17 . . . . . . . 8 (𝜑 → (♯‘(𝐶 ++ ⟨“(♯‘𝐹)”⟩)) = ((♯‘𝐶) + 1))
150149, 96, 783eqtrrd 2782 . . . . . . 7 (𝜑 → (♯‘𝐻) = (♯‘(𝐶 ++ ⟨“(♯‘𝐹)”⟩)))
151142, 133sseqtrd 4020 . . . . . . . . . 10 (𝜑 → (0..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐻)))
15262, 151fssd 6753 . . . . . . . . 9 (𝜑𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐻)))
153 iswrdi 14556 . . . . . . . . 9 (𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐻)) → 𝐶 ∈ Word (0..^(♯‘𝐻)))
154152, 153syl 17 . . . . . . . 8 (𝜑𝐶 ∈ Word (0..^(♯‘𝐻)))
155 fzonn0p1 13781 . . . . . . . . . 10 ((♯‘𝐹) ∈ ℕ0 → (♯‘𝐹) ∈ (0..^((♯‘𝐹) + 1)))
15670, 155syl 17 . . . . . . . . 9 (𝜑 → (♯‘𝐹) ∈ (0..^((♯‘𝐹) + 1)))
157156, 133eleqtrd 2843 . . . . . . . 8 (𝜑 → (♯‘𝐹) ∈ (0..^(♯‘𝐻)))
158 ccatws1cl 14654 . . . . . . . 8 ((𝐶 ∈ Word (0..^(♯‘𝐻)) ∧ (♯‘𝐹) ∈ (0..^(♯‘𝐻))) → (𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∈ Word (0..^(♯‘𝐻)))
159154, 157, 158syl2anc 584 . . . . . . 7 (𝜑 → (𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∈ Word (0..^(♯‘𝐻)))
160150, 159wrdfd 32918 . . . . . 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 7466 . . . 4 (𝜑 → (0..^(♯‘𝐻)) ∈ V)
165 inidm 4227 . . . 4 ((0..^(♯‘𝐻)) ∩ (0..^(♯‘𝐻))) = (0..^(♯‘𝐻))
166132, 163, 164, 164, 165offn 7710 . . 3 (𝜑 → (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))) Fn (0..^(♯‘𝐻)))
167 1arithidomlem.10 . . . 4 (𝜑 → (𝐻𝑆) = (((𝐻𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻𝐾)”⟩))
168 eqid 2737 . . . . . . . . 9 (♯‘𝐹) = (♯‘𝐹)
169168, 1, 135, 60ccatws1f1olast 32937 . . . . . . . 8 (𝜑 → ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) = ((𝐹𝐶) ++ ⟨“𝑄”⟩))
170169oveq2d 7447 . . . . . . 7 (𝜑 → ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) = ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹𝐶) ++ ⟨“𝑄”⟩)))
171123s1cld 14641 . . . . . . . 8 (𝜑 → ⟨“𝑇”⟩ ∈ Word 𝑈)
172 iswrdi 14556 . . . . . . . . 9 ((𝐹𝐶):(0..^(♯‘𝐹))⟶𝑃 → (𝐹𝐶) ∈ Word 𝑃)
17363, 172syl 17 . . . . . . . 8 (𝜑 → (𝐹𝐶) ∈ Word 𝑃)
174135s1cld 14641 . . . . . . . 8 (𝜑 → ⟨“𝑄”⟩ ∈ Word 𝑃)
175 lenco 14871 . . . . . . . . . 10 ((𝐶 ∈ Word (0..^(♯‘𝐹)) ∧ 𝐹:(0..^(♯‘𝐹))⟶𝑃) → (♯‘(𝐹𝐶)) = (♯‘𝐶))
176146, 59, 175syl2anc 584 . . . . . . . . 9 (𝜑 → (♯‘(𝐹𝐶)) = (♯‘𝐶))
17785, 176, 1173eqtr4rd 2788 . . . . . . . 8 (𝜑 → (♯‘𝐷) = (♯‘(𝐹𝐶)))
178 s1len 14644 . . . . . . . . . 10 (♯‘⟨“𝑇”⟩) = 1
179 s1len 14644 . . . . . . . . . 10 (♯‘⟨“𝑄”⟩) = 1
180178, 179eqtr4i 2768 . . . . . . . . 9 (♯‘⟨“𝑇”⟩) = (♯‘⟨“𝑄”⟩)
181180a1i 11 . . . . . . . 8 (𝜑 → (♯‘⟨“𝑇”⟩) = (♯‘⟨“𝑄”⟩))
182112, 171, 173, 174, 177, 181ofccat 15008 . . . . . . 7 (𝜑 → ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹𝐶) ++ ⟨“𝑄”⟩)) = ((𝐷f · (𝐹𝐶)) ++ (⟨“𝑇”⟩ ∘f · ⟨“𝑄”⟩)))
183170, 182eqtrd 2777 . . . . . 6 (𝜑 → ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) = ((𝐷f · (𝐹𝐶)) ++ (⟨“𝑇”⟩ ∘f · ⟨“𝑄”⟩)))
184139, 160fcod 6761 . . . . . . . . . . 11 (𝜑 → ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)):(0..^(♯‘𝐻))⟶𝑃)
185184ffnd 6737 . . . . . . . . . 10 (𝜑 → ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) Fn (0..^(♯‘𝐻)))
186128, 185, 130, 164, 164, 164, 165ofco 7722 . . . . . . . . 9 (𝜑 → (((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ 𝑆) = (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)))
187186coeq1d 5872 . . . . . . . 8 (𝜑 → ((((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ 𝑆) ∘ 𝑆) = ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)) ∘ 𝑆))
188 coass 6285 . . . . . . . 8 ((((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ 𝑆) ∘ 𝑆) = (((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ (𝑆𝑆))
189187, 188eqtr3di 2792 . . . . . . 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 5873 . . . . . . 7 (𝜑 → (((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ (𝑆𝑆)) = (((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))) ∘ ( I ↾ (0..^(♯‘𝐻)))))
19554, 127, 184, 164, 164, 165off 7715 . . . . . . . 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 2781 . . . . . 6 (𝜑 → ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)) ∘ 𝑆) = ((𝐷 ++ ⟨“𝑇”⟩) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩))))
199 ofs1 15009 . . . . . . . . 9 ((𝑇𝑈𝑄𝑃) → (⟨“𝑇”⟩ ∘f · ⟨“𝑄”⟩) = ⟨“(𝑇 · 𝑄)”⟩)
200123, 135, 199syl2anc 584 . . . . . . . 8 (𝜑 → (⟨“𝑇”⟩ ∘f · ⟨“𝑄”⟩) = ⟨“(𝑇 · 𝑄)”⟩)
201 1arithidomlem.8 . . . . . . . . 9 (𝜑 → (𝑇 · 𝑄) = (𝐻𝐾))
202201s1eqd 14639 . . . . . . . 8 (𝜑 → ⟨“(𝑇 · 𝑄)”⟩ = ⟨“(𝐻𝐾)”⟩)
203200, 202eqtr2d 2778 . . . . . . 7 (𝜑 → ⟨“(𝐻𝐾)”⟩ = (⟨“𝑇”⟩ ∘f · ⟨“𝑄”⟩))
2044, 203oveq12d 7449 . . . . . 6 (𝜑 → (((𝐻𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻𝐾)”⟩) = ((𝐷f · (𝐹𝐶)) ++ (⟨“𝑇”⟩ ∘f · ⟨“𝑄”⟩)))
205183, 198, 2043eqtr4rd 2788 . . . . 5 (𝜑 → (((𝐻𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻𝐾)”⟩) = ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)) ∘ 𝑆))
206 coass 6285 . . . . . . 7 (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆) = ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))
207206oveq2i 7442 . . . . . 6 (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)) = (((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆)))
208207coeq1i 5870 . . . . 5 ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · (((𝐹 ++ ⟨“𝑄”⟩) ∘ (𝐶 ++ ⟨“(♯‘𝐹)”⟩)) ∘ 𝑆)) ∘ 𝑆) = ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))) ∘ 𝑆)
209205, 208eqtrdi 2793 . . . 4 (𝜑 → (((𝐻𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻𝐾)”⟩) = ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))) ∘ 𝑆))
210167, 209eqtrd 2777 . . 3 (𝜑 → (𝐻𝑆) = ((((𝐷 ++ ⟨“𝑇”⟩) ∘ 𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ 𝑆))) ∘ 𝑆))
211 cocan2 7312 . . . 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 1375 . 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 1087   = wceq 1540  wex 1779  wcel 2108  wral 3061  wrex 3070  Vcvv 3480  wss 3951   class class class wbr 5143   I cid 5577  ccnv 5684  dom cdm 5685  cres 5687  ccom 5689   Fn wfn 6556  wf 6557  1-1wf1 6558  ontowfo 6559  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  f cof 7695  m cmap 8866  cc 11153  0cc0 11155  1c1 11156   + caddc 11158   < clt 11295  cle 11296  cmin 11492  cn 12266  0cn0 12526  ...cfz 13547  ..^cfzo 13694  chash 14369  Word cword 14552   ++ cconcat 14608  ⟨“cs1 14633   prefix cpfx 14708  Basecbs 17247  .rcmulr 17298   Σg cgsu 17485  mulGrpcmgp 20137  Ringcrg 20230  rcdsr 20354  Unitcui 20355  RPrimecrpm 20432  IDomncidom 20693
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-fzo 13695  df-hash 14370  df-word 14553  df-concat 14609  df-s1 14634  df-substr 14679  df-pfx 14709  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-plusg 17310  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-mgp 20138  df-ring 20232  df-cring 20233  df-dvdsr 20357  df-unit 20358  df-rprm 20433  df-idom 20696
This theorem is referenced by:  1arithidom  33565
  Copyright terms: Public domain W3C validator