This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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