Metamath Proof Explorer


Theorem mplsubglem

Description: If A is an ideal of sets (a nonempty collection closed under subset and binary union) of the set D of finite bags (the primary applications being A = Fin and A = ~P B for some B ), then the set of all power series whose coefficient functions are supported on an element of A is a subgroup of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015) (Revised by AV, 16-Jul-2019)

Ref Expression
Hypotheses mplsubglem.s
|- S = ( I mPwSer R )
mplsubglem.b
|- B = ( Base ` S )
mplsubglem.z
|- .0. = ( 0g ` R )
mplsubglem.d
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mplsubglem.i
|- ( ph -> I e. W )
mplsubglem.0
|- ( ph -> (/) e. A )
mplsubglem.a
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x u. y ) e. A )
mplsubglem.y
|- ( ( ph /\ ( x e. A /\ y C_ x ) ) -> y e. A )
mplsubglem.u
|- ( ph -> U = { g e. B | ( g supp .0. ) e. A } )
mplsubglem.r
|- ( ph -> R e. Grp )
Assertion mplsubglem
|- ( ph -> U e. ( SubGrp ` S ) )

Proof

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