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
|- ( ph -> D e. V )
psgnunilem2.w
|- ( ph -> W e. Word T )
psgnunilem2.id
|- ( ph -> ( G gsum W ) = ( _I |` D ) )
psgnunilem2.l
|- ( ph -> ( # ` W ) = L )
psgnunilem2.ix
|- ( ph -> I e. ( 0 ..^ L ) )
psgnunilem2.a
|- ( ph -> A e. dom ( ( W ` I ) \ _I ) )
psgnunilem2.al
|- ( ph -> A. k e. ( 0 ..^ I ) -. A e. dom ( ( W ` k ) \ _I ) )
Assertion psgnunilem5
|- ( ph -> ( I + 1 ) e. ( 0 ..^ L ) )

Proof

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