Metamath Proof Explorer


Theorem 1arithidom

Description: Uniqueness of prime factorizations in an integral domain R . Given two equal products F and G of prime elements, F and G are equal up to a renumbering w and a multiplication by units u . See also 1arith . Chapter VII, Paragraph 3, Section 3, Proposition 2 of BourbakiCAlg2, p. 228. (Contributed by Thierry Arnoux, 27-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
Assertion 1arithidom ⊢ φ → ∃ w ∃ u ∈ U J w : J ⟶ 1-1 onto J ∧ G = u · ˙ f F ∘ w

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 6 idomringd ⊢ φ → R ∈ Ring
11 eqid ⊢ 1 R = 1 R
12 1 11 1unit ⊢ R ∈ Ring → 1 R ∈ U
13 10 12 syl ⊢ φ → 1 R ∈ U
14 oveq1 ⊢ k = 1 R → k · ˙ ∑ M G = 1 R · ˙ ∑ M G
15 14 adantl ⊢ φ ∧ k = 1 R → k · ˙ ∑ M G = 1 R · ˙ ∑ M G
16 eqid ⊢ Base R = Base R
17 10 adantr ⊢ φ ∧ k = 1 R → R ∈ Ring
18 3 16 mgpbas ⊢ Base R = Base M
19 3 11 ringidval ⊢ 1 R = 0 M
20 id ⊢ R ∈ IDomn → R ∈ IDomn
21 20 idomcringd ⊢ R ∈ IDomn → R ∈ CRing
22 3 crngmgp ⊢ R ∈ CRing → M ∈ CMnd
23 21 22 syl ⊢ R ∈ IDomn → M ∈ CMnd
24 6 23 syl ⊢ φ → M ∈ CMnd
25 ovexd ⊢ φ → 0 ..^ G ∈ V
26 eqidd ⊢ φ → G = G
27 26 8 wrdfd ⊢ φ → G : 0 ..^ G ⟶ P
28 6 adantr ⊢ φ ∧ p ∈ P → R ∈ IDomn
29 simpr ⊢ φ ∧ p ∈ P → p ∈ P
30 16 2 28 29 rprmcl ⊢ φ ∧ p ∈ P → p ∈ Base R
31 30 ex ⊢ φ → p ∈ P → p ∈ Base R
32 31 ssrdv ⊢ φ → P ⊆ Base R
33 27 32 fssd ⊢ φ → G : 0 ..^ G ⟶ Base R
34 13 8 wrdfsupp ⊢ φ → finSupp 1 R⁡ G
35 18 19 24 25 33 34 gsumcl ⊢ φ → ∑ M G ∈ Base R
36 35 adantr ⊢ φ ∧ k = 1 R → ∑ M G ∈ Base R
37 16 4 11 17 36 ringlidmd ⊢ φ ∧ k = 1 R → 1 R · ˙ ∑ M G = ∑ M G
38 15 37 eqtrd ⊢ φ ∧ k = 1 R → k · ˙ ∑ M G = ∑ M G
39 38 eqeq2d ⊢ φ ∧ k = 1 R → ∑ M F = k · ˙ ∑ M G ↔ ∑ M F = ∑ M G
40 13 39 9 rspcedvd ⊢ φ → ∃ k ∈ U ∑ M F = k · ˙ ∑ M G
41 oveq2 ⊢ g = G → ∑ M g = ∑ M G
42 41 oveq2d ⊢ g = G → k · ˙ ∑ M g = k · ˙ ∑ M G
43 42 eqeq2d ⊢ g = G → ∑ M F = k · ˙ ∑ M g ↔ ∑ M F = k · ˙ ∑ M G
44 43 rexbidv ⊢ g = G → ∃ k ∈ U ∑ M F = k · ˙ ∑ M g ↔ ∃ k ∈ U ∑ M F = k · ˙ ∑ M G
45 eqeq1 ⊢ g = G → g = u · ˙ f F ∘ w ↔ G = u · ˙ f F ∘ w
46 45 anbi2d ⊢ g = G → w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ g = u · ˙ f F ∘ w ↔ w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ G = u · ˙ f F ∘ w
47 46 rexbidv ⊢ g = G → ∃ 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 ∧ G = u · ˙ f F ∘ w
48 47 exbidv ⊢ g = G → ∃ 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 ∧ G = u · ˙ f F ∘ w
49 44 48 imbi12d ⊢ g = G → ∃ 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 G → ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ G = u · ˙ f F ∘ w
50 oveq2 ⊢ h = ∅ → ∑ M h = ∑ M ∅
51 50 eqeq1d ⊢ h = ∅ → ∑ M h = k · ˙ ∑ M g ↔ ∑ M ∅ = k · ˙ ∑ M g
52 51 rexbidv ⊢ h = ∅ → ∃ k ∈ U ∑ M h = k · ˙ ∑ M g ↔ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g
53 fveq2 ⊢ h = ∅ → h = ∅
54 53 oveq2d ⊢ h = ∅ → 0 ..^ h = 0 ..^ ∅
55 54 oveq2d ⊢ h = ∅ → U 0 ..^ h = U 0 ..^ ∅
56 eqidd ⊢ h = ∅ → w = w
57 56 54 54 f1oeq123d ⊢ h = ∅ → w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ↔ w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅
58 coeq1 ⊢ h = ∅ → h ∘ w = ∅ ∘ w
59 58 oveq2d ⊢ h = ∅ → u · ˙ f h ∘ w = u · ˙ f ∅ ∘ w
60 59 eqeq2d ⊢ h = ∅ → g = u · ˙ f h ∘ w ↔ g = u · ˙ f ∅ ∘ w
61 57 60 anbi12d ⊢ h = ∅ → w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅ ∧ g = u · ˙ f ∅ ∘ w
62 55 61 rexeqbidv ⊢ h = ∅ → ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∃ u ∈ U 0 ..^ ∅ w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅ ∧ g = u · ˙ f ∅ ∘ w
63 62 exbidv ⊢ h = ∅ → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∃ w ∃ u ∈ U 0 ..^ ∅ w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅ ∧ g = u · ˙ f ∅ ∘ w
64 52 63 imbi12d ⊢ h = ∅ → ∃ k ∈ U ∑ M h = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ ∅ w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅ ∧ g = u · ˙ f ∅ ∘ w
65 64 ralbidv ⊢ h = ∅ → ∀ g ∈ Word P ∃ k ∈ U ∑ M h = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∀ g ∈ Word P ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ ∅ w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅ ∧ g = u · ˙ f ∅ ∘ w
66 65 imbi2d ⊢ h = ∅ → R ∈ IDomn → ∀ g ∈ Word P ∃ k ∈ U ∑ M h = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ R ∈ IDomn → ∀ g ∈ Word P ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ ∅ w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅ ∧ g = u · ˙ f ∅ ∘ w
67 oveq2 ⊢ h = f → ∑ M h = ∑ M f
68 67 eqeq1d ⊢ h = f → ∑ M h = k · ˙ ∑ M g ↔ ∑ M f = k · ˙ ∑ M g
69 68 rexbidv ⊢ h = f → ∃ k ∈ U ∑ M h = k · ˙ ∑ M g ↔ ∃ k ∈ U ∑ M f = k · ˙ ∑ M g
70 fveq2 ⊢ h = f → h = f
71 70 oveq2d ⊢ h = f → 0 ..^ h = 0 ..^ f
72 71 oveq2d ⊢ h = f → U 0 ..^ h = U 0 ..^ f
73 eqidd ⊢ h = f → w = w
74 73 71 71 f1oeq123d ⊢ h = f → w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ↔ w : 0 ..^ f ⟶ 1-1 onto 0 ..^ f
75 coeq1 ⊢ h = f → h ∘ w = f ∘ w
76 75 oveq2d ⊢ h = f → u · ˙ f h ∘ w = u · ˙ f f ∘ w
77 76 eqeq2d ⊢ h = f → g = u · ˙ f h ∘ w ↔ g = u · ˙ f f ∘ w
78 74 77 anbi12d ⊢ h = f → w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ w : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ g = u · ˙ f f ∘ w
79 72 78 rexeqbidv ⊢ h = f → ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∃ u ∈ U 0 ..^ f w : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ g = u · ˙ f f ∘ w
80 79 exbidv ⊢ h = f → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∃ w ∃ u ∈ U 0 ..^ f w : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ g = u · ˙ f f ∘ w
81 69 80 imbi12d ⊢ h = f → ∃ k ∈ U ∑ M h = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∃ 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
82 81 ralbidv ⊢ h = f → ∀ g ∈ Word P ∃ k ∈ U ∑ M h = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∀ 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
83 82 imbi2d ⊢ h = f → R ∈ IDomn → ∀ g ∈ Word P ∃ k ∈ U ∑ M h = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ R ∈ IDomn → ∀ 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
84 oveq2 ⊢ h = f ++ ⟨“ p ”⟩ → ∑ M h = ∑ M f ++ ⟨“ p ”⟩
85 84 eqeq1d ⊢ h = f ++ ⟨“ p ”⟩ → ∑ M h = k · ˙ ∑ M g ↔ ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g
86 85 rexbidv ⊢ h = f ++ ⟨“ p ”⟩ → ∃ k ∈ U ∑ M h = k · ˙ ∑ M g ↔ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g
87 fveq2 ⊢ h = f ++ ⟨“ p ”⟩ → h = f ++ ⟨“ p ”⟩
88 87 oveq2d ⊢ h = f ++ ⟨“ p ”⟩ → 0 ..^ h = 0 ..^ f ++ ⟨“ p ”⟩
89 88 oveq2d ⊢ h = f ++ ⟨“ p ”⟩ → U 0 ..^ h = U 0 ..^ f ++ ⟨“ p ”⟩
90 eqidd ⊢ h = f ++ ⟨“ p ”⟩ → w = w
91 90 88 88 f1oeq123d ⊢ h = f ++ ⟨“ p ”⟩ → w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ↔ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩
92 coeq1 ⊢ h = f ++ ⟨“ p ”⟩ → h ∘ w = f ++ ⟨“ p ”⟩ ∘ w
93 92 oveq2d ⊢ h = f ++ ⟨“ p ”⟩ → u · ˙ f h ∘ w = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w
94 93 eqeq2d ⊢ h = f ++ ⟨“ p ”⟩ → g = u · ˙ f h ∘ w ↔ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w
95 91 94 anbi12d ⊢ h = f ++ ⟨“ p ”⟩ → w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w
96 89 95 rexeqbidv ⊢ h = f ++ ⟨“ p ”⟩ → ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w
97 96 exbidv ⊢ h = f ++ ⟨“ p ”⟩ → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∃ w ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w
98 86 97 imbi12d ⊢ h = f ++ ⟨“ p ”⟩ → ∃ k ∈ U ∑ M h = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w
99 98 ralbidv ⊢ h = f ++ ⟨“ p ”⟩ → ∀ g ∈ Word P ∃ k ∈ U ∑ M h = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∀ g ∈ Word P ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w
100 99 imbi2d ⊢ h = f ++ ⟨“ p ”⟩ → R ∈ IDomn → ∀ g ∈ Word P ∃ k ∈ U ∑ M h = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ R ∈ IDomn → ∀ g ∈ Word P ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w
101 oveq2 ⊢ h = F → ∑ M h = ∑ M F
102 101 eqeq1d ⊢ h = F → ∑ M h = k · ˙ ∑ M g ↔ ∑ M F = k · ˙ ∑ M g
103 102 rexbidv ⊢ h = F → ∃ k ∈ U ∑ M h = k · ˙ ∑ M g ↔ ∃ k ∈ U ∑ M F = k · ˙ ∑ M g
104 fveq2 ⊢ h = F → h = F
105 104 oveq2d ⊢ h = F → 0 ..^ h = 0 ..^ F
106 105 oveq2d ⊢ h = F → U 0 ..^ h = U 0 ..^ F
107 eqidd ⊢ h = F → w = w
108 107 105 105 f1oeq123d ⊢ h = F → w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ↔ w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F
109 coeq1 ⊢ h = F → h ∘ w = F ∘ w
110 109 oveq2d ⊢ h = F → u · ˙ f h ∘ w = u · ˙ f F ∘ w
111 110 eqeq2d ⊢ h = F → g = u · ˙ f h ∘ w ↔ g = u · ˙ f F ∘ w
112 108 111 anbi12d ⊢ h = F → w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ g = u · ˙ f F ∘ w
113 106 112 rexeqbidv ⊢ h = F → ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ g = u · ˙ f F ∘ w
114 113 exbidv ⊢ h = F → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ g = u · ˙ f F ∘ w
115 103 114 imbi12d ⊢ h = F → ∃ k ∈ U ∑ M h = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∃ 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
116 115 ralbidv ⊢ h = F → ∀ g ∈ Word P ∃ k ∈ U ∑ M h = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ ∀ 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
117 116 imbi2d ⊢ h = F → R ∈ IDomn → ∀ g ∈ Word P ∃ k ∈ U ∑ M h = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ h w : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ g = u · ˙ f h ∘ w ↔ R ∈ IDomn → ∀ 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
118 0ex ⊢ ∅ ∈ V
119 118 a1i ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ∅ ∈ V
120 118 snid ⊢ ∅ ∈ ∅
121 1 fvexi ⊢ U ∈ V
122 mapdm0 ⊢ U ∈ V → U ∅ = ∅
123 121 122 ax-mp ⊢ U ∅ = ∅
124 120 123 eleqtrri ⊢ ∅ ∈ U ∅
125 124 a1i ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ∅ ∈ U ∅
126 f1o0 ⊢ ∅ : ∅ ⟶ 1-1 onto ∅
127 126 biantrur ⊢ g = u · ˙ f ∅ ∘ ∅ ↔ ∅ : ∅ ⟶ 1-1 onto ∅ ∧ g = u · ˙ f ∅ ∘ ∅
128 co02 ⊢ ∅ ∘ ∅ = ∅
129 128 oveq2i ⊢ u · ˙ f ∅ ∘ ∅ = u · ˙ f ∅
130 of0r ⊢ u · ˙ f ∅ = ∅
131 129 130 eqtri ⊢ u · ˙ f ∅ ∘ ∅ = ∅
132 131 eqeq2i ⊢ g = u · ˙ f ∅ ∘ ∅ ↔ g = ∅
133 127 132 bitr3i ⊢ ∅ : ∅ ⟶ 1-1 onto ∅ ∧ g = u · ˙ f ∅ ∘ ∅ ↔ g = ∅
134 133 a1i ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ u = ∅ → ∅ : ∅ ⟶ 1-1 onto ∅ ∧ g = u · ˙ f ∅ ∘ ∅ ↔ g = ∅
135 simpl ⊢ R ∈ IDomn ∧ g ∈ Word P → R ∈ IDomn
136 135 idomcringd ⊢ R ∈ IDomn ∧ g ∈ Word P → R ∈ CRing
137 136 ad2antrr ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → R ∈ CRing
138 simplr ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → k ∈ U
139 16 1 unitcl ⊢ k ∈ U → k ∈ Base R
140 138 139 syl ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → k ∈ Base R
141 137 22 syl ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → M ∈ CMnd
142 ovexd ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → 0 ..^ g ∈ V
143 eqidd ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → g = g
144 simpl ⊢ R ∈ IDomn ∧ p ∈ P → R ∈ IDomn
145 simpr ⊢ R ∈ IDomn ∧ p ∈ P → p ∈ P
146 16 2 144 145 rprmcl ⊢ R ∈ IDomn ∧ p ∈ P → p ∈ Base R
147 146 ex ⊢ R ∈ IDomn → p ∈ P → p ∈ Base R
148 147 ssrdv ⊢ R ∈ IDomn → P ⊆ Base R
149 sswrd ⊢ P ⊆ Base R → Word P ⊆ Word Base R
150 148 149 syl ⊢ R ∈ IDomn → Word P ⊆ Word Base R
151 150 sselda ⊢ R ∈ IDomn ∧ g ∈ Word P → g ∈ Word Base R
152 151 ad2antrr ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → g ∈ Word Base R
153 143 152 wrdfd ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → g : 0 ..^ g ⟶ Base R
154 135 idomringd ⊢ R ∈ IDomn ∧ g ∈ Word P → R ∈ Ring
155 154 12 syl ⊢ R ∈ IDomn ∧ g ∈ Word P → 1 R ∈ U
156 155 ad2antrr ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → 1 R ∈ U
157 156 152 wrdfsupp ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → finSupp 1 R⁡ g
158 18 19 141 142 153 157 gsumcl ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → ∑ M g ∈ Base R
159 simpr ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → ∑ M ∅ = k · ˙ ∑ M g
160 19 gsum0 ⊢ ∑ M ∅ = 1 R
161 160 156 eqeltrid ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → ∑ M ∅ ∈ U
162 159 161 eqeltrrd ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → k · ˙ ∑ M g ∈ U
163 1 4 16 unitmulclb ⊢ R ∈ CRing ∧ k ∈ Base R ∧ ∑ M g ∈ Base R → k · ˙ ∑ M g ∈ U ↔ k ∈ U ∧ ∑ M g ∈ U
164 163 biimpa ⊢ R ∈ CRing ∧ k ∈ Base R ∧ ∑ M g ∈ Base R ∧ k · ˙ ∑ M g ∈ U → k ∈ U ∧ ∑ M g ∈ U
165 137 140 158 162 164 syl31anc ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → k ∈ U ∧ ∑ M g ∈ U
166 165 simprd ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ k ∈ U ∧ ∑ M ∅ = k · ˙ ∑ M g → ∑ M g ∈ U
167 166 r19.29an ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ∑ M g ∈ U
168 16 1 3 136 151 unitprodclb ⊢ R ∈ IDomn ∧ g ∈ Word P → ∑ M g ∈ U ↔ ran ⁡ g ⊆ U
169 168 adantr ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ∑ M g ∈ U ↔ ran ⁡ g ⊆ U
170 167 169 mpbid ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ran ⁡ g ⊆ U
171 170 adantr ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ g ≠ ∅ → ran ⁡ g ⊆ U
172 eqidd ⊢ R ∈ IDomn ∧ g ∈ Word P → g = g
173 simpr ⊢ R ∈ IDomn ∧ g ∈ Word P → g ∈ Word P
174 172 173 wrdfd ⊢ R ∈ IDomn ∧ g ∈ Word P → g : 0 ..^ g ⟶ P
175 174 freld ⊢ R ∈ IDomn ∧ g ∈ Word P → Rel ⁡ g
176 175 ad2antrr ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ g ≠ ∅ → Rel ⁡ g
177 simpr ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ g ≠ ∅ → g ≠ ∅
178 relrn0 ⊢ Rel ⁡ g → g = ∅ ↔ ran ⁡ g = ∅
179 178 necon3bid ⊢ Rel ⁡ g → g ≠ ∅ ↔ ran ⁡ g ≠ ∅
180 179 biimpa ⊢ Rel ⁡ g ∧ g ≠ ∅ → ran ⁡ g ≠ ∅
181 176 177 180 syl2anc ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ g ≠ ∅ → ran ⁡ g ≠ ∅
182 n0 ⊢ ran ⁡ g ≠ ∅ ↔ ∃ i i ∈ ran ⁡ g
183 181 182 sylib ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ g ≠ ∅ → ∃ i i ∈ ran ⁡ g
184 simpr ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ g ≠ ∅ ∧ i ∈ ran ⁡ g → i ∈ ran ⁡ g
185 135 ad3antrrr ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ g ≠ ∅ ∧ i ∈ ran ⁡ g → R ∈ IDomn
186 174 frnd ⊢ R ∈ IDomn ∧ g ∈ Word P → ran ⁡ g ⊆ P
187 186 ad2antrr ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ g ≠ ∅ → ran ⁡ g ⊆ P
188 187 sselda ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ g ≠ ∅ ∧ i ∈ ran ⁡ g → i ∈ P
189 2 1 185 188 rprmnunit ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ g ≠ ∅ ∧ i ∈ ran ⁡ g → ¬ i ∈ U
190 nelss ⊢ i ∈ ran ⁡ g ∧ ¬ i ∈ U → ¬ ran ⁡ g ⊆ U
191 184 189 190 syl2anc ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ g ≠ ∅ ∧ i ∈ ran ⁡ g → ¬ ran ⁡ g ⊆ U
192 183 191 exlimddv ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g ∧ g ≠ ∅ → ¬ ran ⁡ g ⊆ U
193 171 192 pm2.65da ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ¬ g ≠ ∅
194 nne ⊢ ¬ g ≠ ∅ ↔ g = ∅
195 193 194 sylib ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → g = ∅
196 125 134 195 rspcedvd ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ∃ u ∈ U ∅ ∅ : ∅ ⟶ 1-1 onto ∅ ∧ g = u · ˙ f ∅ ∘ ∅
197 hash0 ⊢ ∅ = 0
198 197 oveq2i ⊢ 0 ..^ ∅ = 0 ..^ 0
199 fzo0 ⊢ 0 ..^ 0 = ∅
200 198 199 eqtri ⊢ 0 ..^ ∅ = ∅
201 200 oveq2i ⊢ U 0 ..^ ∅ = U ∅
202 201 a1i ⊢ w = ∅ → U 0 ..^ ∅ = U ∅
203 id ⊢ w = ∅ → w = ∅
204 200 a1i ⊢ w = ∅ → 0 ..^ ∅ = ∅
205 203 204 204 f1oeq123d ⊢ w = ∅ → w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅ ↔ ∅ : ∅ ⟶ 1-1 onto ∅
206 coeq2 ⊢ w = ∅ → ∅ ∘ w = ∅ ∘ ∅
207 206 oveq2d ⊢ w = ∅ → u · ˙ f ∅ ∘ w = u · ˙ f ∅ ∘ ∅
208 207 eqeq2d ⊢ w = ∅ → g = u · ˙ f ∅ ∘ w ↔ g = u · ˙ f ∅ ∘ ∅
209 205 208 anbi12d ⊢ w = ∅ → w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅ ∧ g = u · ˙ f ∅ ∘ w ↔ ∅ : ∅ ⟶ 1-1 onto ∅ ∧ g = u · ˙ f ∅ ∘ ∅
210 202 209 rexeqbidv ⊢ w = ∅ → ∃ u ∈ U 0 ..^ ∅ w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅ ∧ g = u · ˙ f ∅ ∘ w ↔ ∃ u ∈ U ∅ ∅ : ∅ ⟶ 1-1 onto ∅ ∧ g = u · ˙ f ∅ ∘ ∅
211 119 196 210 spcedv ⊢ R ∈ IDomn ∧ g ∈ Word P ∧ ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ ∅ w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅ ∧ g = u · ˙ f ∅ ∘ w
212 211 ex ⊢ R ∈ IDomn ∧ g ∈ Word P → ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ ∅ w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅ ∧ g = u · ˙ f ∅ ∘ w
213 212 ralrimiva ⊢ R ∈ IDomn → ∀ g ∈ Word P ∃ k ∈ U ∑ M ∅ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ ∅ w : 0 ..^ ∅ ⟶ 1-1 onto 0 ..^ ∅ ∧ g = u · ˙ f ∅ ∘ w
214 eqid ⊢ 0 ..^ h = 0 ..^ h
215 simp-4r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j → j ∈ 0 ..^ h
216 simp-4r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j → h ∈ Word P
217 216 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j → h ∈ Word P
218 eqid ⊢ h ∘ r prefix h − 1 = h ∘ r prefix h − 1
219 214 215 217 218 wrdpmtrlast ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j → ∃ r r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩
220 eqid ⊢ 0 ..^ f = 0 ..^ f
221 simp-5r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j → R ∈ IDomn
222 221 ad6antr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → R ∈ IDomn
223 simp-5l ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → f ∈ Word P
224 223 ad8antr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → f ∈ Word P
225 eqidd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∑ M f = ∑ M f
226 simp-7r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j → p ∈ P
227 226 ad6antr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → p ∈ P
228 simplr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn → R ∈ IDomn → ∀ 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
229 228 ad10antr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → R ∈ IDomn → ∀ 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
230 222 229 mpd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∀ 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
231 217 ad4antr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h ∈ Word P
232 simp-9r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h
233 215 ad4antr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → j ∈ 0 ..^ h
234 simpr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j → p ∥ r ⁡ R h ⁡ j
235 234 ad6antr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → p ∥ r ⁡ R h ⁡ j
236 simp-6r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → t ∈ U
237 simp-5r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → t · ˙ p = h ⁡ j
238 simp-4r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h
239 simpllr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩
240 simplr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → m ∈ U
241 simpr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h
242 1 2 3 4 220 222 224 224 225 227 230 231 232 233 235 236 237 238 239 240 241 1arithidomlem1 ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∃ c ∃ d ∈ U 0 ..^ f c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c
243 ovexd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → c ++ ⟨“ f ”⟩ ∈ V
244 vex ⊢ r ∈ V
245 244 cnvex ⊢ r -1 ∈ V
246 245 a1i ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → r -1 ∈ V
247 243 246 coexd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → c ++ ⟨“ f ”⟩ ∘ r -1 ∈ V
248 oveq1 ⊢ s = d ++ ⟨“ t ”⟩ ∘ r -1 → s · ˙ f f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1 = d ++ ⟨“ t ”⟩ ∘ r -1 · ˙ f f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1
249 248 eqeq2d ⊢ s = d ++ ⟨“ t ”⟩ ∘ r -1 → h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1 ↔ h = d ++ ⟨“ t ”⟩ ∘ r -1 · ˙ f f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1
250 249 anbi2d ⊢ s = d ++ ⟨“ t ”⟩ ∘ r -1 → c ++ ⟨“ f ”⟩ ∘ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1 ↔ c ++ ⟨“ f ”⟩ ∘ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = d ++ ⟨“ t ”⟩ ∘ r -1 · ˙ f f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1
251 121 a1i ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → U ∈ V
252 ovexd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → 0 ..^ f ++ ⟨“ p ”⟩ ∈ V
253 simplr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d ∈ U 0 ..^ f
254 elmapi ⊢ d ∈ U 0 ..^ f → d : 0 ..^ f ⟶ U
255 253 254 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d : 0 ..^ f ⟶ U
256 iswrdi ⊢ d : 0 ..^ f ⟶ U → d ∈ Word U
257 255 256 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d ∈ Word U
258 ccatws1len ⊢ d ∈ Word U → d ++ ⟨“ t ”⟩ = d + 1
259 257 258 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d ++ ⟨“ t ”⟩ = d + 1
260 elmapfn ⊢ d ∈ U 0 ..^ f → d Fn 0 ..^ f
261 hashfn ⊢ d Fn 0 ..^ f → d = 0 ..^ f
262 253 260 261 3syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d = 0 ..^ f
263 223 ad10antr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → f ∈ Word P
264 lencl ⊢ f ∈ Word P → f ∈ ℕ 0
265 263 264 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → f ∈ ℕ 0
266 hashfzo0 ⊢ f ∈ ℕ 0 → 0 ..^ f = f
267 265 266 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → 0 ..^ f = f
268 262 267 eqtrd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d = f
269 268 oveq1d ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d + 1 = f + 1
270 simprr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → h ∘ r prefix h − 1 = d · ˙ f f ∘ c
271 270 dmeqd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → dom ⁡ h ∘ r prefix h − 1 = dom ⁡ d · ˙ f f ∘ c
272 f1of ⊢ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h → r : 0 ..^ h ⟶ 0 ..^ h
273 iswrdi ⊢ r : 0 ..^ h ⟶ 0 ..^ h → r ∈ Word 0 ..^ h
274 238 272 273 3syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → r ∈ Word 0 ..^ h
275 eqidd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j → h = h
276 275 216 wrdfd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j → h : 0 ..^ h ⟶ P
277 276 ad6antr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h : 0 ..^ h ⟶ P
278 wrdco ⊢ r ∈ Word 0 ..^ h ∧ h : 0 ..^ h ⟶ P → h ∘ r ∈ Word P
279 274 277 278 syl2anc ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h ∘ r ∈ Word P
280 279 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → h ∘ r ∈ Word P
281 elfzo0 ⊢ j ∈ 0 ..^ h ↔ j ∈ ℕ 0 ∧ h ∈ ℕ ∧ j < h
282 281 simp2bi ⊢ j ∈ 0 ..^ h → h ∈ ℕ
283 nnm1nn0 ⊢ h ∈ ℕ → h − 1 ∈ ℕ 0
284 233 282 283 3syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h − 1 ∈ ℕ 0
285 lenco ⊢ r ∈ Word 0 ..^ h ∧ h : 0 ..^ h ⟶ P → h ∘ r = r
286 274 277 285 syl2anc ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h ∘ r = r
287 lencl ⊢ r ∈ Word 0 ..^ h → r ∈ ℕ 0
288 274 287 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → r ∈ ℕ 0
289 286 288 eqeltrd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h ∘ r ∈ ℕ 0
290 lencl ⊢ h ∈ Word P → h ∈ ℕ 0
291 231 290 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h ∈ ℕ 0
292 291 nn0red ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h ∈ ℝ
293 292 lem1d ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h − 1 ≤ h
294 238 272 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → r : 0 ..^ h ⟶ 0 ..^ h
295 ffn ⊢ r : 0 ..^ h ⟶ 0 ..^ h → r Fn 0 ..^ h
296 hashfn ⊢ r Fn 0 ..^ h → r = 0 ..^ h
297 294 295 296 3syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → r = 0 ..^ h
298 hashfzo0 ⊢ h ∈ ℕ 0 → 0 ..^ h = h
299 231 290 298 3syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → 0 ..^ h = h
300 286 297 299 3eqtrrd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h = h ∘ r
301 293 300 breqtrd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h − 1 ≤ h ∘ r
302 elfz2nn0 ⊢ h − 1 ∈ 0 … h ∘ r ↔ h − 1 ∈ ℕ 0 ∧ h ∘ r ∈ ℕ 0 ∧ h − 1 ≤ h ∘ r
303 284 289 301 302 syl3anbrc ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h − 1 ∈ 0 … h ∘ r
304 303 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → h − 1 ∈ 0 … h ∘ r
305 pfxfn ⊢ h ∘ r ∈ Word P ∧ h − 1 ∈ 0 … h ∘ r → h ∘ r prefix h − 1 Fn 0 ..^ h − 1
306 280 304 305 syl2anc ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → h ∘ r prefix h − 1 Fn 0 ..^ h − 1
307 306 fndmd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → dom ⁡ h ∘ r prefix h − 1 = 0 ..^ h − 1
308 222 idomringd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → R ∈ Ring
309 308 ad3antrrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c ∧ x ∈ U ∧ y ∈ P → R ∈ Ring
310 simprl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c ∧ x ∈ U ∧ y ∈ P → x ∈ U
311 16 1 unitcl ⊢ x ∈ U → x ∈ Base R
312 310 311 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c ∧ x ∈ U ∧ y ∈ P → x ∈ Base R
313 222 ad3antrrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c ∧ x ∈ U ∧ y ∈ P → R ∈ IDomn
314 simprr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c ∧ x ∈ U ∧ y ∈ P → y ∈ P
315 16 2 313 314 rprmcl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c ∧ x ∈ U ∧ y ∈ P → y ∈ Base R
316 16 4 309 312 315 ringcld ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c ∧ x ∈ U ∧ y ∈ P → x · ˙ y ∈ Base R
317 eqidd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → f = f
318 317 263 wrdfd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → f : 0 ..^ f ⟶ P
319 simprl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f
320 f1of ⊢ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f → c : 0 ..^ f ⟶ 0 ..^ f
321 319 320 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → c : 0 ..^ f ⟶ 0 ..^ f
322 318 321 fcod ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → f ∘ c : 0 ..^ f ⟶ P
323 ovexd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → 0 ..^ f ∈ V
324 inidm ⊢ 0 ..^ f ∩ 0 ..^ f = 0 ..^ f
325 316 255 322 323 323 324 off ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d · ˙ f f ∘ c : 0 ..^ f ⟶ Base R
326 325 fdmd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → dom ⁡ d · ˙ f f ∘ c = 0 ..^ f
327 271 307 326 3eqtr3d ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → 0 ..^ h − 1 = 0 ..^ f
328 284 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → h − 1 ∈ ℕ 0
329 328 265 fzo0opth ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → 0 ..^ h − 1 = 0 ..^ f ↔ h − 1 = f
330 327 329 mpbid ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → h − 1 = f
331 330 oveq1d ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → h - 1 + 1 = f + 1
332 282 ad10antlr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → h ∈ ℕ
333 332 nncnd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → h ∈ ℂ
334 npcan1 ⊢ h ∈ ℂ → h - 1 + 1 = h
335 333 334 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → h - 1 + 1 = h
336 331 335 eqtr3d ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → f + 1 = h
337 259 269 336 3eqtrd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d ++ ⟨“ t ”⟩ = h
338 337 oveq2d ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → 0 ..^ d ++ ⟨“ t ”⟩ = 0 ..^ h
339 eqidd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d ++ ⟨“ t ”⟩ = d ++ ⟨“ t ”⟩
340 236 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → t ∈ U
341 ccatws1cl ⊢ d ∈ Word U ∧ t ∈ U → d ++ ⟨“ t ”⟩ ∈ Word U
342 257 340 341 syl2anc ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d ++ ⟨“ t ”⟩ ∈ Word U
343 339 342 wrdfd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d ++ ⟨“ t ”⟩ : 0 ..^ d ++ ⟨“ t ”⟩ ⟶ U
344 338 343 feq2dd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d ++ ⟨“ t ”⟩ : 0 ..^ h ⟶ U
345 ccatws1len ⊢ f ∈ Word P → f ++ ⟨“ p ”⟩ = f + 1
346 263 345 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → f ++ ⟨“ p ”⟩ = f + 1
347 346 336 eqtrd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → f ++ ⟨“ p ”⟩ = h
348 347 oveq2d ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → 0 ..^ f ++ ⟨“ p ”⟩ = 0 ..^ h
349 348 eqcomd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → 0 ..^ h = 0 ..^ f ++ ⟨“ p ”⟩
350 238 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h
351 f1ocnv ⊢ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h → r -1 : 0 ..^ h ⟶ 1-1 onto 0 ..^ h
352 f1of ⊢ r -1 : 0 ..^ h ⟶ 1-1 onto 0 ..^ h → r -1 : 0 ..^ h ⟶ 0 ..^ h
353 350 351 352 3syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → r -1 : 0 ..^ h ⟶ 0 ..^ h
354 349 353 feq2dd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → r -1 : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 0 ..^ h
355 344 354 fcod ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d ++ ⟨“ t ”⟩ ∘ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ U
356 251 252 355 elmapdd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → d ++ ⟨“ t ”⟩ ∘ r -1 ∈ U 0 ..^ f ++ ⟨“ p ”⟩
357 222 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → R ∈ IDomn
358 eqidd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → ∑ M f = ∑ M f
359 227 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → p ∈ P
360 230 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → ∀ 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
361 231 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → h ∈ Word P
362 232 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h
363 233 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → j ∈ 0 ..^ h
364 235 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → p ∥ r ⁡ R h ⁡ j
365 237 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → t · ˙ p = h ⁡ j
366 simp-5r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩
367 simp-4r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → m ∈ U
368 simpllr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h
369 1 2 3 4 220 357 263 263 358 359 360 361 362 363 364 340 365 350 366 367 368 253 319 270 1arithidomlem2 ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → c ++ ⟨“ f ”⟩ ∘ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = d ++ ⟨“ t ”⟩ ∘ r -1 · ˙ f f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1
370 250 356 369 rspcedvdw ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ ∘ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1
371 f1oeq1 ⊢ v = c ++ ⟨“ f ”⟩ ∘ r -1 → v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ↔ c ++ ⟨“ f ”⟩ ∘ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩
372 coeq2 ⊢ v = c ++ ⟨“ f ”⟩ ∘ r -1 → f ++ ⟨“ p ”⟩ ∘ v = f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1
373 372 oveq2d ⊢ v = c ++ ⟨“ f ”⟩ ∘ r -1 → s · ˙ f f ++ ⟨“ p ”⟩ ∘ v = s · ˙ f f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1
374 373 eqeq2d ⊢ v = c ++ ⟨“ f ”⟩ ∘ r -1 → h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1
375 371 374 anbi12d ⊢ v = c ++ ⟨“ f ”⟩ ∘ r -1 → v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ c ++ ⟨“ f ”⟩ ∘ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1
376 375 rexbidv ⊢ v = c ++ ⟨“ f ”⟩ ∘ r -1 → ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ ∘ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ c ++ ⟨“ f ”⟩ ∘ r -1
377 247 370 376 spcedv ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ d ∈ U 0 ..^ f ∧ c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
378 377 r19.29an ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h ∧ ∃ d ∈ U 0 ..^ f c : 0 ..^ f ⟶ 1-1 onto 0 ..^ f ∧ h ∘ r prefix h − 1 = d · ˙ f f ∘ c → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
379 242 378 exlimddv ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
380 simp-7r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ → ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h
381 oveq1 ⊢ k = m → k · ˙ ∑ M h = m · ˙ ∑ M h
382 381 eqeq2d ⊢ k = m → ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ↔ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h
383 382 cbvrexvw ⊢ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ↔ ∃ m ∈ U ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h
384 380 383 sylib ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ → ∃ m ∈ U ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h
385 379 384 r19.29a ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
386 385 anasss ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j ∧ r : 0 ..^ h ⟶ 1-1 onto 0 ..^ h ∧ h ∘ r = h ∘ r prefix h − 1 ++ ⟨“ h ⁡ j ”⟩ → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
387 219 386 exlimddv ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j ∧ t ∈ U ∧ t · ˙ p = h ⁡ j → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
388 eqid ⊢ ∥ r ⁡ R = ∥ r ⁡ R
389 simplr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j → j ∈ 0 ..^ h
390 276 389 ffvelcdmd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j → h ⁡ j ∈ P
391 16 2 388 221 226 234 390 4 1 rprmasso3 ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j → ∃ t ∈ U t · ˙ p = h ⁡ j
392 387 391 r19.29a ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ j ∈ 0 ..^ h ∧ p ∥ r ⁡ R h ⁡ j → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
393 suppssdm ⊢ h supp 1 R ⊆ dom ⁡ h
394 eqidd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h = h
395 simpllr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → R ∈ IDomn
396 395 150 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → Word P ⊆ Word Base R
397 396 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → Word P ⊆ Word Base R
398 simp-4r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h ∈ Word P
399 397 398 sseldd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h ∈ Word Base R
400 394 399 wrdfd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h : 0 ..^ h ⟶ Base R
401 393 400 fssdm ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → h supp 1 R ⊆ 0 ..^ h
402 21 ad5antlr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → R ∈ CRing
403 simp-5r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → p ∈ P
404 403 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → p ∈ P
405 ovexd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → 0 ..^ h ∈ V
406 fvexd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → 1 R ∈ V
407 406 398 wrdfsupp ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → finSupp 1 R⁡ h
408 simp-5r ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → R ∈ IDomn
409 simplr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → m ∈ U
410 16 1 unitcl ⊢ m ∈ U → m ∈ Base R
411 409 410 syl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → m ∈ Base R
412 23 ad5antlr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → M ∈ CMnd
413 18 19 412 405 400 407 gsumcl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∑ M h ∈ Base R
414 16 2 395 403 rprmcl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → p ∈ Base R
415 414 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → p ∈ Base R
416 ovexd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → 0 ..^ f ∈ V
417 eqidd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → f = f
418 396 223 sseldd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → f ∈ Word Base R
419 418 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → f ∈ Word Base R
420 417 419 wrdfd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → f : 0 ..^ f ⟶ Base R
421 406 419 wrdfsupp ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → finSupp 1 R⁡ f
422 18 19 412 416 420 421 gsumcl ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∑ M f ∈ Base R
423 16 388 4 dvdsrmul ⊢ p ∈ Base R ∧ ∑ M f ∈ Base R → p ∥ r ⁡ R ∑ M f · ˙ p
424 415 422 423 syl2anc ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → p ∥ r ⁡ R ∑ M f · ˙ p
425 20 idomringd ⊢ R ∈ IDomn → R ∈ Ring
426 3 ringmgp ⊢ R ∈ Ring → M ∈ Mnd
427 425 426 syl ⊢ R ∈ IDomn → M ∈ Mnd
428 427 ad3antlr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → M ∈ Mnd
429 3 4 mgpplusg ⊢ · ˙ = + M
430 18 429 gsumccatsn ⊢ M ∈ Mnd ∧ f ∈ Word Base R ∧ p ∈ Base R → ∑ M f ++ ⟨“ p ”⟩ = ∑ M f · ˙ p
431 428 418 414 430 syl3anc ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → ∑ M f ++ ⟨“ p ”⟩ = ∑ M f · ˙ p
432 431 ad2antrr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∑ M f ++ ⟨“ p ”⟩ = ∑ M f · ˙ p
433 simpr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h
434 432 433 eqtr3d ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∑ M f · ˙ p = m · ˙ ∑ M h
435 424 434 breqtrd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → p ∥ r ⁡ R m · ˙ ∑ M h
436 16 2 388 4 408 404 411 413 435 rprmdvds ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → p ∥ r ⁡ R m ∨ p ∥ r ⁡ R ∑ M h
437 1 2 388 402 404 409 rprmndvdsru ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ¬ p ∥ r ⁡ R m
438 436 437 orcnd ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → p ∥ r ⁡ R ∑ M h
439 16 2 388 11 3 402 404 405 407 400 438 rprmdvdsprod ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∃ j ∈ supp 1 R⁡ h p ∥ r ⁡ R h ⁡ j
440 ssrexv ⊢ h supp 1 R ⊆ 0 ..^ h → ∃ j ∈ supp 1 R⁡ h p ∥ r ⁡ R h ⁡ j → ∃ j ∈ 0 ..^ h p ∥ r ⁡ R h ⁡ j
441 401 439 440 sylc ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h ∧ m ∈ U ∧ ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h → ∃ j ∈ 0 ..^ h p ∥ r ⁡ R h ⁡ j
442 383 bilani ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → ∃ m ∈ U ∑ M f ++ ⟨“ p ”⟩ = m · ˙ ∑ M h
443 441 442 r19.29a ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → ∃ j ∈ 0 ..^ h p ∥ r ⁡ R h ⁡ j
444 392 443 r19.29a ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P ∧ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
445 444 ex ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn ∧ h ∈ Word P → ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
446 445 ralrimiva ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn → ∀ h ∈ Word P ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
447 f1oeq1 ⊢ w = v → w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ↔ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩
448 coeq2 ⊢ w = v → f ++ ⟨“ p ”⟩ ∘ w = f ++ ⟨“ p ”⟩ ∘ v
449 448 oveq2d ⊢ w = v → u · ˙ f f ++ ⟨“ p ”⟩ ∘ w = u · ˙ f f ++ ⟨“ p ”⟩ ∘ v
450 449 eqeq2d ⊢ w = v → g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w ↔ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ v
451 447 450 anbi12d ⊢ w = v → w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w ↔ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ v
452 451 rexbidv ⊢ w = v → ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w ↔ ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ v
453 452 cbvexvw ⊢ ∃ w ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w ↔ ∃ v ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ v
454 oveq1 ⊢ u = s → u · ˙ f f ++ ⟨“ p ”⟩ ∘ v = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
455 454 eqeq2d ⊢ u = s → g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
456 455 anbi2d ⊢ u = s → v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
457 456 cbvrexvw ⊢ ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
458 457 exbii ⊢ ∃ v ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
459 453 458 bitri ⊢ ∃ w ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w ↔ ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
460 459 imbi2i ⊢ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w ↔ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
461 460 ralbii ⊢ ∀ g ∈ Word P ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w ↔ ∀ g ∈ Word P ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
462 oveq2 ⊢ g = h → ∑ M g = ∑ M h
463 462 oveq2d ⊢ g = h → k · ˙ ∑ M g = k · ˙ ∑ M h
464 463 eqeq2d ⊢ g = h → ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g ↔ ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h
465 464 rexbidv ⊢ g = h → ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g ↔ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h
466 eqeq1 ⊢ g = h → g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
467 466 anbi2d ⊢ g = h → v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
468 467 rexbidv ⊢ g = h → ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
469 468 exbidv ⊢ g = h → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
470 465 469 imbi12d ⊢ g = h → ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
471 470 cbvralvw ⊢ ∀ g ∈ Word P ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v ↔ ∀ h ∈ Word P ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
472 461 471 bitri ⊢ ∀ g ∈ Word P ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w ↔ ∀ h ∈ Word P ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M h → ∃ v ∃ s ∈ U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ h = s · ˙ f f ++ ⟨“ p ”⟩ ∘ v
473 446 472 sylibr ⊢ f ∈ Word P ∧ p ∈ P ∧ R ∈ IDomn → ∀ 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 ∧ R ∈ IDomn → ∀ g ∈ Word P ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w
474 473 exp31 ⊢ f ∈ Word P ∧ p ∈ P → R ∈ IDomn → ∀ 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 → R ∈ IDomn → ∀ g ∈ Word P ∃ k ∈ U ∑ M f ++ ⟨“ p ”⟩ = k · ˙ ∑ M g → ∃ w ∃ u ∈ U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ ⟶ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ ∧ g = u · ˙ f f ++ ⟨“ p ”⟩ ∘ w
475 66 83 100 117 213 474 wrdind ⊢ F ∈ Word P → R ∈ IDomn → ∀ 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
476 7 6 475 sylc ⊢ φ → ∀ 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
477 49 476 8 rspcdva ⊢ φ → ∃ 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
478 40 477 mpd ⊢ φ → ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ G = u · ˙ f F ∘ w
479 5 oveq2i ⊢ U J = U 0 ..^ F
480 f1oeq23 ⊢ J = 0 ..^ F ∧ J = 0 ..^ F → w : J ⟶ 1-1 onto J ↔ w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F
481 5 5 480 mp2an ⊢ w : J ⟶ 1-1 onto J ↔ w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F
482 481 anbi1i ⊢ w : J ⟶ 1-1 onto J ∧ G = u · ˙ f F ∘ w ↔ w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ G = u · ˙ f F ∘ w
483 479 482 rexeqbii ⊢ ∃ u ∈ U J w : J ⟶ 1-1 onto J ∧ G = u · ˙ f F ∘ w ↔ ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ G = u · ˙ f F ∘ w
484 483 exbii ⊢ ∃ w ∃ u ∈ U J w : J ⟶ 1-1 onto J ∧ G = u · ˙ f F ∘ w ↔ ∃ w ∃ u ∈ U 0 ..^ F w : 0 ..^ F ⟶ 1-1 onto 0 ..^ F ∧ G = u · ˙ f F ∘ w
485 478 484 sylibr ⊢ φ → ∃ w ∃ u ∈ U J w : J ⟶ 1-1 onto J ∧ G = u · ˙ f F ∘ w