Metamath Proof Explorer


Theorem psgnunilem5

Description: Lemma for psgnuni . It is impossible to shift a transposition off the end because if the active transposition is at the right end, it is the only transposition moving A in contradiction to this being a representation of the identity. (Contributed by Stefan O'Rear, 25-Aug-2015) (Revised by Mario Carneiro, 28-Feb-2016) (Proof shortened by AV, 12-Oct-2022)

Ref Expression
Hypotheses psgnunilem2.g G = SymGrp D
psgnunilem2.t T = ran pmTrsp D
psgnunilem2.d φ D V
psgnunilem2.w φ W Word T
psgnunilem2.id φ G W = I D
psgnunilem2.l φ W = L
psgnunilem2.ix φ I 0 ..^ L
psgnunilem2.a φ A dom W I I
psgnunilem2.al φ k 0 ..^ I ¬ A dom W k I
Assertion psgnunilem5 φ I + 1 0 ..^ L

Proof

Step Hyp Ref Expression
1 psgnunilem2.g G = SymGrp D
2 psgnunilem2.t T = ran pmTrsp D
3 psgnunilem2.d φ D V
4 psgnunilem2.w φ W Word T
5 psgnunilem2.id φ G W = I D
6 psgnunilem2.l φ W = L
7 psgnunilem2.ix φ I 0 ..^ L
8 psgnunilem2.a φ A dom W I I
9 psgnunilem2.al φ k 0 ..^ I ¬ A dom W k I
10 noel ¬ A
11 5 difeq1d φ G W I = I D I
12 11 dmeqd φ dom G W I = dom I D I
13 resss I D I
14 ssdif0 I D I I D I =
15 13 14 mpbi I D I =
16 15 dmeqi dom I D I = dom
17 dm0 dom =
18 16 17 eqtri dom I D I =
19 12 18 eqtrdi φ dom G W I =
20 19 eleq2d φ A dom G W I A
21 10 20 mtbiri φ ¬ A dom G W I
22 1 symggrp D V G Grp
23 grpmnd G Grp G Mnd
24 3 22 23 3syl φ G Mnd
25 eqid Base G = Base G
26 2 1 25 symgtrf T Base G
27 sswrd T Base G Word T Word Base G
28 26 27 mp1i φ Word T Word Base G
29 28 4 sseldd φ W Word Base G
30 pfxcl W Word Base G W prefix I Word Base G
31 29 30 syl φ W prefix I Word Base G
32 25 gsumwcl G Mnd W prefix I Word Base G G W prefix I Base G
33 24 31 32 syl2anc φ G W prefix I Base G
34 1 25 symgbasf1o G W prefix I Base G G W prefix I : D 1-1 onto D
35 33 34 syl φ G W prefix I : D 1-1 onto D
36 35 adantr φ I + 1 = L G W prefix I : D 1-1 onto D
37 wrdf W Word T W : 0 ..^ W T
38 4 37 syl φ W : 0 ..^ W T
39 6 oveq2d φ 0 ..^ W = 0 ..^ L
40 7 39 eleqtrrd φ I 0 ..^ W
41 38 40 ffvelrnd φ W I T
42 26 41 sselid φ W I Base G
43 1 25 symgbasf1o W I Base G W I : D 1-1 onto D
44 42 43 syl φ W I : D 1-1 onto D
45 44 adantr φ I + 1 = L W I : D 1-1 onto D
46 1 25 symgsssg D V j Base G | dom j I V A SubGrp G
47 subgsubm j Base G | dom j I V A SubGrp G j Base G | dom j I V A SubMnd G
48 3 46 47 3syl φ j Base G | dom j I V A SubMnd G
49 fzossfz 0 ..^ L 0 L
50 49 7 sselid φ I 0 L
51 6 oveq2d φ 0 W = 0 L
52 50 51 eleqtrrd φ I 0 W
53 pfxmpt W Word T I 0 W W prefix I = s 0 ..^ I W s
54 4 52 53 syl2anc φ W prefix I = s 0 ..^ I W s
55 difeq1 j = W s j I = W s I
56 55 dmeqd j = W s dom j I = dom W s I
57 56 sseq1d j = W s dom j I V A dom W s I V A
58 disj2 dom W s I A = dom W s I V A
59 disjsn dom W s I A = ¬ A dom W s I
60 58 59 bitr3i dom W s I V A ¬ A dom W s I
61 57 60 bitrdi j = W s dom j I V A ¬ A dom W s I
62 elfzuz3 I 0 L L I
63 50 62 syl φ L I
64 6 63 eqeltrd φ W I
65 fzoss2 W I 0 ..^ I 0 ..^ W
66 64 65 syl φ 0 ..^ I 0 ..^ W
67 66 sselda φ s 0 ..^ I s 0 ..^ W
68 38 ffvelrnda φ s 0 ..^ W W s T
69 26 68 sselid φ s 0 ..^ W W s Base G
70 67 69 syldan φ s 0 ..^ I W s Base G
71 fveq2 k = s W k = W s
72 71 difeq1d k = s W k I = W s I
73 72 dmeqd k = s dom W k I = dom W s I
74 73 eleq2d k = s A dom W k I A dom W s I
75 74 notbid k = s ¬ A dom W k I ¬ A dom W s I
76 75 cbvralvw k 0 ..^ I ¬ A dom W k I s 0 ..^ I ¬ A dom W s I
77 9 76 sylib φ s 0 ..^ I ¬ A dom W s I
78 77 r19.21bi φ s 0 ..^ I ¬ A dom W s I
79 61 70 78 elrabd φ s 0 ..^ I W s j Base G | dom j I V A
80 54 79 fmpt3d φ W prefix I : 0 ..^ I j Base G | dom j I V A
81 80 adantr φ I + 1 = L W prefix I : 0 ..^ I j Base G | dom j I V A
82 iswrdi W prefix I : 0 ..^ I j Base G | dom j I V A W prefix I Word j Base G | dom j I V A
83 81 82 syl φ I + 1 = L W prefix I Word j Base G | dom j I V A
84 gsumwsubmcl j Base G | dom j I V A SubMnd G W prefix I Word j Base G | dom j I V A G W prefix I j Base G | dom j I V A
85 48 83 84 syl2an2r φ I + 1 = L G W prefix I j Base G | dom j I V A
86 difeq1 j = G W prefix I j I = G W prefix I I
87 86 dmeqd j = G W prefix I dom j I = dom G W prefix I I
88 87 sseq1d j = G W prefix I dom j I V A dom G W prefix I I V A
89 88 elrab G W prefix I j Base G | dom j I V A G W prefix I Base G dom G W prefix I I V A
90 89 simprbi G W prefix I j Base G | dom j I V A dom G W prefix I I V A
91 disj2 dom G W prefix I I A = dom G W prefix I I V A
92 disjsn dom G W prefix I I A = ¬ A dom G W prefix I I
93 91 92 bitr3i dom G W prefix I I V A ¬ A dom G W prefix I I
94 90 93 sylib G W prefix I j Base G | dom j I V A ¬ A dom G W prefix I I
95 85 94 syl φ I + 1 = L ¬ A dom G W prefix I I
96 8 adantr φ I + 1 = L A dom W I I
97 95 96 jca φ I + 1 = L ¬ A dom G W prefix I I A dom W I I
98 97 olcd φ I + 1 = L A dom G W prefix I I ¬ A dom W I I ¬ A dom G W prefix I I A dom W I I
99 excxor A dom G W prefix I I A dom W I I A dom G W prefix I I ¬ A dom W I I ¬ A dom G W prefix I I A dom W I I
100 98 99 sylibr φ I + 1 = L A dom G W prefix I I A dom W I I
101 f1omvdco3 G W prefix I : D 1-1 onto D W I : D 1-1 onto D A dom G W prefix I I A dom W I I A dom G W prefix I W I I
102 36 45 100 101 syl3anc φ I + 1 = L A dom G W prefix I W I I
103 elfzo0 I 0 ..^ L I 0 L I < L
104 103 simp2bi I 0 ..^ L L
105 7 104 syl φ L
106 6 105 eqeltrd φ W
107 wrdfin W Word T W Fin
108 hashnncl W Fin W W
109 4 107 108 3syl φ W W
110 106 109 mpbid φ W
111 110 adantr φ I + 1 = L W
112 pfxlswccat W Word T W W prefix W 1 ++ ⟨“ lastS W ”⟩ = W
113 112 eqcomd W Word T W W = W prefix W 1 ++ ⟨“ lastS W ”⟩
114 4 111 113 syl2an2r φ I + 1 = L W = W prefix W 1 ++ ⟨“ lastS W ”⟩
115 6 oveq1d φ W 1 = L 1
116 115 adantr φ I + 1 = L W 1 = L 1
117 105 nncnd φ L
118 1cnd φ 1
119 elfzoelz I 0 ..^ L I
120 7 119 syl φ I
121 120 zcnd φ I
122 117 118 121 subadd2d φ L 1 = I I + 1 = L
123 122 biimpar φ I + 1 = L L 1 = I
124 116 123 eqtrd φ I + 1 = L W 1 = I
125 oveq2 W 1 = I W prefix W 1 = W prefix I
126 125 adantl φ W 1 = I W prefix W 1 = W prefix I
127 lsw W Word T lastS W = W W 1
128 4 127 syl φ lastS W = W W 1
129 fveq2 W 1 = I W W 1 = W I
130 128 129 sylan9eq φ W 1 = I lastS W = W I
131 130 s1eqd φ W 1 = I ⟨“ lastS W ”⟩ = ⟨“ W I ”⟩
132 126 131 oveq12d φ W 1 = I W prefix W 1 ++ ⟨“ lastS W ”⟩ = W prefix I ++ ⟨“ W I ”⟩
133 124 132 syldan φ I + 1 = L W prefix W 1 ++ ⟨“ lastS W ”⟩ = W prefix I ++ ⟨“ W I ”⟩
134 114 133 eqtrd φ I + 1 = L W = W prefix I ++ ⟨“ W I ”⟩
135 134 oveq2d φ I + 1 = L G W = G W prefix I ++ ⟨“ W I ”⟩
136 42 s1cld φ ⟨“ W I ”⟩ Word Base G
137 eqid + G = + G
138 25 137 gsumccat G Mnd W prefix I Word Base G ⟨“ W I ”⟩ Word Base G G W prefix I ++ ⟨“ W I ”⟩ = G W prefix I + G G ⟨“ W I ”⟩
139 24 31 136 138 syl3anc φ G W prefix I ++ ⟨“ W I ”⟩ = G W prefix I + G G ⟨“ W I ”⟩
140 139 adantr φ I + 1 = L G W prefix I ++ ⟨“ W I ”⟩ = G W prefix I + G G ⟨“ W I ”⟩
141 25 gsumws1 W I Base G G ⟨“ W I ”⟩ = W I
142 42 141 syl φ G ⟨“ W I ”⟩ = W I
143 142 oveq2d φ G W prefix I + G G ⟨“ W I ”⟩ = G W prefix I + G W I
144 1 25 137 symgov G W prefix I Base G W I Base G G W prefix I + G W I = G W prefix I W I
145 33 42 144 syl2anc φ G W prefix I + G W I = G W prefix I W I
146 143 145 eqtrd φ G W prefix I + G G ⟨“ W I ”⟩ = G W prefix I W I
147 146 adantr φ I + 1 = L G W prefix I + G G ⟨“ W I ”⟩ = G W prefix I W I
148 135 140 147 3eqtrd φ I + 1 = L G W = G W prefix I W I
149 148 difeq1d φ I + 1 = L G W I = G W prefix I W I I
150 149 dmeqd φ I + 1 = L dom G W I = dom G W prefix I W I I
151 102 150 eleqtrrd φ I + 1 = L A dom G W I
152 21 151 mtand φ ¬ I + 1 = L
153 fzostep1 I 0 ..^ L I + 1 0 ..^ L I + 1 = L
154 7 153 syl φ I + 1 0 ..^ L I + 1 = L
155 154 ord φ ¬ I + 1 0 ..^ L I + 1 = L
156 152 155 mt3d φ I + 1 0 ..^ L