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