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 ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgnunilem2.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
psgnunilem2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
psgnunilem2.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑇 )
psgnunilem2.id ⊢ ( 𝜑 → ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) )
psgnunilem2.l ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = 𝐿 )
psgnunilem2.ix ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝐿 ) )
psgnunilem2.a ⊢ ( 𝜑 → 𝐴 ∈ dom ( ( 𝑊 ‘ 𝐼 ) ∖ I ) )
psgnunilem2.al ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝐼 ) ¬ 𝐴 ∈ dom ( ( 𝑊 ‘ 𝑘 ) ∖ I ) )
Assertion psgnunilem5 ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝐿 ) )

Proof

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