Metamath Proof Explorer

Theorem 1arithidomlem1

Description: Lemma for 1arithidom . (Contributed by Thierry Arnoux, 30-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 𝐻 ) ) )
Assertion 1arithidomlem1 ( 𝜑 → ∃ 𝑐 ∃ 𝑑 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑐 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑑 ∘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 oveq1 ⊢ ( 𝑙 = ( 𝑁 · 𝑇 ) → ( 𝑙 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) = ( ( 𝑁 · 𝑇 ) · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) )
23 22 eqeq2d ⊢ ( 𝑙 = ( 𝑁 · 𝑇 ) → ( ( 𝑀 Σg 𝐹 ) = ( 𝑙 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) ↔ ( 𝑀 Σg 𝐹 ) = ( ( 𝑁 · 𝑇 ) · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) ) )
24 6 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
25 1 4 unitmulcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ 𝑈 ∧ 𝑇 ∈ 𝑈 ) → ( 𝑁 · 𝑇 ) ∈ 𝑈 )
26 24 20 16 25 syl3anc ⊢ ( 𝜑 → ( 𝑁 · 𝑇 ) ∈ 𝑈 )
27 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
28 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
29 3 27 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 )
30 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
31 3 30 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑀 )
32 id ⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ IDomn )
33 32 idomcringd ⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ CRing )
34 3 crngmgp ⊢ ( 𝑅 ∈ CRing → 𝑀 ∈ CMnd )
35 33 34 syl ⊢ ( 𝑅 ∈ IDomn → 𝑀 ∈ CMnd )
36 6 35 syl ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
37 ovexd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ V )
38 eqidd ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝐹 ) )
39 simpl ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑞 ∈ 𝑃 ) → 𝑅 ∈ IDomn )
40 simpr ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑞 ∈ 𝑃 ) → 𝑞 ∈ 𝑃 )
41 27 2 39 40 rprmcl ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑞 ∈ 𝑃 ) → 𝑞 ∈ ( Base ‘ 𝑅 ) )
42 41 ex ⊢ ( 𝑅 ∈ IDomn → ( 𝑞 ∈ 𝑃 → 𝑞 ∈ ( Base ‘ 𝑅 ) ) )
43 42 ssrdv ⊢ ( 𝑅 ∈ IDomn → 𝑃 ⊆ ( Base ‘ 𝑅 ) )
44 sswrd ⊢ ( 𝑃 ⊆ ( Base ‘ 𝑅 ) → Word 𝑃 ⊆ Word ( Base ‘ 𝑅 ) )
45 6 43 44 3syl ⊢ ( 𝜑 → Word 𝑃 ⊆ Word ( Base ‘ 𝑅 ) )
46 45 7 sseldd ⊢ ( 𝜑 → 𝐹 ∈ Word ( Base ‘ 𝑅 ) )
47 38 46 wrdfd ⊢ ( 𝜑 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ( Base ‘ 𝑅 ) )
48 fvexd ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ V )
49 48 7 wrdfsupp ⊢ ( 𝜑 → 𝐹 finSupp ( 1r ‘ 𝑅 ) )
50 29 31 36 37 47 49 gsumcl ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) ∈ ( Base ‘ 𝑅 ) )
51 27 1 unitcl ⊢ ( 𝑁 ∈ 𝑈 → 𝑁 ∈ ( Base ‘ 𝑅 ) )
52 20 51 syl ⊢ ( 𝜑 → 𝑁 ∈ ( Base ‘ 𝑅 ) )
53 27 1 unitcl ⊢ ( 𝑇 ∈ 𝑈 → 𝑇 ∈ ( Base ‘ 𝑅 ) )
54 16 53 syl ⊢ ( 𝜑 → 𝑇 ∈ ( Base ‘ 𝑅 ) )
55 27 4 24 52 54 ringcld ⊢ ( 𝜑 → ( 𝑁 · 𝑇 ) ∈ ( Base ‘ 𝑅 ) )
56 ovexd ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝐻 ) − 1 ) ) ∈ V )
57 f1of ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
58 iswrdi ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → 𝑆 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
59 18 57 58 3syl ⊢ ( 𝜑 → 𝑆 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
60 eqidd ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ 𝐻 ) )
61 60 12 wrdfd ⊢ ( 𝜑 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ 𝑃 )
62 wrdco ⊢ ( ( 𝑆 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ 𝑃 ) → ( 𝐻 ∘ 𝑆 ) ∈ Word 𝑃 )
63 59 61 62 syl2anc ⊢ ( 𝜑 → ( 𝐻 ∘ 𝑆 ) ∈ Word 𝑃 )
64 elfzo0 ⊢ ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ↔ ( 𝐾 ∈ ℕ0 ∧ ( ♯ ‘ 𝐻 ) ∈ ℕ ∧ 𝐾 < ( ♯ ‘ 𝐻 ) ) )
65 64 simp2bi ⊢ ( 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → ( ♯ ‘ 𝐻 ) ∈ ℕ )
66 nnm1nn0 ⊢ ( ( ♯ ‘ 𝐻 ) ∈ ℕ → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ0 )
67 14 65 66 3syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ0 )
68 lenco ⊢ ( ( 𝑆 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∧ 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ 𝑃 ) → ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) = ( ♯ ‘ 𝑆 ) )
69 59 61 68 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) = ( ♯ ‘ 𝑆 ) )
70 lencl ⊢ ( 𝑆 ∈ Word ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
71 59 70 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
72 69 71 eqeltrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) ∈ ℕ0 )
73 lencl ⊢ ( 𝐻 ∈ Word 𝑃 → ( ♯ ‘ 𝐻 ) ∈ ℕ0 )
74 12 73 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℕ0 )
75 74 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℝ )
76 75 lem1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ≤ ( ♯ ‘ 𝐻 ) )
77 18 57 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
78 ffn ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
79 hashfn ⊢ ( 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) )
80 77 78 79 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) )
81 hashfzo0 ⊢ ( ( ♯ ‘ 𝐻 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) = ( ♯ ‘ 𝐻 ) )
82 12 73 81 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) = ( ♯ ‘ 𝐻 ) )
83 69 80 82 3eqtrrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) )
84 76 83 breqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ≤ ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) )
85 elfz2nn0 ⊢ ( ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) ) ↔ ( ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ0 ∧ ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) ∈ ℕ0 ∧ ( ( ♯ ‘ 𝐻 ) − 1 ) ≤ ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) ) )
86 67 72 84 85 syl3anbrc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) ) )
87 pfxlen ⊢ ( ( ( 𝐻 ∘ 𝑆 ) ∈ Word 𝑃 ∧ ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ ( 𝐻 ∘ 𝑆 ) ) ) ) → ( ♯ ‘ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) = ( ( ♯ ‘ 𝐻 ) − 1 ) )
88 63 86 87 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) = ( ( ♯ ‘ 𝐻 ) − 1 ) )
89 88 eqcomd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) = ( ♯ ‘ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) )
90 pfxcl ⊢ ( ( 𝐻 ∘ 𝑆 ) ∈ Word 𝑃 → ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ∈ Word 𝑃 )
91 63 90 syl ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ∈ Word 𝑃 )
92 45 91 sseldd ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ∈ Word ( Base ‘ 𝑅 ) )
93 89 92 wrdfd ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) : ( 0 ..^ ( ( ♯ ‘ 𝐻 ) − 1 ) ) ⟶ ( Base ‘ 𝑅 ) )
94 32 idomringd ⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ Ring )
95 1 30 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
96 6 94 95 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
97 96 91 wrdfsupp ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) finSupp ( 1r ‘ 𝑅 ) )
98 29 31 36 56 93 97 gsumcl ⊢ ( 𝜑 → ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ∈ ( Base ‘ 𝑅 ) )
99 27 4 24 55 98 ringcld ⊢ ( 𝜑 → ( ( 𝑁 · 𝑇 ) · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
100 27 2 6 10 rprmcl ⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝑅 ) )
101 2 28 6 10 rprmnz ⊢ ( 𝜑 → 𝑄 ≠ ( 0g ‘ 𝑅 ) )
102 100 101 eldifsnd ⊢ ( 𝜑 → 𝑄 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
103 3 ringmgp ⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
104 94 103 syl ⊢ ( 𝑅 ∈ IDomn → 𝑀 ∈ Mnd )
105 6 104 syl ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
106 3 4 mgpplusg ⊢ · = ( +g ‘ 𝑀 )
107 29 106 gsumccatsn ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐹 ∈ Word ( Base ‘ 𝑅 ) ∧ 𝑄 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑀 Σg ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) = ( ( 𝑀 Σg 𝐹 ) · 𝑄 ) )
108 105 46 100 107 syl3anc ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐹 ++ ⟨“ 𝑄 ”⟩ ) ) = ( ( 𝑀 Σg 𝐹 ) · 𝑄 ) )
109 ovexd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ∈ V )
110 45 12 sseldd ⊢ ( 𝜑 → 𝐻 ∈ Word ( Base ‘ 𝑅 ) )
111 60 110 wrdfd ⊢ ( 𝜑 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝑅 ) )
112 48 12 wrdfsupp ⊢ ( 𝜑 → 𝐻 finSupp ( 1r ‘ 𝑅 ) )
113 29 31 36 109 111 112 18 gsumf1o ⊢ ( 𝜑 → ( 𝑀 Σg 𝐻 ) = ( 𝑀 Σg ( 𝐻 ∘ 𝑆 ) ) )
114 113 oveq2d ⊢ ( 𝜑 → ( 𝑁 · ( 𝑀 Σg 𝐻 ) ) = ( 𝑁 · ( 𝑀 Σg ( 𝐻 ∘ 𝑆 ) ) ) )
115 21 108 114 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑀 Σg 𝐹 ) · 𝑄 ) = ( 𝑁 · ( 𝑀 Σg ( 𝐻 ∘ 𝑆 ) ) ) )
116 29 106 cmn12 ⊢ ( ( 𝑀 ∈ CMnd ∧ ( 𝑇 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑄 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑇 · ( ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) · 𝑄 ) ) = ( ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) · ( 𝑇 · 𝑄 ) ) )
117 36 54 98 100 116 syl13anc ⊢ ( 𝜑 → ( 𝑇 · ( ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) · 𝑄 ) ) = ( ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) · ( 𝑇 · 𝑄 ) ) )
118 27 4 24 54 98 100 ringassd ⊢ ( 𝜑 → ( ( 𝑇 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) · 𝑄 ) = ( 𝑇 · ( ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) · 𝑄 ) ) )
119 111 14 ffvelcdmd ⊢ ( 𝜑 → ( 𝐻 ‘ 𝐾 ) ∈ ( Base ‘ 𝑅 ) )
120 29 106 gsumccatsn ⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ∈ Word ( Base ‘ 𝑅 ) ∧ ( 𝐻 ‘ 𝐾 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑀 Σg ( ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ++ ⟨“ ( 𝐻 ‘ 𝐾 ) ”⟩ ) ) = ( ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) · ( 𝐻 ‘ 𝐾 ) ) )
121 105 92 119 120 syl3anc ⊢ ( 𝜑 → ( 𝑀 Σg ( ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ++ ⟨“ ( 𝐻 ‘ 𝐾 ) ”⟩ ) ) = ( ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) · ( 𝐻 ‘ 𝐾 ) ) )
122 19 oveq2d ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐻 ∘ 𝑆 ) ) = ( 𝑀 Σg ( ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ++ ⟨“ ( 𝐻 ‘ 𝐾 ) ”⟩ ) ) )
123 17 oveq2d ⊢ ( 𝜑 → ( ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) · ( 𝑇 · 𝑄 ) ) = ( ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) · ( 𝐻 ‘ 𝐾 ) ) )
124 121 122 123 3eqtr4d ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐻 ∘ 𝑆 ) ) = ( ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) · ( 𝑇 · 𝑄 ) ) )
125 117 118 124 3eqtr4rd ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐻 ∘ 𝑆 ) ) = ( ( 𝑇 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) · 𝑄 ) )
126 125 oveq2d ⊢ ( 𝜑 → ( 𝑁 · ( 𝑀 Σg ( 𝐻 ∘ 𝑆 ) ) ) = ( 𝑁 · ( ( 𝑇 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) · 𝑄 ) ) )
127 27 4 24 52 54 98 ringassd ⊢ ( 𝜑 → ( ( 𝑁 · 𝑇 ) · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) = ( 𝑁 · ( 𝑇 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) ) )
128 127 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 · 𝑇 ) · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) · 𝑄 ) = ( ( 𝑁 · ( 𝑇 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) ) · 𝑄 ) )
129 27 4 24 54 98 ringcld ⊢ ( 𝜑 → ( 𝑇 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
130 27 4 24 52 129 100 ringassd ⊢ ( 𝜑 → ( ( 𝑁 · ( 𝑇 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) ) · 𝑄 ) = ( 𝑁 · ( ( 𝑇 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) · 𝑄 ) ) )
131 128 130 eqtr2d ⊢ ( 𝜑 → ( 𝑁 · ( ( 𝑇 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) · 𝑄 ) ) = ( ( ( 𝑁 · 𝑇 ) · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) · 𝑄 ) )
132 115 126 131 3eqtrd ⊢ ( 𝜑 → ( ( 𝑀 Σg 𝐹 ) · 𝑄 ) = ( ( ( 𝑁 · 𝑇 ) · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) · 𝑄 ) )
133 27 28 4 50 99 102 6 132 idomrcan ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) = ( ( 𝑁 · 𝑇 ) · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) )
134 23 26 133 rspcedvdw ⊢ ( 𝜑 → ∃ 𝑙 ∈ 𝑈 ( 𝑀 Σg 𝐹 ) = ( 𝑙 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) )
135 oveq1 ⊢ ( 𝑘 = 𝑙 → ( 𝑘 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) = ( 𝑙 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) )
136 135 eqeq2d ⊢ ( 𝑘 = 𝑙 → ( ( 𝑀 Σg 𝐹 ) = ( 𝑘 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) ↔ ( 𝑀 Σg 𝐹 ) = ( 𝑙 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) ) )
137 136 cbvrexvw ⊢ ( ∃ 𝑘 ∈ 𝑈 ( 𝑀 Σg 𝐹 ) = ( 𝑘 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) ↔ ∃ 𝑙 ∈ 𝑈 ( 𝑀 Σg 𝐹 ) = ( 𝑙 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) )
138 134 137 sylibr ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑈 ( 𝑀 Σg 𝐹 ) = ( 𝑘 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) )
139 oveq2 ⊢ ( 𝑔 = ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) → ( 𝑀 Σg 𝑔 ) = ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) )
140 139 oveq2d ⊢ ( 𝑔 = ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) → ( 𝑘 · ( 𝑀 Σg 𝑔 ) ) = ( 𝑘 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) )
141 140 eqeq2d ⊢ ( 𝑔 = ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) → ( ( 𝑀 Σg 𝐹 ) = ( 𝑘 · ( 𝑀 Σg 𝑔 ) ) ↔ ( 𝑀 Σg 𝐹 ) = ( 𝑘 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) ) )
142 141 rexbidv ⊢ ( 𝑔 = ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) → ( ∃ 𝑘 ∈ 𝑈 ( 𝑀 Σg 𝐹 ) = ( 𝑘 · ( 𝑀 Σg 𝑔 ) ) ↔ ∃ 𝑘 ∈ 𝑈 ( 𝑀 Σg 𝐹 ) = ( 𝑘 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) ) )
143 eqeq1 ⊢ ( 𝑔 = ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) → ( 𝑔 = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ↔ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) )
144 143 anbi2d ⊢ ( 𝑔 = ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) → ( ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑔 = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ↔ ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ) )
145 144 rexbidv ⊢ ( 𝑔 = ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) → ( ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑔 = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ↔ ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ) )
146 145 exbidv ⊢ ( 𝑔 = ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) → ( ∃ 𝑤 ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑔 = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ) )
147 142 146 imbi12d ⊢ ( 𝑔 = ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) → ( ( ∃ 𝑘 ∈ 𝑈 ( 𝑀 Σg 𝐹 ) = ( 𝑘 · ( 𝑀 Σg 𝑔 ) ) → ∃ 𝑤 ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑔 = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ) ↔ ( ∃ 𝑘 ∈ 𝑈 ( 𝑀 Σg 𝐹 ) = ( 𝑘 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) → ∃ 𝑤 ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ) ) )
148 147 11 91 rspcdva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑈 ( 𝑀 Σg 𝐹 ) = ( 𝑘 · ( 𝑀 Σg ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) ) ) → ∃ 𝑤 ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ) )
149 138 148 mpd ⊢ ( 𝜑 → ∃ 𝑤 ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) )
150 oveq1 ⊢ ( 𝑑 = 𝑢 → ( 𝑑 ∘f · ( 𝐹 ∘ 𝑐 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑐 ) ) )
151 150 eqeq2d ⊢ ( 𝑑 = 𝑢 → ( ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑑 ∘f · ( 𝐹 ∘ 𝑐 ) ) ↔ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑐 ) ) ) )
152 151 anbi2d ⊢ ( 𝑑 = 𝑢 → ( ( 𝑐 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑑 ∘f · ( 𝐹 ∘ 𝑐 ) ) ) ↔ ( 𝑐 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑐 ) ) ) ) )
153 152 cbvrexvw ⊢ ( ∃ 𝑑 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑐 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑑 ∘f · ( 𝐹 ∘ 𝑐 ) ) ) ↔ ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑐 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑐 ) ) ) )
154 f1oeq1 ⊢ ( 𝑐 = 𝑤 → ( 𝑐 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
155 coeq2 ⊢ ( 𝑐 = 𝑤 → ( 𝐹 ∘ 𝑐 ) = ( 𝐹 ∘ 𝑤 ) )
156 155 oveq2d ⊢ ( 𝑐 = 𝑤 → ( 𝑢 ∘f · ( 𝐹 ∘ 𝑐 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) )
157 156 eqeq2d ⊢ ( 𝑐 = 𝑤 → ( ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑐 ) ) ↔ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) )
158 154 157 anbi12d ⊢ ( 𝑐 = 𝑤 → ( ( 𝑐 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑐 ) ) ) ↔ ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ) )
159 158 rexbidv ⊢ ( 𝑐 = 𝑤 → ( ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑐 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑐 ) ) ) ↔ ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ) )
160 153 159 bitrid ⊢ ( 𝑐 = 𝑤 → ( ∃ 𝑑 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑐 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑑 ∘f · ( 𝐹 ∘ 𝑐 ) ) ) ↔ ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) ) )
161 160 cbvexvw ⊢ ( ∃ 𝑐 ∃ 𝑑 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑐 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑑 ∘f · ( 𝐹 ∘ 𝑐 ) ) ) ↔ ∃ 𝑤 ∃ 𝑢 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑢 ∘f · ( 𝐹 ∘ 𝑤 ) ) ) )
162 149 161 sylibr ⊢ ( 𝜑 → ∃ 𝑐 ∃ 𝑑 ∈ ( 𝑈 ↑m ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ( 𝑐 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝐻 ∘ 𝑆 ) prefix ( ( ♯ ‘ 𝐻 ) − 1 ) ) = ( 𝑑 ∘f · ( 𝐹 ∘ 𝑐 ) ) ) )