Theorem mplsubglem 18735

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

Hypotheses

Ref	Expression
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

Ref	Expression
mplsubglem	|- ( ph -> U e. (SubGrp ` S ) )

Distinct variable groups:   f, g, x, y, .0.   A, f, g, x, y   B, f, g   D, g   f, I   ph, x, y   S, f, g, y

Allowed substitution hints:   ph( f, g)   B( x, y)   D( x, y, f)   R( x, y, f, g)   S( x)   U( x, y, f, g)   I( x, y, g)   W( x, y, f, g)

Proof of Theorem mplsubglem

Dummy variables k u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mplsubglem.u	. . 3 |- ( ph -> U = { g e. B | ( g supp .0. ) e. A } )
2		ssrab2 3500	. . 3 |- { g e. B | ( g supp .0. ) e. A } C_ B
3	1, 2	syl6eqss 3468	. 2 |- ( ph -> U C_ B )
4		mplsubglem.s	. . . . 5 |- S = ( I mPwSer R )
5		mplsubglem.i	. . . . 5 |- ( ph -> I e. W )
6		mplsubglem.r	. . . . 5 |- ( ph -> R e. Grp )
7		mplsubglem.d	. . . . 5 |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
8		mplsubglem.z	. . . . 5 |- .0. = ( 0g ` R )
9		mplsubglem.b	. . . . 5 |- B = ( Base ` S )
10	4, 5, 6, 7, 8, 9	psr0cl 18695	. . . 4 |- ( ph -> ( D X. { .0. } ) e. B )
11		eqid 2471	. . . . . . . . 9 |- ( Base ` R ) = ( Base ` R )
12	11, 8	grpidcl 16772	. . . . . . . 8 |- ( R e. Grp -> .0. e. ( Base ` R ) )
13		fconst6g 5785	. . . . . . . 8 |- ( .0. e. ( Base ` R ) -> ( D X. { .0. } ) : D --> ( Base ` R ) )
14	6, 12, 13	3syl 18	. . . . . . 7 |- ( ph -> ( D X. { .0. } ) : D --> ( Base ` R ) )
15		eldifi 3544	. . . . . . . . 9 |- ( u e. ( D \ (/) ) -> u e. D )
16		fvex 5889	. . . . . . . . . . 11 |- ( 0g ` R ) e. _V
17	8, 16	eqeltri 2545	. . . . . . . . . 10 |- .0. e. _V
18	17	fvconst2 6136	. . . . . . . . 9 |- ( u e. D -> ( ( D X. { .0. } ) ` u ) = .0. )
19	15, 18	syl 17	. . . . . . . 8 |- ( u e. ( D \ (/) ) -> ( ( D X. { .0. } ) ` u ) = .0. )
20	19	adantl 473	. . . . . . 7 |- ( ( ph /\ u e. ( D \ (/) ) ) -> ( ( D X. { .0. } ) ` u ) = .0. )
21	14, 20	suppss 6964	. . . . . 6 |- ( ph -> ( ( D X. { .0. } ) supp .0. ) C_ (/) )
22		ss0 3768	. . . . . 6 |- ( ( ( D X. { .0. } ) supp .0. ) C_ (/) -> ( ( D X. { .0. } ) supp .0. ) = (/) )
23	21, 22	syl 17	. . . . 5 |- ( ph -> ( ( D X. { .0. } ) supp .0. ) = (/) )
24		mplsubglem.0	. . . . 5 |- ( ph -> (/) e. A )
25	23, 24	eqeltrd 2549	. . . 4 |- ( ph -> ( ( D X. { .0. } ) supp .0. ) e. A )
26	1	eleq2d 2534	. . . . 5 |- ( ph -> ( ( D X. { .0. } ) e. U <-> ( D X. { .0. } ) e. { g e. B | ( g supp .0. ) e. A } ) )
27		oveq1 6315	. . . . . . 7 |- ( g = ( D X. { .0. } ) -> ( g supp .0. ) = ( ( D X. { .0. } ) supp .0. ) )
28	27	eleq1d 2533	. . . . . 6 |- ( g = ( D X. { .0. } ) -> ( ( g supp .0. ) e. A <-> ( ( D X. { .0. } ) supp .0. ) e. A ) )
29	28	elrab 3184	. . . . 5 |- ( ( D X. { .0. } ) e. { g e. B | ( g supp .0. ) e. A } <-> ( ( D X. { .0. } ) e. B /\ ( ( D X. { .0. } ) supp .0. ) e. A ) )
30	26, 29	syl6bb 269	. . . 4 |- ( ph -> ( ( D X. { .0. } ) e. U <-> ( ( D X. { .0. } ) e. B /\ ( ( D X. { .0. } ) supp .0. ) e. A ) ) )
31	10, 25, 30	mpbir2and 936	. . 3 |- ( ph -> ( D X. { .0. } ) e. U )
32		ne0i 3728	. . 3 |- ( ( D X. { .0. } ) e. U -> U =/= (/) )
33	31, 32	syl 17	. 2 |- ( ph -> U =/= (/) )
34		eqid 2471	. . . . . . 7 |- ( +g ` S ) = ( +g ` S )
35	6	ad2antrr 740	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> R e. Grp )
36	1	eleq2d 2534	. . . . . . . . . . 11 |- ( ph -> ( u e. U <-> u e. { g e. B | ( g supp .0. ) e. A } ) )
37		oveq1 6315	. . . . . . . . . . . . 13 |- ( g = u -> ( g supp .0. ) = ( u supp .0. ) )
38	37	eleq1d 2533	. . . . . . . . . . . 12 |- ( g = u -> ( ( g supp .0. ) e. A <-> ( u supp .0. ) e. A ) )
39	38	elrab 3184	. . . . . . . . . . 11 |- ( u e. { g e. B | ( g supp .0. ) e. A } <-> ( u e. B /\ ( u supp .0. ) e. A ) )
40	36, 39	syl6bb 269	. . . . . . . . . 10 |- ( ph -> ( u e. U <-> ( u e. B /\ ( u supp .0. ) e. A ) ) )
41	40	biimpa 492	. . . . . . . . 9 |- ( ( ph /\ u e. U ) -> ( u e. B /\ ( u supp .0. ) e. A ) )
42	41	simpld 466	. . . . . . . 8 |- ( ( ph /\ u e. U ) -> u e. B )
43	42	adantr 472	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> u e. B )
44	1	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ u e. U ) -> U = { g e. B | ( g supp .0. ) e. A } )
45	44	eleq2d 2534	. . . . . . . . . 10 |- ( ( ph /\ u e. U ) -> ( v e. U <-> v e. { g e. B | ( g supp .0. ) e. A } ) )
46		oveq1 6315	. . . . . . . . . . . 12 |- ( g = v -> ( g supp .0. ) = ( v supp .0. ) )
47	46	eleq1d 2533	. . . . . . . . . . 11 |- ( g = v -> ( ( g supp .0. ) e. A <-> ( v supp .0. ) e. A ) )
48	47	elrab 3184	. . . . . . . . . 10 |- ( v e. { g e. B | ( g supp .0. ) e. A } <-> ( v e. B /\ ( v supp .0. ) e. A ) )
49	45, 48	syl6bb 269	. . . . . . . . 9 |- ( ( ph /\ u e. U ) -> ( v e. U <-> ( v e. B /\ ( v supp .0. ) e. A ) ) )
50	49	biimpa 492	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( v e. B /\ ( v supp .0. ) e. A ) )
51	50	simpld 466	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> v e. B )
52	4, 9, 34, 35, 43, 51	psraddcl 18684	. . . . . 6 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u ( +g ` S ) v ) e. B )
53		ovex 6336	. . . . . . . 8 |- ( ( u ( +g ` S ) v ) supp .0. ) e. _V
54	53	a1i 11	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) supp .0. ) e. _V )
55	41	simprd 470	. . . . . . . . . 10 |- ( ( ph /\ u e. U ) -> ( u supp .0. ) e. A )
56	55	adantr 472	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u supp .0. ) e. A )
57	50	simprd 470	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( v supp .0. ) e. A )
58		mplsubglem.a	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x u. y ) e. A )
59	58	ralrimivva 2814	. . . . . . . . . 10 |- ( ph -> A. x e. A A. y e. A ( x u. y ) e. A )
60	59	ad2antrr 740	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> A. x e. A A. y e. A ( x u. y ) e. A )
61		uneq1 3572	. . . . . . . . . . 11 |- ( x = ( u supp .0. ) -> ( x u. y ) = ( ( u supp .0. ) u. y ) )
62	61	eleq1d 2533	. . . . . . . . . 10 |- ( x = ( u supp .0. ) -> ( ( x u. y ) e. A <-> ( ( u supp .0. ) u. y ) e. A ) )
63		uneq2 3573	. . . . . . . . . . 11 |- ( y = ( v supp .0. ) -> ( ( u supp .0. ) u. y ) = ( ( u supp .0. ) u. ( v supp .0. ) ) )
64	63	eleq1d 2533	. . . . . . . . . 10 |- ( y = ( v supp .0. ) -> ( ( ( u supp .0. ) u. y ) e. A <-> ( ( u supp .0. ) u. ( v supp .0. ) ) e. A ) )
65	62, 64	rspc2va 3148	. . . . . . . . 9 |- ( ( ( ( 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 )
66	56, 57, 60, 65	syl21anc 1291	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u supp .0. ) u. ( v supp .0. ) ) e. A )
67		mplsubglem.y	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. A /\ y C_ x ) ) -> y e. A )
68	67	expr 626	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( y C_ x -> y e. A ) )
69	68	alrimiv 1781	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> A. y ( y C_ x -> y e. A ) )
70	69	ralrimiva 2809	. . . . . . . . 9 |- ( ph -> A. x e. A A. y ( y C_ x -> y e. A ) )
71	70	ad2antrr 740	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> A. x e. A A. y ( y C_ x -> y e. A ) )
72		sseq2 3440	. . . . . . . . . . 11 |- ( x = ( ( u supp .0. ) u. ( v supp .0. ) ) -> ( y C_ x <-> y C_ ( ( u supp .0. ) u. ( v supp .0. ) ) ) )
73	72	imbi1d 324	. . . . . . . . . 10 |- ( 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 ) ) )
74	73	albidv 1775	. . . . . . . . 9 |- ( 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 ) ) )
75	74	rspcv 3132	. . . . . . . 8 |- ( ( ( u supp .0. ) u. ( v supp .0. ) ) e. A -> ( A. x e. A A. y ( y C_ x -> y e. A ) -> A. y ( y C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> y e. A ) ) )
76	66, 71, 75	sylc 61	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> A. y ( y C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> y e. A ) )
77	4, 11, 7, 9, 52	psrelbas 18680	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u ( +g ` S ) v ) : D --> ( Base ` R ) )
78		eqid 2471	. . . . . . . . . . . 12 |- ( +g ` R ) = ( +g ` R )
79	4, 9, 78, 34, 43, 51	psradd 18683	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u ( +g ` S ) v ) = ( u oF ( +g ` R ) v ) )
80	79	fveq1d 5881	. . . . . . . . . 10 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) ` k ) = ( ( u oF ( +g ` R ) v ) ` k ) )
81	80	adantr 472	. . . . . . . . 9 |- ( ( ( ( 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 ) )
82		eldifi 3544	. . . . . . . . . 10 |- ( k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) -> k e. D )
83	4, 11, 7, 9, 42	psrelbas 18680	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. U ) -> u : D --> ( Base ` R ) )
84	83	adantr 472	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> u : D --> ( Base ` R ) )
85	84	ffnd 5740	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> u Fn D )
86	4, 11, 7, 9, 51	psrelbas 18680	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> v : D --> ( Base ` R ) )
87	86	ffnd 5740	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> v Fn D )
88		ovex 6336	. . . . . . . . . . . . 13 |- ( NN0 ^m I ) e. _V
89	7, 88	rabex2 4552	. . . . . . . . . . . 12 |- D e. _V
90	89	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> D e. _V )
91		inidm 3632	. . . . . . . . . . 11 |- ( D i^i D ) = D
92		eqidd 2472	. . . . . . . . . . 11 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. D ) -> ( u ` k ) = ( u ` k ) )
93		eqidd 2472	. . . . . . . . . . 11 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. D ) -> ( v ` k ) = ( v ` k ) )
94	85, 87, 90, 90, 91, 92, 93	ofval 6559	. . . . . . . . . 10 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. D ) -> ( ( u oF ( +g ` R ) v ) ` k ) = ( ( u ` k ) ( +g ` R ) ( v ` k ) ) )
95	82, 94	sylan2 482	. . . . . . . . 9 |- ( ( ( ( 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 ) ) )
96		ssun1 3588	. . . . . . . . . . . . . 14 |- ( u supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) )
97		sscon 3556	. . . . . . . . . . . . . 14 |- ( ( u supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) C_ ( D \ ( u supp .0. ) ) )
98	96, 97	ax-mp 5	. . . . . . . . . . . . 13 |- ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) C_ ( D \ ( u supp .0. ) )
99	98	sseli 3414	. . . . . . . . . . . 12 |- ( k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) -> k e. ( D \ ( u supp .0. ) ) )
100		ssid 3437	. . . . . . . . . . . . . . 15 |- ( u supp .0. ) C_ ( u supp .0. )
101	100	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. U ) -> ( u supp .0. ) C_ ( u supp .0. ) )
102	89	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. U ) -> D e. _V )
103	17	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. U ) -> .0. e. _V )
104	83, 101, 102, 103	suppssr 6965	. . . . . . . . . . . . 13 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( u supp .0. ) ) ) -> ( u ` k ) = .0. )
105	104	adantlr 729	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( u supp .0. ) ) ) -> ( u ` k ) = .0. )
106	99, 105	sylan2 482	. . . . . . . . . . 11 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( u ` k ) = .0. )
107		ssun2 3589	. . . . . . . . . . . . . 14 |- ( v supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) )
108		sscon 3556	. . . . . . . . . . . . . 14 |- ( ( v supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) ) -> ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) C_ ( D \ ( v supp .0. ) ) )
109	107, 108	ax-mp 5	. . . . . . . . . . . . 13 |- ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) C_ ( D \ ( v supp .0. ) )
110	109	sseli 3414	. . . . . . . . . . . 12 |- ( k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) -> k e. ( D \ ( v supp .0. ) ) )
111		ssid 3437	. . . . . . . . . . . . . 14 |- ( v supp .0. ) C_ ( v supp .0. )
112	111	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( v supp .0. ) C_ ( v supp .0. ) )
113	17	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> .0. e. _V )
114	86, 112, 90, 113	suppssr 6965	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( v supp .0. ) ) ) -> ( v ` k ) = .0. )
115	110, 114	sylan2 482	. . . . . . . . . . 11 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( v ` k ) = .0. )
116	106, 115	oveq12d 6326	. . . . . . . . . 10 |- ( ( ( ( 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. ) )
117	11, 78, 8	grplid 16774	. . . . . . . . . . . . 13 |- ( ( R e. Grp /\ .0. e. ( Base ` R ) ) -> ( .0. ( +g ` R ) .0. ) = .0. )
118	12, 117	mpdan 681	. . . . . . . . . . . 12 |- ( R e. Grp -> ( .0. ( +g ` R ) .0. ) = .0. )
119	35, 118	syl 17	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( .0. ( +g ` R ) .0. ) = .0. )
120	119	adantr 472	. . . . . . . . . 10 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( .0. ( +g ` R ) .0. ) = .0. )
121	116, 120	eqtrd 2505	. . . . . . . . 9 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( ( u ` k ) ( +g ` R ) ( v ` k ) ) = .0. )
122	81, 95, 121	3eqtrd 2509	. . . . . . . 8 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( u supp .0. ) u. ( v supp .0. ) ) ) ) -> ( ( u ( +g ` S ) v ) ` k ) = .0. )
123	77, 122	suppss 6964	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) supp .0. ) C_ ( ( u supp .0. ) u. ( v supp .0. ) ) )
124		sseq1 3439	. . . . . . . . 9 |- ( 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. ) ) ) )
125		eleq1 2537	. . . . . . . . 9 |- ( y = ( ( u ( +g ` S ) v ) supp .0. ) -> ( y e. A <-> ( ( u ( +g ` S ) v ) supp .0. ) e. A ) )
126	124, 125	imbi12d 327	. . . . . . . 8 |- ( 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 ) ) )
127	126	spcgv 3120	. . . . . . 7 |- ( ( ( 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 ) ) )
128	54, 76, 123, 127	syl3c 62	. . . . . 6 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) supp .0. ) e. A )
129	1	ad2antrr 740	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> U = { g e. B | ( g supp .0. ) e. A } )
130	129	eleq2d 2534	. . . . . . 7 |- ( ( ( 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 } ) )
131		oveq1 6315	. . . . . . . . 9 |- ( g = ( u ( +g ` S ) v ) -> ( g supp .0. ) = ( ( u ( +g ` S ) v ) supp .0. ) )
132	131	eleq1d 2533	. . . . . . . 8 |- ( g = ( u ( +g ` S ) v ) -> ( ( g supp .0. ) e. A <-> ( ( u ( +g ` S ) v ) supp .0. ) e. A ) )
133	132	elrab 3184	. . . . . . 7 |- ( ( 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 ) )
134	130, 133	syl6bb 269	. . . . . 6 |- ( ( ( 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 ) ) )
135	52, 128, 134	mpbir2and 936	. . . . 5 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u ( +g ` S ) v ) e. U )
136	135	ralrimiva 2809	. . . 4 |- ( ( ph /\ u e. U ) -> A. v e. U ( u ( +g ` S ) v ) e. U )
137	4, 5, 6	psrgrp 18699	. . . . . 6 |- ( ph -> S e. Grp )
138		eqid 2471	. . . . . . 7 |- ( invg ` S ) = ( invg ` S )
139	9, 138	grpinvcl 16789	. . . . . 6 |- ( ( S e. Grp /\ u e. B ) -> ( ( invg ` S ) ` u ) e. B )
140	137, 42, 139	syl2an2r 849	. . . . 5 |- ( ( ph /\ u e. U ) -> ( ( invg ` S ) ` u ) e. B )
141		ovex 6336	. . . . . . 7 |- ( ( ( invg ` S ) ` u ) supp .0. ) e. _V
142	141	a1i 11	. . . . . 6 |- ( ( ph /\ u e. U ) -> ( ( ( invg ` S ) ` u ) supp .0. ) e. _V )
143	70	adantr 472	. . . . . . 7 |- ( ( ph /\ u e. U ) -> A. x e. A A. y ( y C_ x -> y e. A ) )
144		sseq2 3440	. . . . . . . . . 10 |- ( x = ( u supp .0. ) -> ( y C_ x <-> y C_ ( u supp .0. ) ) )
145	144	imbi1d 324	. . . . . . . . 9 |- ( x = ( u supp .0. ) -> ( ( y C_ x -> y e. A ) <-> ( y C_ ( u supp .0. ) -> y e. A ) ) )
146	145	albidv 1775	. . . . . . . 8 |- ( x = ( u supp .0. ) -> ( A. y ( y C_ x -> y e. A ) <-> A. y ( y C_ ( u supp .0. ) -> y e. A ) ) )
147	146	rspcv 3132	. . . . . . 7 |- ( ( u supp .0. ) e. A -> ( A. x e. A A. y ( y C_ x -> y e. A ) -> A. y ( y C_ ( u supp .0. ) -> y e. A ) ) )
148	55, 143, 147	sylc 61	. . . . . 6 |- ( ( ph /\ u e. U ) -> A. y ( y C_ ( u supp .0. ) -> y e. A ) )
149	4, 11, 7, 9, 140	psrelbas 18680	. . . . . . 7 |- ( ( ph /\ u e. U ) -> ( ( invg ` S ) ` u ) : D --> ( Base ` R ) )
150	5	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ u e. U ) -> I e. W )
151	6	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ u e. U ) -> R e. Grp )
152		eqid 2471	. . . . . . . . . . 11 |- ( invg ` R ) = ( invg ` R )
153	4, 150, 151, 7, 152, 9, 138, 42	psrneg 18701	. . . . . . . . . 10 |- ( ( ph /\ u e. U ) -> ( ( invg ` S ) ` u ) = ( ( invg ` R ) o. u ) )
154	153	adantr 472	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( u supp .0. ) ) ) -> ( ( invg ` S ) ` u ) = ( ( invg ` R ) o. u ) )
155	154	fveq1d 5881	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( u supp .0. ) ) ) -> ( ( ( invg ` S ) ` u ) ` k ) = ( ( ( invg ` R ) o. u ) ` k ) )
156		eldifi 3544	. . . . . . . . 9 |- ( k e. ( D \ ( u supp .0. ) ) -> k e. D )
157		fvco3 5957	. . . . . . . . 9 |- ( ( u : D --> ( Base ` R ) /\ k e. D ) -> ( ( ( invg ` R ) o. u ) ` k ) = ( ( invg ` R ) ` ( u ` k ) ) )
158	83, 156, 157	syl2an 485	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( u supp .0. ) ) ) -> ( ( ( invg ` R ) o. u ) ` k ) = ( ( invg ` R ) ` ( u ` k ) ) )
159	104	fveq2d 5883	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( u supp .0. ) ) ) -> ( ( invg ` R ) ` ( u ` k ) ) = ( ( invg ` R ) ` .0. ) )
160	8, 152	grpinvid 16795	. . . . . . . . . . 11 |- ( R e. Grp -> ( ( invg ` R ) ` .0. ) = .0. )
161	151, 160	syl 17	. . . . . . . . . 10 |- ( ( ph /\ u e. U ) -> ( ( invg ` R ) ` .0. ) = .0. )
162	161	adantr 472	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( u supp .0. ) ) ) -> ( ( invg ` R ) ` .0. ) = .0. )
163	159, 162	eqtrd 2505	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( u supp .0. ) ) ) -> ( ( invg ` R ) ` ( u ` k ) ) = .0. )
164	155, 158, 163	3eqtrd 2509	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( u supp .0. ) ) ) -> ( ( ( invg ` S ) ` u ) ` k ) = .0. )
165	149, 164	suppss 6964	. . . . . 6 |- ( ( ph /\ u e. U ) -> ( ( ( invg ` S ) ` u ) supp .0. ) C_ ( u supp .0. ) )
166		sseq1 3439	. . . . . . . 8 |- ( y = ( ( ( invg ` S ) ` u ) supp .0. ) -> ( y C_ ( u supp .0. ) <-> ( ( ( invg ` S ) ` u ) supp .0. ) C_ ( u supp .0. ) ) )
167		eleq1 2537	. . . . . . . 8 |- ( y = ( ( ( invg ` S ) ` u ) supp .0. ) -> ( y e. A <-> ( ( ( invg ` S ) ` u ) supp .0. ) e. A ) )
168	166, 167	imbi12d 327	. . . . . . 7 |- ( 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 ) ) )
169	168	spcgv 3120	. . . . . 6 |- ( ( ( ( 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 ) ) )
170	142, 148, 165, 169	syl3c 62	. . . . 5 |- ( ( ph /\ u e. U ) -> ( ( ( invg ` S ) ` u ) supp .0. ) e. A )
171	44	eleq2d 2534	. . . . . 6 |- ( ( ph /\ u e. U ) -> ( ( ( invg ` S ) ` u ) e. U <-> ( ( invg ` S ) ` u ) e. { g e. B | ( g supp .0. ) e. A } ) )
172		oveq1 6315	. . . . . . . 8 |- ( g = ( ( invg ` S ) ` u ) -> ( g supp .0. ) = ( ( ( invg ` S ) ` u ) supp .0. ) )
173	172	eleq1d 2533	. . . . . . 7 |- ( g = ( ( invg ` S ) ` u ) -> ( ( g supp .0. ) e. A <-> ( ( ( invg ` S ) ` u ) supp .0. ) e. A ) )
174	173	elrab 3184	. . . . . 6 |- ( ( ( invg ` S ) ` u ) e. { g e. B | ( g supp .0. ) e. A } <-> ( ( ( invg ` S ) ` u ) e. B /\ ( ( ( invg ` S ) ` u ) supp .0. ) e. A ) )
175	171, 174	syl6bb 269	. . . . 5 |- ( ( ph /\ u e. U ) -> ( ( ( invg ` S ) ` u ) e. U <-> ( ( ( invg ` S ) ` u ) e. B /\ ( ( ( invg ` S ) ` u ) supp .0. ) e. A ) ) )
176	140, 170, 175	mpbir2and 936	. . . 4 |- ( ( ph /\ u e. U ) -> ( ( invg ` S ) ` u ) e. U )
177	136, 176	jca 541	. . 3 |- ( ( ph /\ u e. U ) -> ( A. v e. U ( u ( +g ` S ) v ) e. U /\ ( ( invg ` S ) ` u ) e. U ) )
178	177	ralrimiva 2809	. 2 |- ( ph -> A. u e. U ( A. v e. U ( u ( +g ` S ) v ) e. U /\ ( ( invg ` S ) ` u ) e. U ) )
179	9, 34, 138	issubg2 16910	. . 3 |- ( 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 ) ) ) )
180	137, 179	syl 17	. 2 |- ( 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 ) ) ) )
181	3, 33, 178, 180	mpbir3and 1213	1 |- ( ph -> U e. (SubGrp ` S ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   /\ w3a 1007   A.wal 1450   = wceq 1452   e. wcel 1904   =/= wne 2641   A.wral 2756   {crab 2760   _Vcvv 3031   \ cdif 3387   u. cun 3388   C_ wss 3390   (/)c0 3722   {csn 3959   X. cxp 4837   `'ccnv 4838   "cima 4842   o. ccom 4843   -->wf 5585   ` cfv 5589  (class class class)co 6308   oFcof 6548   supp csupp 6933   ^m cmap 7490   Fincfn 7587   NNcn 10631   NN0cn0 10893   Basecbs 15199   +g cplusg 15268   0gc0g 15416   Grpcgrp 16747   invgcminusg 16748  SubGrpcsubg 16889   mPwSer cmps 18652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-map 7492  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-n0 10894  df-z 10962  df-uz 11183  df-fz 11811  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-mulr 15282  df-sca 15284  df-vsca 15285  df-tset 15287  df-0g 15418  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-grp 16751  df-minusg 16752  df-subg 16892  df-psr 18657

This theorem is referenced by:  mpllsslem  18736  mplsubg  18738