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 ffvelcdmd 
 |-  ( 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 ffvelcdmda 
 |-  ( ( 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 ) )