This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsmsymgreq

Description: Two combination of permutations moves an element of the intersection of the base sets of the permutations to the same element if each pair of corresponding permutations moves such an element to the same element. (Contributed by AV, 20-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s ⊢ S = SymGrp ⁡ N
gsmsymgrfix.b ⊢ B = Base S
gsmsymgreq.z ⊢ Z = SymGrp ⁡ M
gsmsymgreq.p ⊢ P = Base Z
gsmsymgreq.i ⊢ I = N ∩ M
Assertion gsmsymgreq ⊢ N ∈ Fin ∧ M ∈ Fin ∧ W ∈ Word B ∧ U ∈ Word P ∧ W = U → ∀ i ∈ 0 ..^ W ∀ n ∈ I W ⁡ i ⁡ n = U ⁡ i ⁡ n → ∀ n ∈ I ∑ S W ⁡ n = ∑ Z U ⁡ n

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s ⊢ S = SymGrp ⁡ N
2 gsmsymgrfix.b ⊢ B = Base S
3 gsmsymgreq.z ⊢ Z = SymGrp ⁡ M
4 gsmsymgreq.p ⊢ P = Base Z
5 gsmsymgreq.i ⊢ I = N ∩ M
6 fveq2 ⊢ w = ∅ → w = ∅
7 6 oveq2d ⊢ w = ∅ → 0 ..^ w = 0 ..^ ∅
8 7 adantr ⊢ w = ∅ ∧ u = ∅ → 0 ..^ w = 0 ..^ ∅
9 fveq1 ⊢ w = ∅ → w ⁡ i = ∅ ⁡ i
10 9 fveq1d ⊢ w = ∅ → w ⁡ i ⁡ n = ∅ ⁡ i ⁡ n
11 fveq1 ⊢ u = ∅ → u ⁡ i = ∅ ⁡ i
12 11 fveq1d ⊢ u = ∅ → u ⁡ i ⁡ n = ∅ ⁡ i ⁡ n
13 10 12 eqeqan12d ⊢ w = ∅ ∧ u = ∅ → w ⁡ i ⁡ n = u ⁡ i ⁡ n ↔ ∅ ⁡ i ⁡ n = ∅ ⁡ i ⁡ n
14 13 ralbidv ⊢ w = ∅ ∧ u = ∅ → ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n ↔ ∀ n ∈ I ∅ ⁡ i ⁡ n = ∅ ⁡ i ⁡ n
15 8 14 raleqbidv ⊢ w = ∅ ∧ u = ∅ → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n ↔ ∀ i ∈ 0 ..^ ∅ ∀ n ∈ I ∅ ⁡ i ⁡ n = ∅ ⁡ i ⁡ n
16 oveq2 ⊢ w = ∅ → ∑ S w = ∑ S ∅
17 16 fveq1d ⊢ w = ∅ → ∑ S w ⁡ n = ∑ S ∅ ⁡ n
18 oveq2 ⊢ u = ∅ → ∑ Z u = ∑ Z ∅
19 18 fveq1d ⊢ u = ∅ → ∑ Z u ⁡ n = ∑ Z ∅ ⁡ n
20 17 19 eqeqan12d ⊢ w = ∅ ∧ u = ∅ → ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ ∑ S ∅ ⁡ n = ∑ Z ∅ ⁡ n
21 20 ralbidv ⊢ w = ∅ ∧ u = ∅ → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ ∀ n ∈ I ∑ S ∅ ⁡ n = ∑ Z ∅ ⁡ n
22 15 21 imbi12d ⊢ w = ∅ ∧ u = ∅ → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ ∀ i ∈ 0 ..^ ∅ ∀ n ∈ I ∅ ⁡ i ⁡ n = ∅ ⁡ i ⁡ n → ∀ n ∈ I ∑ S ∅ ⁡ n = ∑ Z ∅ ⁡ n
23 22 imbi2d ⊢ w = ∅ ∧ u = ∅ → N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ ∅ ∀ n ∈ I ∅ ⁡ i ⁡ n = ∅ ⁡ i ⁡ n → ∀ n ∈ I ∑ S ∅ ⁡ n = ∑ Z ∅ ⁡ n
24 fveq2 ⊢ w = x → w = x
25 24 oveq2d ⊢ w = x → 0 ..^ w = 0 ..^ x
26 25 adantr ⊢ w = x ∧ u = y → 0 ..^ w = 0 ..^ x
27 fveq1 ⊢ w = x → w ⁡ i = x ⁡ i
28 27 fveq1d ⊢ w = x → w ⁡ i ⁡ n = x ⁡ i ⁡ n
29 fveq1 ⊢ u = y → u ⁡ i = y ⁡ i
30 29 fveq1d ⊢ u = y → u ⁡ i ⁡ n = y ⁡ i ⁡ n
31 28 30 eqeqan12d ⊢ w = x ∧ u = y → w ⁡ i ⁡ n = u ⁡ i ⁡ n ↔ x ⁡ i ⁡ n = y ⁡ i ⁡ n
32 31 ralbidv ⊢ w = x ∧ u = y → ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n ↔ ∀ n ∈ I x ⁡ i ⁡ n = y ⁡ i ⁡ n
33 26 32 raleqbidv ⊢ w = x ∧ u = y → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n ↔ ∀ i ∈ 0 ..^ x ∀ n ∈ I x ⁡ i ⁡ n = y ⁡ i ⁡ n
34 oveq2 ⊢ w = x → ∑ S w = ∑ S x
35 34 fveq1d ⊢ w = x → ∑ S w ⁡ n = ∑ S x ⁡ n
36 oveq2 ⊢ u = y → ∑ Z u = ∑ Z y
37 36 fveq1d ⊢ u = y → ∑ Z u ⁡ n = ∑ Z y ⁡ n
38 35 37 eqeqan12d ⊢ w = x ∧ u = y → ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ ∑ S x ⁡ n = ∑ Z y ⁡ n
39 38 ralbidv ⊢ w = x ∧ u = y → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ ∀ n ∈ I ∑ S x ⁡ n = ∑ Z y ⁡ n
40 33 39 imbi12d ⊢ w = x ∧ u = y → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ ∀ i ∈ 0 ..^ x ∀ n ∈ I x ⁡ i ⁡ n = y ⁡ i ⁡ n → ∀ n ∈ I ∑ S x ⁡ n = ∑ Z y ⁡ n
41 40 imbi2d ⊢ w = x ∧ u = y → N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ x ∀ n ∈ I x ⁡ i ⁡ n = y ⁡ i ⁡ n → ∀ n ∈ I ∑ S x ⁡ n = ∑ Z y ⁡ n
42 fveq2 ⊢ w = x ++ ⟨“ b ”⟩ → w = x ++ ⟨“ b ”⟩
43 42 oveq2d ⊢ w = x ++ ⟨“ b ”⟩ → 0 ..^ w = 0 ..^ x ++ ⟨“ b ”⟩
44 43 adantr ⊢ w = x ++ ⟨“ b ”⟩ ∧ u = y ++ ⟨“ p ”⟩ → 0 ..^ w = 0 ..^ x ++ ⟨“ b ”⟩
45 fveq1 ⊢ w = x ++ ⟨“ b ”⟩ → w ⁡ i = x ++ ⟨“ b ”⟩ ⁡ i
46 45 fveq1d ⊢ w = x ++ ⟨“ b ”⟩ → w ⁡ i ⁡ n = x ++ ⟨“ b ”⟩ ⁡ i ⁡ n
47 fveq1 ⊢ u = y ++ ⟨“ p ”⟩ → u ⁡ i = y ++ ⟨“ p ”⟩ ⁡ i
48 47 fveq1d ⊢ u = y ++ ⟨“ p ”⟩ → u ⁡ i ⁡ n = y ++ ⟨“ p ”⟩ ⁡ i ⁡ n
49 46 48 eqeqan12d ⊢ w = x ++ ⟨“ b ”⟩ ∧ u = y ++ ⟨“ p ”⟩ → w ⁡ i ⁡ n = u ⁡ i ⁡ n ↔ x ++ ⟨“ b ”⟩ ⁡ i ⁡ n = y ++ ⟨“ p ”⟩ ⁡ i ⁡ n
50 49 ralbidv ⊢ w = x ++ ⟨“ b ”⟩ ∧ u = y ++ ⟨“ p ”⟩ → ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n ↔ ∀ n ∈ I x ++ ⟨“ b ”⟩ ⁡ i ⁡ n = y ++ ⟨“ p ”⟩ ⁡ i ⁡ n
51 44 50 raleqbidv ⊢ w = x ++ ⟨“ b ”⟩ ∧ u = y ++ ⟨“ p ”⟩ → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n ↔ ∀ i ∈ 0 ..^ x ++ ⟨“ b ”⟩ ∀ n ∈ I x ++ ⟨“ b ”⟩ ⁡ i ⁡ n = y ++ ⟨“ p ”⟩ ⁡ i ⁡ n
52 oveq2 ⊢ w = x ++ ⟨“ b ”⟩ → ∑ S w = ∑ S x ++ ⟨“ b ”⟩
53 52 fveq1d ⊢ w = x ++ ⟨“ b ”⟩ → ∑ S w ⁡ n = ∑ S x ++ ⟨“ b ”⟩ ⁡ n
54 oveq2 ⊢ u = y ++ ⟨“ p ”⟩ → ∑ Z u = ∑ Z y ++ ⟨“ p ”⟩
55 54 fveq1d ⊢ u = y ++ ⟨“ p ”⟩ → ∑ Z u ⁡ n = ∑ Z y ++ ⟨“ p ”⟩ ⁡ n
56 53 55 eqeqan12d ⊢ w = x ++ ⟨“ b ”⟩ ∧ u = y ++ ⟨“ p ”⟩ → ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ ∑ S x ++ ⟨“ b ”⟩ ⁡ n = ∑ Z y ++ ⟨“ p ”⟩ ⁡ n
57 56 ralbidv ⊢ w = x ++ ⟨“ b ”⟩ ∧ u = y ++ ⟨“ p ”⟩ → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ ∀ n ∈ I ∑ S x ++ ⟨“ b ”⟩ ⁡ n = ∑ Z y ++ ⟨“ p ”⟩ ⁡ n
58 51 57 imbi12d ⊢ w = x ++ ⟨“ b ”⟩ ∧ u = y ++ ⟨“ p ”⟩ → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ ∀ i ∈ 0 ..^ x ++ ⟨“ b ”⟩ ∀ n ∈ I x ++ ⟨“ b ”⟩ ⁡ i ⁡ n = y ++ ⟨“ p ”⟩ ⁡ i ⁡ n → ∀ n ∈ I ∑ S x ++ ⟨“ b ”⟩ ⁡ n = ∑ Z y ++ ⟨“ p ”⟩ ⁡ n
59 58 imbi2d ⊢ w = x ++ ⟨“ b ”⟩ ∧ u = y ++ ⟨“ p ”⟩ → N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ x ++ ⟨“ b ”⟩ ∀ n ∈ I x ++ ⟨“ b ”⟩ ⁡ i ⁡ n = y ++ ⟨“ p ”⟩ ⁡ i ⁡ n → ∀ n ∈ I ∑ S x ++ ⟨“ b ”⟩ ⁡ n = ∑ Z y ++ ⟨“ p ”⟩ ⁡ n
60 fveq2 ⊢ w = W → w = W
61 60 oveq2d ⊢ w = W → 0 ..^ w = 0 ..^ W
62 fveq1 ⊢ w = W → w ⁡ i = W ⁡ i
63 62 fveq1d ⊢ w = W → w ⁡ i ⁡ n = W ⁡ i ⁡ n
64 63 eqeq1d ⊢ w = W → w ⁡ i ⁡ n = U ⁡ i ⁡ n ↔ W ⁡ i ⁡ n = U ⁡ i ⁡ n
65 64 ralbidv ⊢ w = W → ∀ n ∈ I w ⁡ i ⁡ n = U ⁡ i ⁡ n ↔ ∀ n ∈ I W ⁡ i ⁡ n = U ⁡ i ⁡ n
66 61 65 raleqbidv ⊢ w = W → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = U ⁡ i ⁡ n ↔ ∀ i ∈ 0 ..^ W ∀ n ∈ I W ⁡ i ⁡ n = U ⁡ i ⁡ n
67 oveq2 ⊢ w = W → ∑ S w = ∑ S W
68 67 fveq1d ⊢ w = W → ∑ S w ⁡ n = ∑ S W ⁡ n
69 68 eqeq1d ⊢ w = W → ∑ S w ⁡ n = ∑ Z U ⁡ n ↔ ∑ S W ⁡ n = ∑ Z U ⁡ n
70 69 ralbidv ⊢ w = W → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z U ⁡ n ↔ ∀ n ∈ I ∑ S W ⁡ n = ∑ Z U ⁡ n
71 66 70 imbi12d ⊢ w = W → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = U ⁡ i ⁡ n → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z U ⁡ n ↔ ∀ i ∈ 0 ..^ W ∀ n ∈ I W ⁡ i ⁡ n = U ⁡ i ⁡ n → ∀ n ∈ I ∑ S W ⁡ n = ∑ Z U ⁡ n
72 71 imbi2d ⊢ w = W → N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = U ⁡ i ⁡ n → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z U ⁡ n ↔ N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ W ∀ n ∈ I W ⁡ i ⁡ n = U ⁡ i ⁡ n → ∀ n ∈ I ∑ S W ⁡ n = ∑ Z U ⁡ n
73 fveq1 ⊢ u = U → u ⁡ i = U ⁡ i
74 73 fveq1d ⊢ u = U → u ⁡ i ⁡ n = U ⁡ i ⁡ n
75 74 eqeq2d ⊢ u = U → w ⁡ i ⁡ n = u ⁡ i ⁡ n ↔ w ⁡ i ⁡ n = U ⁡ i ⁡ n
76 75 ralbidv ⊢ u = U → ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n ↔ ∀ n ∈ I w ⁡ i ⁡ n = U ⁡ i ⁡ n
77 76 ralbidv ⊢ u = U → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n ↔ ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = U ⁡ i ⁡ n
78 oveq2 ⊢ u = U → ∑ Z u = ∑ Z U
79 78 fveq1d ⊢ u = U → ∑ Z u ⁡ n = ∑ Z U ⁡ n
80 79 eqeq2d ⊢ u = U → ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ ∑ S w ⁡ n = ∑ Z U ⁡ n
81 80 ralbidv ⊢ u = U → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ ∀ n ∈ I ∑ S w ⁡ n = ∑ Z U ⁡ n
82 77 81 imbi12d ⊢ u = U → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = U ⁡ i ⁡ n → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z U ⁡ n
83 82 imbi2d ⊢ u = U → N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = u ⁡ i ⁡ n → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z u ⁡ n ↔ N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ w ∀ n ∈ I w ⁡ i ⁡ n = U ⁡ i ⁡ n → ∀ n ∈ I ∑ S w ⁡ n = ∑ Z U ⁡ n
84 eleq2 ⊢ I = N ∩ M → n ∈ I ↔ n ∈ N ∩ M
85 elin ⊢ n ∈ N ∩ M ↔ n ∈ N ∧ n ∈ M
86 84 85 bitrdi ⊢ I = N ∩ M → n ∈ I ↔ n ∈ N ∧ n ∈ M
87 simpl ⊢ n ∈ N ∧ n ∈ M → n ∈ N
88 86 87 biimtrdi ⊢ I = N ∩ M → n ∈ I → n ∈ N
89 5 88 ax-mp ⊢ n ∈ I → n ∈ N
90 89 adantl ⊢ N ∈ Fin ∧ M ∈ Fin ∧ n ∈ I → n ∈ N
91 fvresi ⊢ n ∈ N → I ↾ N ⁡ n = n
92 90 91 syl ⊢ N ∈ Fin ∧ M ∈ Fin ∧ n ∈ I → I ↾ N ⁡ n = n
93 simpr ⊢ n ∈ N ∧ n ∈ M → n ∈ M
94 86 93 biimtrdi ⊢ I = N ∩ M → n ∈ I → n ∈ M
95 5 94 ax-mp ⊢ n ∈ I → n ∈ M
96 95 adantl ⊢ N ∈ Fin ∧ M ∈ Fin ∧ n ∈ I → n ∈ M
97 fvresi ⊢ n ∈ M → I ↾ M ⁡ n = n
98 96 97 syl ⊢ N ∈ Fin ∧ M ∈ Fin ∧ n ∈ I → I ↾ M ⁡ n = n
99 92 98 eqtr4d ⊢ N ∈ Fin ∧ M ∈ Fin ∧ n ∈ I → I ↾ N ⁡ n = I ↾ M ⁡ n
100 99 ralrimiva ⊢ N ∈ Fin ∧ M ∈ Fin → ∀ n ∈ I I ↾ N ⁡ n = I ↾ M ⁡ n
101 eqid ⊢ 0 S = 0 S
102 101 gsum0 ⊢ ∑ S ∅ = 0 S
103 1 symgid ⊢ N ∈ Fin → I ↾ N = 0 S
104 103 adantr ⊢ N ∈ Fin ∧ M ∈ Fin → I ↾ N = 0 S
105 102 104 eqtr4id ⊢ N ∈ Fin ∧ M ∈ Fin → ∑ S ∅ = I ↾ N
106 105 fveq1d ⊢ N ∈ Fin ∧ M ∈ Fin → ∑ S ∅ ⁡ n = I ↾ N ⁡ n
107 eqid ⊢ 0 Z = 0 Z
108 107 gsum0 ⊢ ∑ Z ∅ = 0 Z
109 3 symgid ⊢ M ∈ Fin → I ↾ M = 0 Z
110 109 adantl ⊢ N ∈ Fin ∧ M ∈ Fin → I ↾ M = 0 Z
111 108 110 eqtr4id ⊢ N ∈ Fin ∧ M ∈ Fin → ∑ Z ∅ = I ↾ M
112 111 fveq1d ⊢ N ∈ Fin ∧ M ∈ Fin → ∑ Z ∅ ⁡ n = I ↾ M ⁡ n
113 106 112 eqeq12d ⊢ N ∈ Fin ∧ M ∈ Fin → ∑ S ∅ ⁡ n = ∑ Z ∅ ⁡ n ↔ I ↾ N ⁡ n = I ↾ M ⁡ n
114 113 ralbidv ⊢ N ∈ Fin ∧ M ∈ Fin → ∀ n ∈ I ∑ S ∅ ⁡ n = ∑ Z ∅ ⁡ n ↔ ∀ n ∈ I I ↾ N ⁡ n = I ↾ M ⁡ n
115 100 114 mpbird ⊢ N ∈ Fin ∧ M ∈ Fin → ∀ n ∈ I ∑ S ∅ ⁡ n = ∑ Z ∅ ⁡ n
116 115 a1d ⊢ N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ ∅ ∀ n ∈ I ∅ ⁡ i ⁡ n = ∅ ⁡ i ⁡ n → ∀ n ∈ I ∑ S ∅ ⁡ n = ∑ Z ∅ ⁡ n
117 1 2 3 4 5 gsmsymgreqlem2 ⊢ N ∈ Fin ∧ M ∈ Fin ∧ x ∈ Word B ∧ b ∈ B ∧ y ∈ Word P ∧ p ∈ P ∧ x = y → ∀ i ∈ 0 ..^ x ∀ n ∈ I x ⁡ i ⁡ n = y ⁡ i ⁡ n → ∀ n ∈ I ∑ S x ⁡ n = ∑ Z y ⁡ n → ∀ i ∈ 0 ..^ x ++ ⟨“ b ”⟩ ∀ n ∈ I x ++ ⟨“ b ”⟩ ⁡ i ⁡ n = y ++ ⟨“ p ”⟩ ⁡ i ⁡ n → ∀ n ∈ I ∑ S x ++ ⟨“ b ”⟩ ⁡ n = ∑ Z y ++ ⟨“ p ”⟩ ⁡ n
118 117 expcom ⊢ x ∈ Word B ∧ b ∈ B ∧ y ∈ Word P ∧ p ∈ P ∧ x = y → N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ x ∀ n ∈ I x ⁡ i ⁡ n = y ⁡ i ⁡ n → ∀ n ∈ I ∑ S x ⁡ n = ∑ Z y ⁡ n → ∀ i ∈ 0 ..^ x ++ ⟨“ b ”⟩ ∀ n ∈ I x ++ ⟨“ b ”⟩ ⁡ i ⁡ n = y ++ ⟨“ p ”⟩ ⁡ i ⁡ n → ∀ n ∈ I ∑ S x ++ ⟨“ b ”⟩ ⁡ n = ∑ Z y ++ ⟨“ p ”⟩ ⁡ n
119 118 a2d ⊢ x ∈ Word B ∧ b ∈ B ∧ y ∈ Word P ∧ p ∈ P ∧ x = y → N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ x ∀ n ∈ I x ⁡ i ⁡ n = y ⁡ i ⁡ n → ∀ n ∈ I ∑ S x ⁡ n = ∑ Z y ⁡ n → N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ x ++ ⟨“ b ”⟩ ∀ n ∈ I x ++ ⟨“ b ”⟩ ⁡ i ⁡ n = y ++ ⟨“ p ”⟩ ⁡ i ⁡ n → ∀ n ∈ I ∑ S x ++ ⟨“ b ”⟩ ⁡ n = ∑ Z y ++ ⟨“ p ”⟩ ⁡ n
120 23 41 59 72 83 116 119 wrd2ind ⊢ W ∈ Word B ∧ U ∈ Word P ∧ W = U → N ∈ Fin ∧ M ∈ Fin → ∀ i ∈ 0 ..^ W ∀ n ∈ I W ⁡ i ⁡ n = U ⁡ i ⁡ n → ∀ n ∈ I ∑ S W ⁡ n = ∑ Z U ⁡ n
121 120 impcom ⊢ N ∈ Fin ∧ M ∈ Fin ∧ W ∈ Word B ∧ U ∈ Word P ∧ W = U → ∀ i ∈ 0 ..^ W ∀ n ∈ I W ⁡ i ⁡ n = U ⁡ i ⁡ n → ∀ n ∈ I ∑ S W ⁡ n = ∑ Z U ⁡ n