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 syl6bi 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 syl6bi 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