Metamath Proof Explorer

Theorem 1arithidomlem1

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

Ref Expression
Hypotheses 1arithidom.u ⊢ U = Unit ⁡ R
1arithidom.i ⊢ P = RPrime ⁡ R
1arithidom.m ⊢ M = mulGrp R
1arithidom.t ⊢ · ˙ = ⋅ R
1arithidom.j ⊢ J = 0 ..^ F
1arithidom.r ⊢ φ → R ∈ IDomn
1arithidom.f ⊢ φ → F ∈ Word P
1arithidom.g ⊢ φ → G ∈ Word P
1arithidom.1 ⊢ φ → ∑ M F = ∑ M G
1arithidomlem.1 ⊢ φ → Q ∈ P
1arithidomlem.2 ⊢ φ → ∀ g ∈ Word P ∃ k ∈ U ∑ M F = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ g = u · ˙ f F ∘ w
1arithidomlem.3 ⊢ φ → H ∈ Word P
1arithidomlem.4 ⊢ φ → ∃ k ∈ U ∑ M F ++ ⟨“ Q ”⟩ = k · ˙ ∑ M H
1arithidomlem.5 ⊢ φ → K ∈ 0 ..^ H
1arithidomlem.6 ⊢ φ → Q ∥ r ⁡ R H ⁡ K
1arithidomlem.7 ⊢ φ → T ∈ U
1arithidomlem.8 ⊢ φ → T · ˙ Q = H ⁡ K
1arithidomlem.9 ⊢ φ → S : 0 ..^ H ⟶ 1-1 onto 0 ..^ H
1arithidomlem.10 ⊢ φ → H ∘ S = H ∘ S prefix H − 1 ++ ⟨“ H ⁡ K ”⟩
1arithidomlem.11 ⊢ φ → N ∈ U
1arithidomlem.12 ⊢ φ → ∑ M F ++ ⟨“ Q ”⟩ = N · ˙ ∑ M H
Assertion 1arithidomlem1 ⊢ φ → ∃ c ∃ d ∈ U 0 ..^ F c : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = d · ˙ f F ∘ c

Proof

Step Hyp Ref Expression
1 1arithidom.u ⊢ U = Unit ⁡ R
2 1arithidom.i ⊢ P = RPrime ⁡ R
3 1arithidom.m ⊢ M = mulGrp R
4 1arithidom.t ⊢ · ˙ = ⋅ R
5 1arithidom.j ⊢ J = 0 ..^ F
6 1arithidom.r ⊢ φ → R ∈ IDomn
7 1arithidom.f ⊢ φ → F ∈ Word P
8 1arithidom.g ⊢ φ → G ∈ Word P
9 1arithidom.1 ⊢ φ → ∑ M F = ∑ M G
10 1arithidomlem.1 ⊢ φ → Q ∈ P
11 1arithidomlem.2 ⊢ φ → ∀ g ∈ Word P ∃ k ∈ U ∑ M F = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ g = u · ˙ f F ∘ w
12 1arithidomlem.3 ⊢ φ → H ∈ Word P
13 1arithidomlem.4 ⊢ φ → ∃ k ∈ U ∑ M F ++ ⟨“ Q ”⟩ = k · ˙ ∑ M H
14 1arithidomlem.5 ⊢ φ → K ∈ 0 ..^ H
15 1arithidomlem.6 ⊢ φ → Q ∥ r ⁡ R H ⁡ K
16 1arithidomlem.7 ⊢ φ → T ∈ U
17 1arithidomlem.8 ⊢ φ → T · ˙ Q = H ⁡ K
18 1arithidomlem.9 ⊢ φ → S : 0 ..^ H ⟶ 1-1 onto 0 ..^ H
19 1arithidomlem.10 ⊢ φ → H ∘ S = H ∘ S prefix H − 1 ++ ⟨“ H ⁡ K ”⟩
20 1arithidomlem.11 ⊢ φ → N ∈ U
21 1arithidomlem.12 ⊢ φ → ∑ M F ++ ⟨“ Q ”⟩ = N · ˙ ∑ M H
22 oveq1 ⊢ l = N · ˙ T → l · ˙ ∑ M H ∘ S prefix H − 1 = N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1
23 22 eqeq2d ⊢ l = N · ˙ T → ∑ M F = l · ˙ ∑ M H ∘ S prefix H − 1 ↔ ∑ M F = N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1
24 6 idomringd ⊢ φ → R ∈ Ring
25 1 4 unitmulcl ⊢ R ∈ Ring ∧ N ∈ U ∧ T ∈ U → N · ˙ T ∈ U
26 24 20 16 25 syl3anc ⊢ φ → N · ˙ T ∈ U
27 eqid ⊢ Base R = Base R
28 eqid ⊢ 0 R = 0 R
29 3 27 mgpbas ⊢ Base R = Base M
30 eqid ⊢ 1 R = 1 R
31 3 30 ringidval ⊢ 1 R = 0 M
32 id ⊢ R ∈ IDomn → R ∈ IDomn
33 32 idomcringd ⊢ R ∈ IDomn → R ∈ CRing
34 3 crngmgp ⊢ R ∈ CRing → M ∈ CMnd
35 33 34 syl ⊢ R ∈ IDomn → M ∈ CMnd
36 6 35 syl ⊢ φ → M ∈ CMnd
37 ovexd ⊢ φ → 0 ..^ F ∈ V
38 eqidd ⊢ φ → F = F
39 simpl ⊢ R ∈ IDomn ∧ q ∈ P → R ∈ IDomn
40 simpr ⊢ R ∈ IDomn ∧ q ∈ P → q ∈ P
41 27 2 39 40 rprmcl ⊢ R ∈ IDomn ∧ q ∈ P → q ∈ Base R
42 41 ex ⊢ R ∈ IDomn → q ∈ P → q ∈ Base R
43 42 ssrdv ⊢ R ∈ IDomn → P ⊆ Base R
44 sswrd ⊢ P ⊆ Base R → Word P ⊆ Word Base R
45 6 43 44 3syl ⊢ φ → Word P ⊆ Word Base R
46 45 7 sseldd ⊢ φ → F ∈ Word Base R
47 38 46 wrdfd ⊢ φ → F : 0 ..^ F ⟶ Base R
48 fvexd ⊢ φ → 1 R ∈ V
49 48 7 wrdfsupp ⊢ φ → finSupp 1 R⁡ F
50 29 31 36 37 47 49 gsumcl ⊢ φ → ∑ M F ∈ Base R
51 27 1 unitcl ⊢ N ∈ U → N ∈ Base R
52 20 51 syl ⊢ φ → N ∈ Base R
53 27 1 unitcl ⊢ T ∈ U → T ∈ Base R
54 16 53 syl ⊢ φ → T ∈ Base R
55 27 4 24 52 54 ringcld ⊢ φ → N · ˙ T ∈ Base R
56 ovexd ⊢ φ → 0 ..^ H − 1 ∈ V
57 f1of ⊢ S : 0 ..^ H ⟶ 1-1 onto 0 ..^ H → S : 0 ..^ H ⟶ 0 ..^ H
58 iswrdi ⊢ S : 0 ..^ H ⟶ 0 ..^ H → S ∈ Word 0 ..^ H
59 18 57 58 3syl ⊢ φ → S ∈ Word 0 ..^ H
60 eqidd ⊢ φ → H = H
61 60 12 wrdfd ⊢ φ → H : 0 ..^ H ⟶ P
62 wrdco ⊢ S ∈ Word 0 ..^ H ∧ H : 0 ..^ H ⟶ P → H ∘ S ∈ Word P
63 59 61 62 syl2anc ⊢ φ → H ∘ S ∈ Word P
64 elfzo0 ⊢ K ∈ 0 ..^ H ↔ K ∈ ℕ 0 ∧ H ∈ ℕ ∧ K < H
65 64 simp2bi ⊢ K ∈ 0 ..^ H → H ∈ ℕ
66 nnm1nn0 ⊢ H ∈ ℕ → H − 1 ∈ ℕ 0
67 14 65 66 3syl ⊢ φ → H − 1 ∈ ℕ 0
68 lenco ⊢ S ∈ Word 0 ..^ H ∧ H : 0 ..^ H ⟶ P → H ∘ S = S
69 59 61 68 syl2anc ⊢ φ → H ∘ S = S
70 lencl ⊢ S ∈ Word 0 ..^ H → S ∈ ℕ 0
71 59 70 syl ⊢ φ → S ∈ ℕ 0
72 69 71 eqeltrd ⊢ φ → H ∘ S ∈ ℕ 0
73 lencl ⊢ H ∈ Word P → H ∈ ℕ 0
74 12 73 syl ⊢ φ → H ∈ ℕ 0
75 74 nn0red ⊢ φ → H ∈ ℝ
76 75 lem1d ⊢ φ → H − 1 ≤ H
77 18 57 syl ⊢ φ → S : 0 ..^ H ⟶ 0 ..^ H
78 ffn ⊢ S : 0 ..^ H ⟶ 0 ..^ H → S Fn 0 ..^ H
79 hashfn ⊢ S Fn 0 ..^ H → S = 0 ..^ H
80 77 78 79 3syl ⊢ φ → S = 0 ..^ H
81 hashfzo0 ⊢ H ∈ ℕ 0 → 0 ..^ H = H
82 12 73 81 3syl ⊢ φ → 0 ..^ H = H
83 69 80 82 3eqtrrd ⊢ φ → H = H ∘ S
84 76 83 breqtrd ⊢ φ → H − 1 ≤ H ∘ S
85 elfz2nn0 ⊢ H − 1 ∈ 0 … H ∘ S ↔ H − 1 ∈ ℕ 0 ∧ H ∘ S ∈ ℕ 0 ∧ H − 1 ≤ H ∘ S
86 67 72 84 85 syl3anbrc ⊢ φ → H − 1 ∈ 0 … H ∘ S
87 pfxlen ⊢ H ∘ S ∈ Word P ∧ H − 1 ∈ 0 … H ∘ S → H ∘ S prefix H − 1 = H − 1
88 63 86 87 syl2anc ⊢ φ → H ∘ S prefix H − 1 = H − 1
89 88 eqcomd ⊢ φ → H − 1 = H ∘ S prefix H − 1
90 pfxcl ⊢ H ∘ S ∈ Word P → H ∘ S prefix H − 1 ∈ Word P
91 63 90 syl ⊢ φ → H ∘ S prefix H − 1 ∈ Word P
92 45 91 sseldd ⊢ φ → H ∘ S prefix H − 1 ∈ Word Base R
93 89 92 wrdfd ⊢ φ → H ∘ S prefix H − 1 : 0 ..^ H − 1 ⟶ Base R
94 32 idomringd ⊢ R ∈ IDomn → R ∈ Ring
95 1 30 1unit ⊢ R ∈ Ring → 1 R ∈ U
96 6 94 95 3syl ⊢ φ → 1 R ∈ U
97 96 91 wrdfsupp ⊢ φ → finSupp 1 R⁡ H ∘ S prefix H − 1
98 29 31 36 56 93 97 gsumcl ⊢ φ → ∑ M H ∘ S prefix H − 1 ∈ Base R
99 27 4 24 55 98 ringcld ⊢ φ → N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1 ∈ Base R
100 27 2 6 10 rprmcl ⊢ φ → Q ∈ Base R
101 2 28 6 10 rprmnz ⊢ φ → Q ≠ 0 R
102 100 101 eldifsnd ⊢ φ → Q ∈ Base R ∖ 0 R
103 3 ringmgp ⊢ R ∈ Ring → M ∈ Mnd
104 94 103 syl ⊢ R ∈ IDomn → M ∈ Mnd
105 6 104 syl ⊢ φ → M ∈ Mnd
106 3 4 mgpplusg ⊢ · ˙ = + M
107 29 106 gsumccatsn ⊢ M ∈ Mnd ∧ F ∈ Word Base R ∧ Q ∈ Base R → ∑ M F ++ ⟨“ Q ”⟩ = ∑ M F · ˙ Q
108 105 46 100 107 syl3anc ⊢ φ → ∑ M F ++ ⟨“ Q ”⟩ = ∑ M F · ˙ Q
109 ovexd ⊢ φ → 0 ..^ H ∈ V
110 45 12 sseldd ⊢ φ → H ∈ Word Base R
111 60 110 wrdfd ⊢ φ → H : 0 ..^ H ⟶ Base R
112 48 12 wrdfsupp ⊢ φ → finSupp 1 R⁡ H
113 29 31 36 109 111 112 18 gsumf1o ⊢ φ → ∑ M H = ∑ M H ∘ S
114 113 oveq2d ⊢ φ → N · ˙ ∑ M H = N · ˙ ∑ M H ∘ S
115 21 108 114 3eqtr3d ⊢ φ → ∑ M F · ˙ Q = N · ˙ ∑ M H ∘ S
116 29 106 cmn12 ⊢ M ∈ CMnd ∧ T ∈ Base R ∧ ∑ M H ∘ S prefix H − 1 ∈ Base R ∧ Q ∈ Base R → T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q = ∑ M H ∘ S prefix H − 1 · ˙ T · ˙ Q
117 36 54 98 100 116 syl13anc ⊢ φ → T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q = ∑ M H ∘ S prefix H − 1 · ˙ T · ˙ Q
118 27 4 24 54 98 100 ringassd ⊢ φ → T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q = T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q
119 111 14 ffvelcdmd ⊢ φ → H ⁡ K ∈ Base R
120 29 106 gsumccatsn ⊢ M ∈ Mnd ∧ H ∘ S prefix H − 1 ∈ Word Base R ∧ H ⁡ K ∈ Base R → ∑ M H ∘ S prefix H − 1 ++ ⟨“ H ⁡ K ”⟩ = ∑ M H ∘ S prefix H − 1 · ˙ H ⁡ K
121 105 92 119 120 syl3anc ⊢ φ → ∑ M H ∘ S prefix H − 1 ++ ⟨“ H ⁡ K ”⟩ = ∑ M H ∘ S prefix H − 1 · ˙ H ⁡ K
122 19 oveq2d ⊢ φ → ∑ M H ∘ S = ∑ M H ∘ S prefix H − 1 ++ ⟨“ H ⁡ K ”⟩
123 17 oveq2d ⊢ φ → ∑ M H ∘ S prefix H − 1 · ˙ T · ˙ Q = ∑ M H ∘ S prefix H − 1 · ˙ H ⁡ K
124 121 122 123 3eqtr4d ⊢ φ → ∑ M H ∘ S = ∑ M H ∘ S prefix H − 1 · ˙ T · ˙ Q
125 117 118 124 3eqtr4rd ⊢ φ → ∑ M H ∘ S = T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q
126 125 oveq2d ⊢ φ → N · ˙ ∑ M H ∘ S = N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q
127 27 4 24 52 54 98 ringassd ⊢ φ → N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1 = N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1
128 127 oveq1d ⊢ φ → N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q = N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q
129 27 4 24 54 98 ringcld ⊢ φ → T · ˙ ∑ M H ∘ S prefix H − 1 ∈ Base R
130 27 4 24 52 129 100 ringassd ⊢ φ → N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q = N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q
131 128 130 eqtr2d ⊢ φ → N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q = N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q
132 115 126 131 3eqtrd ⊢ φ → ∑ M F · ˙ Q = N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1 · ˙ Q
133 27 28 4 50 99 102 6 132 idomrcan ⊢ φ → ∑ M F = N · ˙ T · ˙ ∑ M H ∘ S prefix H − 1
134 23 26 133 rspcedvdw ⊢ φ → ∃ l ∈ U ∑ M F = l · ˙ ∑ M H ∘ S prefix H − 1
135 oveq1 ⊢ k = l → k · ˙ ∑ M H ∘ S prefix H − 1 = l · ˙ ∑ M H ∘ S prefix H − 1
136 135 eqeq2d ⊢ k = l → ∑ M F = k · ˙ ∑ M H ∘ S prefix H − 1 ↔ ∑ M F = l · ˙ ∑ M H ∘ S prefix H − 1
137 136 cbvrexvw ⊢ ∃ k ∈ U ∑ M F = k · ˙ ∑ M H ∘ S prefix H − 1 ↔ ∃ l ∈ U ∑ M F = l · ˙ ∑ M H ∘ S prefix H − 1
138 134 137 sylibr ⊢ φ → ∃ k ∈ U ∑ M F = k · ˙ ∑ M H ∘ S prefix H − 1
139 oveq2 ⊢ g = H ∘ S prefix H − 1 → ∑ M g = ∑ M H ∘ S prefix H − 1
140 139 oveq2d ⊢ g = H ∘ S prefix H − 1 → k · ˙ ∑ M g = k · ˙ ∑ M H ∘ S prefix H − 1
141 140 eqeq2d ⊢ g = H ∘ S prefix H − 1 → ∑ M F = k · ˙ ∑ M g ↔ ∑ M F = k · ˙ ∑ M H ∘ S prefix H − 1
142 141 rexbidv ⊢ g = H ∘ S prefix H − 1 → ∃ k ∈ U ∑ M F = k · ˙ ∑ M g ↔ ∃ k ∈ U ∑ M F = k · ˙ ∑ M H ∘ S prefix H − 1
143 eqeq1 ⊢ g = H ∘ S prefix H − 1 → g = u · ˙ f F ∘ w ↔ H ∘ S prefix H − 1 = u · ˙ f F ∘ w
144 143 anbi2d ⊢ g = H ∘ S prefix H − 1 → w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ g = u · ˙ f F ∘ w ↔ w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ w
145 144 rexbidv ⊢ g = H ∘ S prefix H − 1 → ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ g = u · ˙ f F ∘ w ↔ ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ w
146 145 exbidv ⊢ g = H ∘ S prefix H − 1 → ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ g = u · ˙ f F ∘ w ↔ ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ w
147 142 146 imbi12d ⊢ g = H ∘ S prefix H − 1 → ∃ k ∈ U ∑ M F = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ g = u · ˙ f F ∘ w ↔ ∃ k ∈ U ∑ M F = k · ˙ ∑ M H ∘ S prefix H − 1 → ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ w
148 147 11 91 rspcdva ⊢ φ → ∃ k ∈ U ∑ M F = k · ˙ ∑ M H ∘ S prefix H − 1 → ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ w
149 138 148 mpd ⊢ φ → ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ w
150 oveq1 ⊢ d = u → d · ˙ f F ∘ c = u · ˙ f F ∘ c
151 150 eqeq2d ⊢ d = u → H ∘ S prefix H − 1 = d · ˙ f F ∘ c ↔ H ∘ S prefix H − 1 = u · ˙ f F ∘ c
152 151 anbi2d ⊢ d = u → c : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = d · ˙ f F ∘ c ↔ c : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ c
153 152 cbvrexvw ⊢ ∃ d ∈ U 0 ..^ F c : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = d · ˙ f F ∘ c ↔ ∃ u ∈ U 0 ..^ F c : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ c
154 f1oeq1 ⊢ c = w → c : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ↔ w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F
155 coeq2 ⊢ c = w → F ∘ c = F ∘ w
156 155 oveq2d ⊢ c = w → u · ˙ f F ∘ c = u · ˙ f F ∘ w
157 156 eqeq2d ⊢ c = w → H ∘ S prefix H − 1 = u · ˙ f F ∘ c ↔ H ∘ S prefix H − 1 = u · ˙ f F ∘ w
158 154 157 anbi12d ⊢ c = w → c : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ c ↔ w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ w
159 158 rexbidv ⊢ c = w → ∃ u ∈ U 0 ..^ F c : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ c ↔ ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ w
160 153 159 bitrid ⊢ c = w → ∃ d ∈ U 0 ..^ F c : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = d · ˙ f F ∘ c ↔ ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ w
161 160 cbvexvw ⊢ ∃ c ∃ d ∈ U 0 ..^ F c : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = d · ˙ f F ∘ c ↔ ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = u · ˙ f F ∘ w
162 149 161 sylibr ⊢ φ → ∃ c ∃ d ∈ U 0 ..^ F c : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ H ∘ S prefix H − 1 = d · ˙ f F ∘ c