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=BaseS
gsmsymgreq.z ⊢Z=SymGrp⁡M
gsmsymgreq.p ⊢P=BaseZ
gsmsymgreq.i ⊢I=N∩M
Assertion gsmsymgreq ⊢N∈Fin∧M∈Fin∧W∈WordB∧U∈WordP∧W=U→∀i∈0..^W∀n∈IW⁡i⁡n=U⁡i⁡n→∀n∈I∑SW⁡n=∑ZU⁡n

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s ⊢S=SymGrp⁡N
2 gsmsymgrfix.b ⊢B=BaseS
3 gsmsymgreq.z ⊢Z=SymGrp⁡M
4 gsmsymgreq.p ⊢P=BaseZ
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∈Iw⁡i⁡n=u⁡i⁡n↔∀n∈I∅⁡i⁡n=∅⁡i⁡n
15 8 14 raleqbidv ⊢w=∅∧u=∅→∀i∈0..^w∀n∈Iw⁡i⁡n=u⁡i⁡n↔∀i∈0..^∅∀n∈I∅⁡i⁡n=∅⁡i⁡n
16 oveq2 ⊢w=∅→∑Sw=∑S∅
17 16 fveq1d ⊢w=∅→∑Sw⁡n=∑S∅⁡n
18 oveq2 ⊢u=∅→∑Zu=∑Z∅
19 18 fveq1d ⊢u=∅→∑Zu⁡n=∑Z∅⁡n
20 17 19 eqeqan12d ⊢w=∅∧u=∅→∑Sw⁡n=∑Zu⁡n↔∑S∅⁡n=∑Z∅⁡n
21 20 ralbidv ⊢w=∅∧u=∅→∀n∈I∑Sw⁡n=∑Zu⁡n↔∀n∈I∑S∅⁡n=∑Z∅⁡n
22 15 21 imbi12d ⊢w=∅∧u=∅→∀i∈0..^w∀n∈Iw⁡i⁡n=u⁡i⁡n→∀n∈I∑Sw⁡n=∑Zu⁡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∈Iw⁡i⁡n=u⁡i⁡n→∀n∈I∑Sw⁡n=∑Zu⁡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∈Iw⁡i⁡n=u⁡i⁡n↔∀n∈Ix⁡i⁡n=y⁡i⁡n
33 26 32 raleqbidv ⊢w=x∧u=y→∀i∈0..^w∀n∈Iw⁡i⁡n=u⁡i⁡n↔∀i∈0..^x∀n∈Ix⁡i⁡n=y⁡i⁡n
34 oveq2 ⊢w=x→∑Sw=∑Sx
35 34 fveq1d ⊢w=x→∑Sw⁡n=∑Sx⁡n
36 oveq2 ⊢u=y→∑Zu=∑Zy
37 36 fveq1d ⊢u=y→∑Zu⁡n=∑Zy⁡n
38 35 37 eqeqan12d ⊢w=x∧u=y→∑Sw⁡n=∑Zu⁡n↔∑Sx⁡n=∑Zy⁡n
39 38 ralbidv ⊢w=x∧u=y→∀n∈I∑Sw⁡n=∑Zu⁡n↔∀n∈I∑Sx⁡n=∑Zy⁡n
40 33 39 imbi12d ⊢w=x∧u=y→∀i∈0..^w∀n∈Iw⁡i⁡n=u⁡i⁡n→∀n∈I∑Sw⁡n=∑Zu⁡n↔∀i∈0..^x∀n∈Ix⁡i⁡n=y⁡i⁡n→∀n∈I∑Sx⁡n=∑Zy⁡n
41 40 imbi2d ⊢w=x∧u=y→N∈Fin∧M∈Fin→∀i∈0..^w∀n∈Iw⁡i⁡n=u⁡i⁡n→∀n∈I∑Sw⁡n=∑Zu⁡n↔N∈Fin∧M∈Fin→∀i∈0..^x∀n∈Ix⁡i⁡n=y⁡i⁡n→∀n∈I∑Sx⁡n=∑Zy⁡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∈Iw⁡i⁡n=u⁡i⁡n↔∀n∈Ix++⟨“b”⟩⁡i⁡n=y++⟨“p”⟩⁡i⁡n
51 44 50 raleqbidv ⊢w=x++⟨“b”⟩∧u=y++⟨“p”⟩→∀i∈0..^w∀n∈Iw⁡i⁡n=u⁡i⁡n↔∀i∈0..^x++⟨“b”⟩∀n∈Ix++⟨“b”⟩⁡i⁡n=y++⟨“p”⟩⁡i⁡n
52 oveq2 ⊢w=x++⟨“b”⟩→∑Sw=∑Sx++⟨“b”⟩
53 52 fveq1d ⊢w=x++⟨“b”⟩→∑Sw⁡n=∑Sx++⟨“b”⟩⁡n
54 oveq2 ⊢u=y++⟨“p”⟩→∑Zu=∑Zy++⟨“p”⟩
55 54 fveq1d ⊢u=y++⟨“p”⟩→∑Zu⁡n=∑Zy++⟨“p”⟩⁡n
56 53 55 eqeqan12d ⊢w=x++⟨“b”⟩∧u=y++⟨“p”⟩→∑Sw⁡n=∑Zu⁡n↔∑Sx++⟨“b”⟩⁡n=∑Zy++⟨“p”⟩⁡n
57 56 ralbidv ⊢w=x++⟨“b”⟩∧u=y++⟨“p”⟩→∀n∈I∑Sw⁡n=∑Zu⁡n↔∀n∈I∑Sx++⟨“b”⟩⁡n=∑Zy++⟨“p”⟩⁡n
58 51 57 imbi12d ⊢w=x++⟨“b”⟩∧u=y++⟨“p”⟩→∀i∈0..^w∀n∈Iw⁡i⁡n=u⁡i⁡n→∀n∈I∑Sw⁡n=∑Zu⁡n↔∀i∈0..^x++⟨“b”⟩∀n∈Ix++⟨“b”⟩⁡i⁡n=y++⟨“p”⟩⁡i⁡n→∀n∈I∑Sx++⟨“b”⟩⁡n=∑Zy++⟨“p”⟩⁡n
59 58 imbi2d ⊢w=x++⟨“b”⟩∧u=y++⟨“p”⟩→N∈Fin∧M∈Fin→∀i∈0..^w∀n∈Iw⁡i⁡n=u⁡i⁡n→∀n∈I∑Sw⁡n=∑Zu⁡n↔N∈Fin∧M∈Fin→∀i∈0..^x++⟨“b”⟩∀n∈Ix++⟨“b”⟩⁡i⁡n=y++⟨“p”⟩⁡i⁡n→∀n∈I∑Sx++⟨“b”⟩⁡n=∑Zy++⟨“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∈Iw⁡i⁡n=U⁡i⁡n↔∀n∈IW⁡i⁡n=U⁡i⁡n
66 61 65 raleqbidv ⊢w=W→∀i∈0..^w∀n∈Iw⁡i⁡n=U⁡i⁡n↔∀i∈0..^W∀n∈IW⁡i⁡n=U⁡i⁡n
67 oveq2 ⊢w=W→∑Sw=∑SW
68 67 fveq1d ⊢w=W→∑Sw⁡n=∑SW⁡n
69 68 eqeq1d ⊢w=W→∑Sw⁡n=∑ZU⁡n↔∑SW⁡n=∑ZU⁡n
70 69 ralbidv ⊢w=W→∀n∈I∑Sw⁡n=∑ZU⁡n↔∀n∈I∑SW⁡n=∑ZU⁡n
71 66 70 imbi12d ⊢w=W→∀i∈0..^w∀n∈Iw⁡i⁡n=U⁡i⁡n→∀n∈I∑Sw⁡n=∑ZU⁡n↔∀i∈0..^W∀n∈IW⁡i⁡n=U⁡i⁡n→∀n∈I∑SW⁡n=∑ZU⁡n
72 71 imbi2d ⊢w=W→N∈Fin∧M∈Fin→∀i∈0..^w∀n∈Iw⁡i⁡n=U⁡i⁡n→∀n∈I∑Sw⁡n=∑ZU⁡n↔N∈Fin∧M∈Fin→∀i∈0..^W∀n∈IW⁡i⁡n=U⁡i⁡n→∀n∈I∑SW⁡n=∑ZU⁡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∈Iw⁡i⁡n=u⁡i⁡n↔∀n∈Iw⁡i⁡n=U⁡i⁡n
77 76 ralbidv ⊢u=U→∀i∈0..^w∀n∈Iw⁡i⁡n=u⁡i⁡n↔∀i∈0..^w∀n∈Iw⁡i⁡n=U⁡i⁡n
78 oveq2 ⊢u=U→∑Zu=∑ZU
79 78 fveq1d ⊢u=U→∑Zu⁡n=∑ZU⁡n
80 79 eqeq2d ⊢u=U→∑Sw⁡n=∑Zu⁡n↔∑Sw⁡n=∑ZU⁡n
81 80 ralbidv ⊢u=U→∀n∈I∑Sw⁡n=∑Zu⁡n↔∀n∈I∑Sw⁡n=∑ZU⁡n
82 77 81 imbi12d ⊢u=U→∀i∈0..^w∀n∈Iw⁡i⁡n=u⁡i⁡n→∀n∈I∑Sw⁡n=∑Zu⁡n↔∀i∈0..^w∀n∈Iw⁡i⁡n=U⁡i⁡n→∀n∈I∑Sw⁡n=∑ZU⁡n
83 82 imbi2d ⊢u=U→N∈Fin∧M∈Fin→∀i∈0..^w∀n∈Iw⁡i⁡n=u⁡i⁡n→∀n∈I∑Sw⁡n=∑Zu⁡n↔N∈Fin∧M∈Fin→∀i∈0..^w∀n∈Iw⁡i⁡n=U⁡i⁡n→∀n∈I∑Sw⁡n=∑ZU⁡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∈II↾N⁡n=I↾M⁡n
101 eqid ⊢0S=0S
102 101 gsum0 ⊢∑S∅=0S
103 1 symgid ⊢N∈Fin→I↾N=0S
104 103 adantr ⊢N∈Fin∧M∈Fin→I↾N=0S
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 ⊢0Z=0Z
108 107 gsum0 ⊢∑Z∅=0Z
109 3 symgid ⊢M∈Fin→I↾M=0Z
110 109 adantl ⊢N∈Fin∧M∈Fin→I↾M=0Z
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∈II↾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∈WordB∧b∈B∧y∈WordP∧p∈P∧x=y→∀i∈0..^x∀n∈Ix⁡i⁡n=y⁡i⁡n→∀n∈I∑Sx⁡n=∑Zy⁡n→∀i∈0..^x++⟨“b”⟩∀n∈Ix++⟨“b”⟩⁡i⁡n=y++⟨“p”⟩⁡i⁡n→∀n∈I∑Sx++⟨“b”⟩⁡n=∑Zy++⟨“p”⟩⁡n
118 117 expcom ⊢x∈WordB∧b∈B∧y∈WordP∧p∈P∧x=y→N∈Fin∧M∈Fin→∀i∈0..^x∀n∈Ix⁡i⁡n=y⁡i⁡n→∀n∈I∑Sx⁡n=∑Zy⁡n→∀i∈0..^x++⟨“b”⟩∀n∈Ix++⟨“b”⟩⁡i⁡n=y++⟨“p”⟩⁡i⁡n→∀n∈I∑Sx++⟨“b”⟩⁡n=∑Zy++⟨“p”⟩⁡n
119 118 a2d ⊢x∈WordB∧b∈B∧y∈WordP∧p∈P∧x=y→N∈Fin∧M∈Fin→∀i∈0..^x∀n∈Ix⁡i⁡n=y⁡i⁡n→∀n∈I∑Sx⁡n=∑Zy⁡n→N∈Fin∧M∈Fin→∀i∈0..^x++⟨“b”⟩∀n∈Ix++⟨“b”⟩⁡i⁡n=y++⟨“p”⟩⁡i⁡n→∀n∈I∑Sx++⟨“b”⟩⁡n=∑Zy++⟨“p”⟩⁡n
120 23 41 59 72 83 116 119 wrd2ind ⊢W∈WordB∧U∈WordP∧W=U→N∈Fin∧M∈Fin→∀i∈0..^W∀n∈IW⁡i⁡n=U⁡i⁡n→∀n∈I∑SW⁡n=∑ZU⁡n
121 120 impcom ⊢N∈Fin∧M∈Fin∧W∈WordB∧U∈WordP∧W=U→∀i∈0..^W∀n∈IW⁡i⁡n=U⁡i⁡n→∀n∈I∑SW⁡n=∑ZU⁡n