Step |
Hyp |
Ref |
Expression |
1 |
|
mplsubglem.s |
|- S = ( I mPwSer R ) |
2 |
|
mplsubglem.b |
|- B = ( Base ` S ) |
3 |
|
mplsubglem.z |
|- .0. = ( 0g ` R ) |
4 |
|
mplsubglem.d |
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
5 |
|
mplsubglem.i |
|- ( ph -> I e. W ) |
6 |
|
mplsubglem.0 |
|- ( ph -> (/) e. A ) |
7 |
|
mplsubglem.a |
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x u. y ) e. A ) |
8 |
|
mplsubglem.y |
|- ( ( ph /\ ( x e. A /\ y C_ x ) ) -> y e. A ) |
9 |
|
mplsubglem.u |
|- ( ph -> U = { g e. B | ( g supp .0. ) e. A } ) |
10 |
|
mplsubglem.r |
|- ( ph -> R e. Grp ) |
11 |
|
ssrab2 |
|- { g e. B | ( g supp .0. ) e. A } C_ B |
12 |
9 11
|
eqsstrdi |
|- ( ph -> U C_ B ) |
13 |
1 5 10 4 3 2
|
psr0cl |
|- ( ph -> ( D X. { .0. } ) e. B ) |
14 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
15 |
14 3
|
grpidcl |
|- ( R e. Grp -> .0. e. ( Base ` R ) ) |
16 |
|
fconst6g |
|- ( .0. e. ( Base ` R ) -> ( D X. { .0. } ) : D --> ( Base ` R ) ) |
17 |
10 15 16
|
3syl |
|- ( ph -> ( D X. { .0. } ) : D --> ( Base ` R ) ) |
18 |
|
eldifi |
|- ( u e. ( D \ (/) ) -> u e. D ) |
19 |
3
|
fvexi |
|- .0. e. _V |
20 |
19
|
fvconst2 |
|- ( u e. D -> ( ( D X. { .0. } ) ` u ) = .0. ) |
21 |
18 20
|
syl |
|- ( u e. ( D \ (/) ) -> ( ( D X. { .0. } ) ` u ) = .0. ) |
22 |
21
|
adantl |
|- ( ( ph /\ u e. ( D \ (/) ) ) -> ( ( D X. { .0. } ) ` u ) = .0. ) |
23 |
17 22
|
suppss |
|- ( ph -> ( ( D X. { .0. } ) supp .0. ) C_ (/) ) |
24 |
|
ss0 |
|- ( ( ( D X. { .0. } ) supp .0. ) C_ (/) -> ( ( D X. { .0. } ) supp .0. ) = (/) ) |
25 |
23 24
|
syl |
|- ( ph -> ( ( D X. { .0. } ) supp .0. ) = (/) ) |
26 |
25 6
|
eqeltrd |
|- ( ph -> ( ( D X. { .0. } ) supp .0. ) e. A ) |
27 |
9
|
eleq2d |
|- ( ph -> ( ( D X. { .0. } ) e. U <-> ( D X. { .0. } ) e. { g e. B | ( g supp .0. ) e. A } ) ) |
28 |
|
oveq1 |
|- ( g = ( D X. { .0. } ) -> ( g supp .0. ) = ( ( D X. { .0. } ) supp .0. ) ) |
29 |
28
|
eleq1d |
|- ( g = ( D X. { .0. } ) -> ( ( g supp .0. ) e. A <-> ( ( D X. { .0. } ) supp .0. ) e. A ) ) |
30 |
29
|
elrab |
|- ( ( D X. { .0. } ) e. { g e. B | ( g supp .0. ) e. A } <-> ( ( D X. { .0. } ) e. B /\ ( ( D X. { .0. } ) supp .0. ) e. A ) ) |
31 |
27 30
|
bitrdi |
|- ( ph -> ( ( D X. { .0. } ) e. U <-> ( ( D X. { .0. } ) e. B /\ ( ( D X. { .0. } ) supp .0. ) e. A ) ) ) |
32 |
13 26 31
|
mpbir2and |
|- ( ph -> ( D X. { .0. } ) e. U ) |
33 |
32
|
ne0d |
|- ( ph -> U =/= (/) ) |
34 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
35 |
10
|
grpmgmd |
|- ( ph -> R e. Mgm ) |
36 |
35
|
ad2antrr |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> R e. Mgm ) |
37 |
9
|
eleq2d |
|- ( ph -> ( u e. U <-> u e. { g e. B | ( g supp .0. ) e. A } ) ) |
38 |
|
oveq1 |
|- ( g = u -> ( g supp .0. ) = ( u supp .0. ) ) |
39 |
38
|
eleq1d |
|- ( g = u -> ( ( g supp .0. ) e. A <-> ( u supp .0. ) e. A ) ) |
40 |
39
|
elrab |
|- ( u e. { g e. B | ( g supp .0. ) e. A } <-> ( u e. B /\ ( u supp .0. ) e. A ) ) |
41 |
37 40
|
bitrdi |
|- ( ph -> ( u e. U <-> ( u e. B /\ ( u supp .0. ) e. A ) ) ) |
42 |
41
|
biimpa |
|- ( ( ph /\ u e. U ) -> ( u e. B /\ ( u supp .0. ) e. A ) ) |
43 |
42
|
simpld |
|- ( ( ph /\ u e. U ) -> u e. B ) |
44 |
43
|
adantr |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> u e. B ) |
45 |
9
|
adantr |
|- ( ( ph /\ u e. U ) -> U = { g e. B | ( g supp .0. ) e. A } ) |
46 |
45
|
eleq2d |
|- ( ( ph /\ u e. U ) -> ( v e. U <-> v e. { g e. B | ( g supp .0. ) e. A } ) ) |
47 |
|
oveq1 |
|- ( g = v -> ( g supp .0. ) = ( v supp .0. ) ) |
48 |
47
|
eleq1d |
|- ( g = v -> ( ( g supp .0. ) e. A <-> ( v supp .0. ) e. A ) ) |
49 |
48
|
elrab |
|- ( v e. { g e. B | ( g supp .0. ) e. A } <-> ( v e. B /\ ( v supp .0. ) e. A ) ) |
50 |
46 49
|
bitrdi |
|- ( ( ph /\ u e. U ) -> ( v e. U <-> ( v e. B /\ ( v supp .0. ) e. A ) ) ) |
51 |
50
|
biimpa |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( v e. B /\ ( v supp .0. ) e. A ) ) |
52 |
51
|
simpld |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> v e. B ) |
53 |
1 2 34 36 44 52
|
psraddcl |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u ( +g ` S ) v ) e. B ) |
54 |
|
ovexd |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) supp .0. ) e. _V ) |
55 |
|
sseq2 |
|- ( x = ( ( u supp .0. ) u. ( v supp .0. ) ) -> ( y C_ x <-> y C_ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) |
56 |
55
|
imbi1d |
|- ( x = ( ( u supp .0. ) u. ( v supp .0. ) ) -> ( ( y C_ x -> y e. A ) <-> ( y C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> y e. A ) ) ) |
57 |
56
|
albidv |
|- ( x = ( ( u supp .0. ) u. ( v supp .0. ) ) -> ( A. y ( y C_ x -> y e. A ) <-> A. y ( y C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> y e. A ) ) ) |
58 |
8
|
expr |
|- ( ( ph /\ x e. A ) -> ( y C_ x -> y e. A ) ) |
59 |
58
|
alrimiv |
|- ( ( ph /\ x e. A ) -> A. y ( y C_ x -> y e. A ) ) |
60 |
59
|
ralrimiva |
|- ( ph -> A. x e. A A. y ( y C_ x -> y e. A ) ) |
61 |
60
|
ad2antrr |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> A. x e. A A. y ( y C_ x -> y e. A ) ) |
62 |
42
|
simprd |
|- ( ( ph /\ u e. U ) -> ( u supp .0. ) e. A ) |
63 |
62
|
adantr |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u supp .0. ) e. A ) |
64 |
51
|
simprd |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( v supp .0. ) e. A ) |
65 |
7
|
ralrimivva |
|- ( ph -> A. x e. A A. y e. A ( x u. y ) e. A ) |
66 |
65
|
ad2antrr |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> A. x e. A A. y e. A ( x u. y ) e. A ) |
67 |
|
uneq1 |
|- ( x = ( u supp .0. ) -> ( x u. y ) = ( ( u supp .0. ) u. y ) ) |
68 |
67
|
eleq1d |
|- ( x = ( u supp .0. ) -> ( ( x u. y ) e. A <-> ( ( u supp .0. ) u. y ) e. A ) ) |
69 |
|
uneq2 |
|- ( y = ( v supp .0. ) -> ( ( u supp .0. ) u. y ) = ( ( u supp .0. ) u. ( v supp .0. ) ) ) |
70 |
69
|
eleq1d |
|- ( y = ( v supp .0. ) -> ( ( ( u supp .0. ) u. y ) e. A <-> ( ( u supp .0. ) u. ( v supp .0. ) ) e. A ) ) |
71 |
68 70
|
rspc2va |
|- ( ( ( ( u supp .0. ) e. A /\ ( v supp .0. ) e. A ) /\ A. x e. A A. y e. A ( x u. y ) e. A ) -> ( ( u supp .0. ) u. ( v supp .0. ) ) e. A ) |
72 |
63 64 66 71
|
syl21anc |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u supp .0. ) u. ( v supp .0. ) ) e. A ) |
73 |
57 61 72
|
rspcdva |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> A. y ( y C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> y e. A ) ) |
74 |
1 14 4 2 53
|
psrelbas |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u ( +g ` S ) v ) : D --> ( Base ` R ) ) |
75 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
76 |
1 2 75 34 44 52
|
psradd |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u ( +g ` S ) v ) = ( u oF ( +g ` R ) v ) ) |
77 |
76
|
fveq1d |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) ` k ) = ( ( u oF ( +g ` R ) v ) ` k ) ) |
78 |
77
|
adantr |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( ( u ( +g ` S ) v ) ` k ) = ( ( u oF ( +g ` R ) v ) ` k ) ) |
79 |
|
eldifi |
|- ( k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) -> k e. D ) |
80 |
1 14 4 2 43
|
psrelbas |
|- ( ( ph /\ u e. U ) -> u : D --> ( Base ` R ) ) |
81 |
80
|
adantr |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> u : D --> ( Base ` R ) ) |
82 |
81
|
ffnd |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> u Fn D ) |
83 |
1 14 4 2 52
|
psrelbas |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> v : D --> ( Base ` R ) ) |
84 |
83
|
ffnd |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> v Fn D ) |
85 |
|
ovex |
|- ( NN0 ^m I ) e. _V |
86 |
4 85
|
rabex2 |
|- D e. _V |
87 |
86
|
a1i |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> D e. _V ) |
88 |
|
inidm |
|- ( D i^i D ) = D |
89 |
|
eqidd |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. D ) -> ( u ` k ) = ( u ` k ) ) |
90 |
|
eqidd |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. D ) -> ( v ` k ) = ( v ` k ) ) |
91 |
82 84 87 87 88 89 90
|
ofval |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. D ) -> ( ( u oF ( +g ` R ) v ) ` k ) = ( ( u ` k ) ( +g ` R ) ( v ` k ) ) ) |
92 |
79 91
|
sylan2 |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( ( u oF ( +g ` R ) v ) ` k ) = ( ( u ` k ) ( +g ` R ) ( v ` k ) ) ) |
93 |
|
ssun1 |
|- ( u supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) ) |
94 |
|
sscon |
|- ( ( u supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) C_ ( D \ ( u supp .0. ) ) ) |
95 |
93 94
|
ax-mp |
|- ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) C_ ( D \ ( u supp .0. ) ) |
96 |
95
|
sseli |
|- ( k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) -> k e. ( D \ ( u supp .0. ) ) ) |
97 |
|
ssidd |
|- ( ( ph /\ u e. U ) -> ( u supp .0. ) C_ ( u supp .0. ) ) |
98 |
86
|
a1i |
|- ( ( ph /\ u e. U ) -> D e. _V ) |
99 |
19
|
a1i |
|- ( ( ph /\ u e. U ) -> .0. e. _V ) |
100 |
80 97 98 99
|
suppssr |
|- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( u supp .0. ) ) ) -> ( u ` k ) = .0. ) |
101 |
100
|
adantlr |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( u supp .0. ) ) ) -> ( u ` k ) = .0. ) |
102 |
96 101
|
sylan2 |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( u ` k ) = .0. ) |
103 |
|
ssun2 |
|- ( v supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) ) |
104 |
|
sscon |
|- ( ( v supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) C_ ( D \ ( v supp .0. ) ) ) |
105 |
103 104
|
ax-mp |
|- ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) C_ ( D \ ( v supp .0. ) ) |
106 |
105
|
sseli |
|- ( k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) -> k e. ( D \ ( v supp .0. ) ) ) |
107 |
|
ssidd |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( v supp .0. ) C_ ( v supp .0. ) ) |
108 |
19
|
a1i |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> .0. e. _V ) |
109 |
83 107 87 108
|
suppssr |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( v supp .0. ) ) ) -> ( v ` k ) = .0. ) |
110 |
106 109
|
sylan2 |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( v ` k ) = .0. ) |
111 |
102 110
|
oveq12d |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( ( u ` k ) ( +g ` R ) ( v ` k ) ) = ( .0. ( +g ` R ) .0. ) ) |
112 |
10
|
ad2antrr |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> R e. Grp ) |
113 |
14 75 3
|
grplid |
|- ( ( R e. Grp /\ .0. e. ( Base ` R ) ) -> ( .0. ( +g ` R ) .0. ) = .0. ) |
114 |
112 15 113
|
syl2anc2 |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( .0. ( +g ` R ) .0. ) = .0. ) |
115 |
114
|
adantr |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( .0. ( +g ` R ) .0. ) = .0. ) |
116 |
111 115
|
eqtrd |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( ( u ` k ) ( +g ` R ) ( v ` k ) ) = .0. ) |
117 |
78 92 116
|
3eqtrd |
|- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( ( u ( +g ` S ) v ) ` k ) = .0. ) |
118 |
74 117
|
suppss |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) ) ) |
119 |
|
sseq1 |
|- ( y = ( ( u ( +g ` S ) v ) supp .0. ) -> ( y C_ ( ( u supp .0. ) u. ( v supp .0. ) ) <-> ( ( u ( +g ` S ) v ) supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) |
120 |
|
eleq1 |
|- ( y = ( ( u ( +g ` S ) v ) supp .0. ) -> ( y e. A <-> ( ( u ( +g ` S ) v ) supp .0. ) e. A ) ) |
121 |
119 120
|
imbi12d |
|- ( y = ( ( u ( +g ` S ) v ) supp .0. ) -> ( ( y C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> y e. A ) <-> ( ( ( u ( +g ` S ) v ) supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> ( ( u ( +g ` S ) v ) supp .0. ) e. A ) ) ) |
122 |
121
|
spcgv |
|- ( ( ( u ( +g ` S ) v ) supp .0. ) e. _V -> ( A. y ( y C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> y e. A ) -> ( ( ( u ( +g ` S ) v ) supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> ( ( u ( +g ` S ) v ) supp .0. ) e. A ) ) ) |
123 |
54 73 118 122
|
syl3c |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) supp .0. ) e. A ) |
124 |
9
|
ad2antrr |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> U = { g e. B | ( g supp .0. ) e. A } ) |
125 |
124
|
eleq2d |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) e. U <-> ( u ( +g ` S ) v ) e. { g e. B | ( g supp .0. ) e. A } ) ) |
126 |
|
oveq1 |
|- ( g = ( u ( +g ` S ) v ) -> ( g supp .0. ) = ( ( u ( +g ` S ) v ) supp .0. ) ) |
127 |
126
|
eleq1d |
|- ( g = ( u ( +g ` S ) v ) -> ( ( g supp .0. ) e. A <-> ( ( u ( +g ` S ) v ) supp .0. ) e. A ) ) |
128 |
127
|
elrab |
|- ( ( u ( +g ` S ) v ) e. { g e. B | ( g supp .0. ) e. A } <-> ( ( u ( +g ` S ) v ) e. B /\ ( ( u ( +g ` S ) v ) supp .0. ) e. A ) ) |
129 |
125 128
|
bitrdi |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) e. U <-> ( ( u ( +g ` S ) v ) e. B /\ ( ( u ( +g ` S ) v ) supp .0. ) e. A ) ) ) |
130 |
53 123 129
|
mpbir2and |
|- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u ( +g ` S ) v ) e. U ) |
131 |
130
|
ralrimiva |
|- ( ( ph /\ u e. U ) -> A. v e. U ( u ( +g ` S ) v ) e. U ) |
132 |
1 5 10
|
psrgrp |
|- ( ph -> S e. Grp ) |
133 |
|
eqid |
|- ( invg ` S ) = ( invg ` S ) |
134 |
2 133
|
grpinvcl |
|- ( ( S e. Grp /\ u e. B ) -> ( ( invg ` S ) ` u ) e. B ) |
135 |
132 43 134
|
syl2an2r |
|- ( ( ph /\ u e. U ) -> ( ( invg ` S ) ` u ) e. B ) |
136 |
|
ovexd |
|- ( ( ph /\ u e. U ) -> ( ( ( invg ` S ) ` u ) supp .0. ) e. _V ) |
137 |
|
sseq2 |
|- ( x = ( u supp .0. ) -> ( y C_ x <-> y C_ ( u supp .0. ) ) ) |
138 |
137
|
imbi1d |
|- ( x = ( u supp .0. ) -> ( ( y C_ x -> y e. A ) <-> ( y C_ ( u supp .0. ) -> y e. A ) ) ) |
139 |
138
|
albidv |
|- ( x = ( u supp .0. ) -> ( A. y ( y C_ x -> y e. A ) <-> A. y ( y C_ ( u supp .0. ) -> y e. A ) ) ) |
140 |
60
|
adantr |
|- ( ( ph /\ u e. U ) -> A. x e. A A. y ( y C_ x -> y e. A ) ) |
141 |
139 140 62
|
rspcdva |
|- ( ( ph /\ u e. U ) -> A. y ( y C_ ( u supp .0. ) -> y e. A ) ) |
142 |
5
|
adantr |
|- ( ( ph /\ u e. U ) -> I e. W ) |
143 |
10
|
adantr |
|- ( ( ph /\ u e. U ) -> R e. Grp ) |
144 |
|
eqid |
|- ( invg ` R ) = ( invg ` R ) |
145 |
1 142 143 4 144 2 133 43
|
psrneg |
|- ( ( ph /\ u e. U ) -> ( ( invg ` S ) ` u ) = ( ( invg ` R ) o. u ) ) |
146 |
145
|
oveq1d |
|- ( ( ph /\ u e. U ) -> ( ( ( invg ` S ) ` u ) supp .0. ) = ( ( ( invg ` R ) o. u ) supp .0. ) ) |
147 |
14 144
|
grpinvfn |
|- ( invg ` R ) Fn ( Base ` R ) |
148 |
147
|
a1i |
|- ( ( ph /\ u e. U ) -> ( invg ` R ) Fn ( Base ` R ) ) |
149 |
3 144
|
grpinvid |
|- ( R e. Grp -> ( ( invg ` R ) ` .0. ) = .0. ) |
150 |
143 149
|
syl |
|- ( ( ph /\ u e. U ) -> ( ( invg ` R ) ` .0. ) = .0. ) |
151 |
148 80 98 99 150
|
suppcoss |
|- ( ( ph /\ u e. U ) -> ( ( ( invg ` R ) o. u ) supp .0. ) C_ ( u supp .0. ) ) |
152 |
146 151
|
eqsstrd |
|- ( ( ph /\ u e. U ) -> ( ( ( invg ` S ) ` u ) supp .0. ) C_ ( u supp .0. ) ) |
153 |
|
sseq1 |
|- ( y = ( ( ( invg ` S ) ` u ) supp .0. ) -> ( y C_ ( u supp .0. ) <-> ( ( ( invg ` S ) ` u ) supp .0. ) C_ ( u supp .0. ) ) ) |
154 |
|
eleq1 |
|- ( y = ( ( ( invg ` S ) ` u ) supp .0. ) -> ( y e. A <-> ( ( ( invg ` S ) ` u ) supp .0. ) e. A ) ) |
155 |
153 154
|
imbi12d |
|- ( y = ( ( ( invg ` S ) ` u ) supp .0. ) -> ( ( y C_ ( u supp .0. ) -> y e. A ) <-> ( ( ( ( invg ` S ) ` u ) supp .0. ) C_ ( u supp .0. ) -> ( ( ( invg ` S ) ` u ) supp .0. ) e. A ) ) ) |
156 |
155
|
spcgv |
|- ( ( ( ( invg ` S ) ` u ) supp .0. ) e. _V -> ( A. y ( y C_ ( u supp .0. ) -> y e. A ) -> ( ( ( ( invg ` S ) ` u ) supp .0. ) C_ ( u supp .0. ) -> ( ( ( invg ` S ) ` u ) supp .0. ) e. A ) ) ) |
157 |
136 141 152 156
|
syl3c |
|- ( ( ph /\ u e. U ) -> ( ( ( invg ` S ) ` u ) supp .0. ) e. A ) |
158 |
45
|
eleq2d |
|- ( ( ph /\ u e. U ) -> ( ( ( invg ` S ) ` u ) e. U <-> ( ( invg ` S ) ` u ) e. { g e. B | ( g supp .0. ) e. A } ) ) |
159 |
|
oveq1 |
|- ( g = ( ( invg ` S ) ` u ) -> ( g supp .0. ) = ( ( ( invg ` S ) ` u ) supp .0. ) ) |
160 |
159
|
eleq1d |
|- ( g = ( ( invg ` S ) ` u ) -> ( ( g supp .0. ) e. A <-> ( ( ( invg ` S ) ` u ) supp .0. ) e. A ) ) |
161 |
160
|
elrab |
|- ( ( ( invg ` S ) ` u ) e. { g e. B | ( g supp .0. ) e. A } <-> ( ( ( invg ` S ) ` u ) e. B /\ ( ( ( invg ` S ) ` u ) supp .0. ) e. A ) ) |
162 |
158 161
|
bitrdi |
|- ( ( ph /\ u e. U ) -> ( ( ( invg ` S ) ` u ) e. U <-> ( ( ( invg ` S ) ` u ) e. B /\ ( ( ( invg ` S ) ` u ) supp .0. ) e. A ) ) ) |
163 |
135 157 162
|
mpbir2and |
|- ( ( ph /\ u e. U ) -> ( ( invg ` S ) ` u ) e. U ) |
164 |
131 163
|
jca |
|- ( ( ph /\ u e. U ) -> ( A. v e. U ( u ( +g ` S ) v ) e. U /\ ( ( invg ` S ) ` u ) e. U ) ) |
165 |
164
|
ralrimiva |
|- ( ph -> A. u e. U ( A. v e. U ( u ( +g ` S ) v ) e. U /\ ( ( invg ` S ) ` u ) e. U ) ) |
166 |
2 34 133
|
issubg2 |
|- ( S e. Grp -> ( U e. ( SubGrp ` S ) <-> ( U C_ B /\ U =/= (/) /\ A. u e. U ( A. v e. U ( u ( +g ` S ) v ) e. U /\ ( ( invg ` S ) ` u ) e. U ) ) ) ) |
167 |
132 166
|
syl |
|- ( ph -> ( U e. ( SubGrp ` S ) <-> ( U C_ B /\ U =/= (/) /\ A. u e. U ( A. v e. U ( u ( +g ` S ) v ) e. U /\ ( ( invg ` S ) ` u ) e. U ) ) ) ) |
168 |
12 33 165 167
|
mpbir3and |
|- ( ph -> U e. ( SubGrp ` S ) ) |