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 ) ) |