Metamath Proof Explorer

Theorem 1arithidomlem2

Description: Lemma for 1arithidom : induction step. (Contributed by Thierry Arnoux, 27-May-2025)

Ref Expression
Hypotheses 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 1arithidomlem2 ( 𝜑 → ( ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) : ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) ∧ 𝐻 = ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 1arithidom.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
2 1arithidom.i ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
3 1arithidom.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
4 1arithidom.t ⊢ · = ( .r ‘ 𝑅 )
5 1arithidom.j ⊢ 𝐽 = ( 0 ..^ ( ♯ ‘ 𝐹 ) )
6 1arithidom.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
7 1arithidom.f ⊢ ( 𝜑 → 𝐹 ∈ Word 𝑃 )
8 1arithidom.g ⊢ ( 𝜑 → 𝐺 ∈ Word 𝑃 )
9 1arithidom.1 ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) = ( 𝑀 Σg 𝐺 ) )
10 1arithidomlem.1 ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
11 1arithidomlem.2 ⊢ ( 𝜑 → ∀ 𝑔 ∈ Word 𝑃 ( ∃ 𝑘 ∈ 𝑈 ( 𝑀 Σg 𝐹 ) = ( 𝑘 · ( 𝑀 Σg 𝑔 ) ) → ∃ 𝑤 ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑔 = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ) )
12 1arithidomlem.3 ⊢ ( 𝜑 → 𝐻 ∈ Word 𝑃 )
13 1arithidomlem.4 ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑈 ( 𝑀 Σg ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) = ( 𝑘 · ( 𝑀 Σg 𝐻 ) ) )
14 1arithidomlem.5 ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
15 1arithidomlem.6 ⊢ ( 𝜑 → 𝑄 ( ∥r ‘ 𝑅 ) ( 𝐻 ‘ 𝐾 ) )
16 1arithidomlem.7 ⊢ ( 𝜑 → 𝑇 ∈ 𝑈 )
17 1arithidomlem.8 ⊢ ( 𝜑 → ( 𝑇 · 𝑄 ) = ( 𝐻 ‘ 𝐾 ) )
18 1arithidomlem.9 ⊢ ( 𝜑 → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
19 1arithidomlem.10 ⊢ ( 𝜑 → ( 𝐻 ∘ 𝑆 ) = ( ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ++ ⟨“ ( 𝐻 ‘ 𝐾 ) ”⟩ ) )
20 1arithidomlem.11 ⊢ ( 𝜑 → 𝑁 ∈ 𝑈 )
21 1arithidomlem.12 ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) = ( 𝑁 · ( 𝑀 Σg 𝐻 ) ) )
22 1arithidomlem.13 ⊢ ( 𝜑 → 𝐷 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
23 1arithidomlem.14 ⊢ ( 𝜑 → 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
24 1arithidomlem.15 ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝐷 ∘f · ( 𝐹 ∘ 𝐶 ) ) )
25 ccatws1len ⊢ ( 𝐹 ∈ Word 𝑃 → ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
26 7 25 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
27 24 dmeqd ⊢ ( 𝜑 → dom ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = dom ( 𝐷 ∘f · ( 𝐹 ∘ 𝐶 ) ) )
28 f1of ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
29 iswrdi ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → 𝑆 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
30 18 28 29 3syl ⊢ ( 𝜑 → 𝑆 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
31 eqidd ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ 𝐻 ) )
32 31 12 wrdfd ⊢ ( 𝜑 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ 𝑃 )
33 wrdco ⊢ ( ( 𝑆 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ 𝑃 ) → ( 𝐻 ∘ 𝑆 ) ∈ Word 𝑃 )
34 30 32 33 syl2anc ⊢ ( 𝜑 → ( 𝐻 ∘ 𝑆 ) ∈ Word 𝑃 )
35 elfzo0 ⊢ ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ↔ ( 𝐾 ∈ ℕ0 ∧ ( ♯ ‘ 𝐻 ) ∈ ℕ ∧ 𝐾 < ( ♯ ‘ 𝐻 ) ) )
36 35 simp2bi ⊢ ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → ( ♯ ‘ 𝐻 ) ∈ ℕ )
37 nnm1nn0 ⊢ ( ( ♯ ‘ 𝐻 ) ∈ ℕ → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ0 )
38 14 36 37 3syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ0 )
39 lenco ⊢ ( ( 𝑆 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ 𝑃 ) → ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) = ( ♯ ‘ 𝑆 ) )
40 30 32 39 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) = ( ♯ ‘ 𝑆 ) )
41 lencl ⊢ ( 𝑆 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
42 30 41 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
43 40 42 eqeltrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) ∈ ℕ0 )
44 lencl ⊢ ( 𝐻 ∈ Word 𝑃 → ( ♯ ‘ 𝐻 ) ∈ ℕ0 )
45 12 44 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℕ0 )
46 45 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℝ )
47 46 lem1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ≤ ( ♯ ‘ 𝐻 ) )
48 18 28 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
49 ffn ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
50 hashfn ⊢ ( 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) )
51 48 49 50 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) )
52 hashfzo0 ⊢ ( ( ♯ ‘ 𝐻 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) = ( ♯ ‘ 𝐻 ) )
53 12 44 52 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) = ( ♯ ‘ 𝐻 ) )
54 40 51 53 3eqtrrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) )
55 47 54 breqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ≤ ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) )
56 elfz2nn0 ⊢ ( ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) ) ↔ ( ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ0 ∧ ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) ∈ ℕ0 ∧ ( ( ♯ ‘ 𝐻 ) − 1 ) ≤ ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) ) )
57 38 43 55 56 syl3anbrc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) ) )
58 pfxfn ⊢ ( ( ( 𝐻 ∘ 𝑆 ) ∈ Word 𝑃 ∧ ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) ) ) → ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) Fn ( 0 ..^ ( ( ♯ ‘ 𝐻 ) − 1 ) ) )
59 34 57 58 syl2anc ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) Fn ( 0 ..^ ( ( ♯ ‘ 𝐻 ) − 1 ) ) )
60 59 fndmd ⊢ ( 𝜑 → dom ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐻 ) − 1 ) ) )
61 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
62 6 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
63 62 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑃 ) ) → 𝑅 ∈ Ring )
64 61 1 unitcl ⊢ ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ( Base ‘ 𝑅 ) )
65 64 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑃 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
66 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑃 ) ) → 𝑅 ∈ IDomn )
67 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑃 ) ) → 𝑦 ∈ 𝑃 )
68 61 2 66 67 rprmcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑃 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
69 61 4 63 65 68 ringcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 · 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
70 elmapi ⊢ ( 𝐷 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐷 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑈 )
71 22 70 syl ⊢ ( 𝜑 → 𝐷 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑈 )
72 eqidd ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝐹 ) )
73 72 7 wrdfd ⊢ ( 𝜑 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑃 )
74 f1of ⊢ ( 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
75 23 74 syl ⊢ ( 𝜑 → 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
76 73 75 fcod ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐶 ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑃 )
77 ovexd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ V )
78 inidm ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∩ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) )
79 69 71 76 77 77 78 off ⊢ ( 𝜑 → ( 𝐷 ∘f · ( 𝐹 ∘ 𝐶 ) ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ( Base ‘ 𝑅 ) )
80 79 fdmd ⊢ ( 𝜑 → dom ( 𝐷 ∘f · ( 𝐹 ∘ 𝐶 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
81 27 60 80 3eqtr3d ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
82 lencl ⊢ ( 𝐹 ∈ Word 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
83 7 82 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
84 38 83 fzo0opth ⊢ ( 𝜑 → ( ( 0 ..^ ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ( ♯ ‘ 𝐻 ) − 1 ) = ( ♯ ‘ 𝐹 ) ) )
85 81 84 mpbid ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) = ( ♯ ‘ 𝐹 ) )
86 85 oveq1d ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐻 ) − 1 ) + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
87 14 36 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℕ )
88 87 nncnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℂ )
89 npcan1 ⊢ ( ( ♯ ‘ 𝐻 ) ∈ ℂ → ( ( ( ♯ ‘ 𝐻 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐻 ) )
90 88 89 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐻 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐻 ) )
91 86 90 eqtr3d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐹 ) + 1 ) = ( ♯ ‘ 𝐻 ) )
92 26 91 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) = ( ♯ ‘ 𝐻 ) )
93 92 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
94 eqid ⊢ ( ♯ ‘ 𝐶 ) = ( ♯ ‘ 𝐶 )
95 eqid ⊢ ( 0 ..^ ( ( ♯ ‘ 𝐶 ) + 1 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐶 ) + 1 ) )
96 f1ofn ⊢ ( 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝐶 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
97 hashfn ⊢ ( 𝐶 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐶 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
98 23 96 97 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐶 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
99 hashfzo0 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( ♯ ‘ 𝐹 ) )
100 83 99 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( ♯ ‘ 𝐹 ) )
101 98 100 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐶 ) = ( ♯ ‘ 𝐹 ) )
102 101 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐶 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
103 f1oeq23 ⊢ ( ( ( 0 ..^ ( ♯ ‘ 𝐶 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐶 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ↔ 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
104 103 biimpar ⊢ ( ( ( ( 0 ..^ ( ♯ ‘ 𝐶 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐶 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
105 102 102 23 104 syl21anc ⊢ ( 𝜑 → 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐶 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
106 94 95 105 ccatws1f1o ⊢ ( 𝜑 → ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐶 ) ”⟩ ) : ( 0 ..^ ( ( ♯ ‘ 𝐶 ) + 1 ) ) –1-1-onto→ ( 0 ..^ ( ( ♯ ‘ 𝐶 ) + 1 ) ) )
107 101 s1eqd ⊢ ( 𝜑 → ⟨“ ( ♯ ‘ 𝐶 ) ”⟩ = ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ )
108 107 oveq2d ⊢ ( 𝜑 → ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐶 ) ”⟩ ) = ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) )
109 101 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐶 ) + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
110 109 91 eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐶 ) + 1 ) = ( ♯ ‘ 𝐻 ) )
111 110 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝐶 ) + 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
112 108 111 111 f1oeq123d ⊢ ( 𝜑 → ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐶 ) ”⟩ ) : ( 0 ..^ ( ( ♯ ‘ 𝐶 ) + 1 ) ) –1-1-onto→ ( 0 ..^ ( ( ♯ ‘ 𝐶 ) + 1 ) ) ↔ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) )
113 106 112 mpbid ⊢ ( 𝜑 → ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
114 f1ocnv ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → ◡ 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
115 18 114 syl ⊢ ( 𝜑 → ◡ 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
116 f1oco ⊢ ( ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ ◡ 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
117 113 115 116 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
118 f1oeq23 ⊢ ( ( ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) : ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) ↔ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) )
119 118 biimpar ⊢ ( ( ( ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) ∧ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) : ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) )
120 93 93 117 119 syl21anc ⊢ ( 𝜑 → ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) : ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) )
121 f1ofo ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
122 18 121 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
123 32 ffnd ⊢ ( 𝜑 → 𝐻 Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
124 iswrdi ⊢ ( 𝐷 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑈 → 𝐷 ∈ Word 𝑈 )
125 71 124 syl ⊢ ( 𝜑 → 𝐷 ∈ Word 𝑈 )
126 ccatws1len ⊢ ( 𝐷 ∈ Word 𝑈 → ( ♯ ‘ ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ) = ( ( ♯ ‘ 𝐷 ) + 1 ) )
127 125 126 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ) = ( ( ♯ ‘ 𝐷 ) + 1 ) )
128 elmapfn ⊢ ( 𝐷 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐷 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
129 hashfn ⊢ ( 𝐷 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐷 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
130 22 128 129 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐷 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
131 130 100 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐷 ) = ( ♯ ‘ 𝐹 ) )
132 131 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐷 ) + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
133 127 132 91 3eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ) = ( ♯ ‘ 𝐻 ) )
134 133 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
135 eqidd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ) = ( ♯ ‘ ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ) )
136 ccatws1cl ⊢ ( ( 𝐷 ∈ Word 𝑈 ∧ 𝑇 ∈ 𝑈 ) → ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∈ Word 𝑈 )
137 125 16 136 syl2anc ⊢ ( 𝜑 → ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∈ Word 𝑈 )
138 135 137 wrdfd ⊢ ( 𝜑 → ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) : ( 0 ..^ ( ♯ ‘ ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ) ) ⟶ 𝑈 )
139 134 138 feq2dd ⊢ ( 𝜑 → ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ 𝑈 )
140 139 ffnd ⊢ ( 𝜑 → ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
141 f1of ⊢ ( ◡ 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → ◡ 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
142 18 114 141 3syl ⊢ ( 𝜑 → ◡ 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
143 fnfco ⊢ ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ ◡ 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
144 140 142 143 syl2anc ⊢ ( 𝜑 → ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
145 91 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
146 26 eqcomd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐹 ) + 1 ) = ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) )
147 ccatws1cl ⊢ ( ( 𝐹 ∈ Word 𝑃 ∧ 𝑄 ∈ 𝑃 ) → ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∈ Word 𝑃 )
148 7 10 147 syl2anc ⊢ ( 𝜑 → ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∈ Word 𝑃 )
149 146 148 wrdfd ⊢ ( 𝜑 → ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ 𝑃 )
150 145 149 feq2dd ⊢ ( 𝜑 → ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ 𝑃 )
151 150 ffnd ⊢ ( 𝜑 → ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
152 fzossfzop1 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
153 83 152 syl ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
154 sswrd ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) → Word ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ Word ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
155 153 154 syl ⊢ ( 𝜑 → Word ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ Word ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
156 iswrdi ⊢ ( 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝐶 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
157 75 156 syl ⊢ ( 𝜑 → 𝐶 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
158 155 157 sseldd ⊢ ( 𝜑 → 𝐶 ∈ Word ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
159 ccatws1len ⊢ ( 𝐶 ∈ Word ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) → ( ♯ ‘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐶 ) + 1 ) )
160 158 159 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐶 ) + 1 ) )
161 160 109 91 3eqtrrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) )
162 153 145 sseqtrd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
163 75 162 fssd ⊢ ( 𝜑 → 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
164 iswrdi ⊢ ( 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → 𝐶 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
165 163 164 syl ⊢ ( 𝜑 → 𝐶 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
166 fzonn0p1 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
167 83 166 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
168 167 145 eleqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
169 ccatws1cl ⊢ ( ( 𝐶 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
170 165 168 169 syl2anc ⊢ ( 𝜑 → ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
171 161 170 wrdfd ⊢ ( 𝜑 → ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
172 171 142 fcod ⊢ ( 𝜑 → ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
173 fnfco ⊢ ( ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
174 151 172 173 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
175 ovexd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∈ V )
176 inidm ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∩ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐻 ) )
177 144 174 175 175 176 offn ⊢ ( 𝜑 → ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
178 eqid ⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝐹 )
179 178 7 10 23 ccatws1f1olast ⊢ ( 𝜑 → ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) = ( ( 𝐹 ∘ 𝐶 ) ++ ⟨“ 𝑄 ”⟩ ) )
180 179 oveq2d ⊢ ( 𝜑 → ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) = ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ∘ 𝐶 ) ++ ⟨“ 𝑄 ”⟩ ) ) )
181 16 s1cld ⊢ ( 𝜑 → ⟨“ 𝑇 ”⟩ ∈ Word 𝑈 )
182 iswrdi ⊢ ( ( 𝐹 ∘ 𝐶 ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑃 → ( 𝐹 ∘ 𝐶 ) ∈ Word 𝑃 )
183 76 182 syl ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐶 ) ∈ Word 𝑃 )
184 10 s1cld ⊢ ( 𝜑 → ⟨“ 𝑄 ”⟩ ∈ Word 𝑃 )
185 lenco ⊢ ( ( 𝐶 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑃 ) → ( ♯ ‘ ( 𝐹 ∘ 𝐶 ) ) = ( ♯ ‘ 𝐶 ) )
186 157 73 185 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 ∘ 𝐶 ) ) = ( ♯ ‘ 𝐶 ) )
187 98 186 130 3eqtr4rd ⊢ ( 𝜑 → ( ♯ ‘ 𝐷 ) = ( ♯ ‘ ( 𝐹 ∘ 𝐶 ) ) )
188 s1len ⊢ ( ♯ ‘ ⟨“ 𝑇 ”⟩ ) = 1
189 s1len ⊢ ( ♯ ‘ ⟨“ 𝑄 ”⟩ ) = 1
190 188 189 eqtr4i ⊢ ( ♯ ‘ ⟨“ 𝑇 ”⟩ ) = ( ♯ ‘ ⟨“ 𝑄 ”⟩ )
191 190 a1i ⊢ ( 𝜑 → ( ♯ ‘ ⟨“ 𝑇 ”⟩ ) = ( ♯ ‘ ⟨“ 𝑄 ”⟩ ) )
192 125 181 183 184 187 191 ofccat ⊢ ( 𝜑 → ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ∘ 𝐶 ) ++ ⟨“ 𝑄 ”⟩ ) ) = ( ( 𝐷 ∘f · ( 𝐹 ∘ 𝐶 ) ) ++ ( ⟨“ 𝑇 ”⟩ ∘f · ⟨“ 𝑄 ”⟩ ) ) )
193 180 192 eqtrd ⊢ ( 𝜑 → ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) = ( ( 𝐷 ∘f · ( 𝐹 ∘ 𝐶 ) ) ++ ( ⟨“ 𝑇 ”⟩ ∘f · ⟨“ 𝑄 ”⟩ ) ) )
194 150 171 fcod ⊢ ( 𝜑 → ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ 𝑃 )
195 194 ffnd ⊢ ( 𝜑 → ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
196 140 195 142 175 175 175 176 ofco ⊢ ( 𝜑 → ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) ∘ ◡ 𝑆 ) = ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ∘ ◡ 𝑆 ) ) )
197 196 coeq1d ⊢ ( 𝜑 → ( ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) ∘ ◡ 𝑆 ) ∘ 𝑆 ) = ( ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ∘ ◡ 𝑆 ) ) ∘ 𝑆 ) )
198 coass ⊢ ( ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) ∘ ◡ 𝑆 ) ∘ 𝑆 ) = ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) ∘ ( ◡ 𝑆 ∘ 𝑆 ) )
199 197 198 eqtr3di ⊢ ( 𝜑 → ( ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ∘ ◡ 𝑆 ) ) ∘ 𝑆 ) = ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) ∘ ( ◡ 𝑆 ∘ 𝑆 ) ) )
200 f1of1 ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
201 18 200 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
202 f1cocnv1 ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → ( ◡ 𝑆 ∘ 𝑆 ) = ( I ↾ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) )
203 201 202 syl ⊢ ( 𝜑 → ( ◡ 𝑆 ∘ 𝑆 ) = ( I ↾ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) )
204 203 coeq2d ⊢ ( 𝜑 → ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) ∘ ( ◡ 𝑆 ∘ 𝑆 ) ) = ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) ∘ ( I ↾ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) ) )
205 69 139 194 175 175 176 off ⊢ ( 𝜑 → ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝑅 ) )
206 fcoi1 ⊢ ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝑅 ) → ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) ∘ ( I ↾ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) ) = ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) )
207 205 206 syl ⊢ ( 𝜑 → ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) ∘ ( I ↾ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) ) = ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) )
208 199 204 207 3eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ∘ ◡ 𝑆 ) ) ∘ 𝑆 ) = ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ) )
209 ofs1 ⊢ ( ( 𝑇 ∈ 𝑈 ∧ 𝑄 ∈ 𝑃 ) → ( ⟨“ 𝑇 ”⟩ ∘f · ⟨“ 𝑄 ”⟩ ) = ⟨“ ( 𝑇 · 𝑄 ) ”⟩ )
210 16 10 209 syl2anc ⊢ ( 𝜑 → ( ⟨“ 𝑇 ”⟩ ∘f · ⟨“ 𝑄 ”⟩ ) = ⟨“ ( 𝑇 · 𝑄 ) ”⟩ )
211 17 s1eqd ⊢ ( 𝜑 → ⟨“ ( 𝑇 · 𝑄 ) ”⟩ = ⟨“ ( 𝐻 ‘ 𝐾 ) ”⟩ )
212 210 211 eqtr2d ⊢ ( 𝜑 → ⟨“ ( 𝐻 ‘ 𝐾 ) ”⟩ = ( ⟨“ 𝑇 ”⟩ ∘f · ⟨“ 𝑄 ”⟩ ) )
213 24 212 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ++ ⟨“ ( 𝐻 ‘ 𝐾 ) ”⟩ ) = ( ( 𝐷 ∘f · ( 𝐹 ∘ 𝐶 ) ) ++ ( ⟨“ 𝑇 ”⟩ ∘f · ⟨“ 𝑄 ”⟩ ) ) )
214 193 208 213 3eqtr4rd ⊢ ( 𝜑 → ( ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ++ ⟨“ ( 𝐻 ‘ 𝐾 ) ”⟩ ) = ( ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ∘ ◡ 𝑆 ) ) ∘ 𝑆 ) )
215 coass ⊢ ( ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ∘ ◡ 𝑆 ) = ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) )
216 215 oveq2i ⊢ ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ∘ ◡ 𝑆 ) ) = ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) )
217 216 coeq1i ⊢ ( ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ) ∘ ◡ 𝑆 ) ) ∘ 𝑆 ) = ( ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) ∘ 𝑆 )
218 214 217 eqtrdi ⊢ ( 𝜑 → ( ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ++ ⟨“ ( 𝐻 ‘ 𝐾 ) ”⟩ ) = ( ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) ∘ 𝑆 ) )
219 19 218 eqtrd ⊢ ( 𝜑 → ( 𝐻 ∘ 𝑆 ) = ( ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) ∘ 𝑆 ) )
220 cocan2 ⊢ ( ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ 𝐻 Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( ( 𝐻 ∘ 𝑆 ) = ( ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) ∘ 𝑆 ) ↔ 𝐻 = ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) ) )
221 220 biimpa ⊢ ( ( ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ 𝐻 Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) ∧ ( 𝐻 ∘ 𝑆 ) = ( ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) ∘ 𝑆 ) ) → 𝐻 = ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) )
222 122 123 177 219 221 syl31anc ⊢ ( 𝜑 → 𝐻 = ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) )
223 120 222 jca ⊢ ( 𝜑 → ( ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) : ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) ) ∧ 𝐻 = ( ( ( 𝐷 ++ ⟨“ 𝑇 ”⟩ ) ∘ ◡ 𝑆 ) ∘f · ( ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ∘ ( ( 𝐶 ++ ⟨“ ( ♯ ‘ 𝐹 ) ”⟩ ) ∘ ◡ 𝑆 ) ) ) ) )