Theorem mplsubglem 16453

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

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 " ( _V \ { .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 " ( _V \ { .0. } ) ) e. A } )
2		ssrab2 3388	. . 3 |- { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } C_ B
3	1, 2	syl6eqss 3358	. 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 16413	. . . 4 |- ( ph -> ( D X. { .0. } ) e. B )
11		eqid 2404	. . . . . . . . 9 |- ( Base ` R ) = ( Base ` R )
12	11, 8	grpidcl 14788	. . . . . . . 8 |- ( R e. Grp -> .0. e. ( Base ` R ) )
13		fconst6g 5591	. . . . . . . 8 |- ( .0. e. ( Base ` R ) -> ( D X. { .0. } ) : D --> ( Base ` R ) )
14	6, 12, 13	3syl 19	. . . . . . 7 |- ( ph -> ( D X. { .0. } ) : D --> ( Base ` R ) )
15		eldifi 3429	. . . . . . . . 9 |- ( u e. ( D \ (/) ) -> u e. D )
16		fvex 5701	. . . . . . . . . . 11 |- ( 0g ` R ) e. _V
17	8, 16	eqeltri 2474	. . . . . . . . . 10 |- .0. e. _V
18	17	fvconst2 5906	. . . . . . . . 9 |- ( u e. D -> ( ( D X. { .0. } ) ` u ) = .0. )
19	15, 18	syl 16	. . . . . . . 8 |- ( u e. ( D \ (/) ) -> ( ( D X. { .0. } ) ` u ) = .0. )
20	19	adantl 453	. . . . . . 7 |- ( ( ph /\ u e. ( D \ (/) ) ) -> ( ( D X. { .0. } ) ` u ) = .0. )
21	14, 20	suppss 5822	. . . . . 6 |- ( ph -> ( `' ( D X. { .0. } ) " ( _V \ { .0. } ) ) C_ (/) )
22		ss0 3618	. . . . . 6 |- ( ( `' ( D X. { .0. } ) " ( _V \ { .0. } ) ) C_ (/) -> ( `' ( D X. { .0. } ) " ( _V \ { .0. } ) ) = (/) )
23	21, 22	syl 16	. . . . 5 |- ( ph -> ( `' ( D X. { .0. } ) " ( _V \ { .0. } ) ) = (/) )
24		mplsubglem.0	. . . . 5 |- ( ph -> (/) e. A )
25	23, 24	eqeltrd 2478	. . . 4 |- ( ph -> ( `' ( D X. { .0. } ) " ( _V \ { .0. } ) ) e. A )
26	1	eleq2d 2471	. . . . 5 |- ( ph -> ( ( D X. { .0. } ) e. U <-> ( D X. { .0. } ) e. { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } ) )
27		cnveq 5005	. . . . . . . 8 |- ( g = ( D X. { .0. } ) -> `' g = `' ( D X. { .0. } ) )
28	27	imaeq1d 5161	. . . . . . 7 |- ( g = ( D X. { .0. } ) -> ( `' g " ( _V \ { .0. } ) ) = ( `' ( D X. { .0. } ) " ( _V \ { .0. } ) ) )
29	28	eleq1d 2470	. . . . . 6 |- ( g = ( D X. { .0. } ) -> ( ( `' g " ( _V \ { .0. } ) ) e. A <-> ( `' ( D X. { .0. } ) " ( _V \ { .0. } ) ) e. A ) )
30	29	elrab 3052	. . . . 5 |- ( ( D X. { .0. } ) e. { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } <-> ( ( D X. { .0. } ) e. B /\ ( `' ( D X. { .0. } ) " ( _V \ { .0. } ) ) e. A ) )
31	26, 30	syl6bb 253	. . . 4 |- ( ph -> ( ( D X. { .0. } ) e. U <-> ( ( D X. { .0. } ) e. B /\ ( `' ( D X. { .0. } ) " ( _V \ { .0. } ) ) e. A ) ) )
32	10, 25, 31	mpbir2and 889	. . 3 |- ( ph -> ( D X. { .0. } ) e. U )
33		ne0i 3594	. . 3 |- ( ( D X. { .0. } ) e. U -> U =/= (/) )
34	32, 33	syl 16	. 2 |- ( ph -> U =/= (/) )
35		eqid 2404	. . . . . . 7 |- ( +g ` S ) = ( +g ` S )
36	6	ad2antrr 707	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> R e. Grp )
37	1	eleq2d 2471	. . . . . . . . . . 11 |- ( ph -> ( u e. U <-> u e. { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } ) )
38		cnveq 5005	. . . . . . . . . . . . . 14 |- ( g = u -> `' g = `' u )
39	38	imaeq1d 5161	. . . . . . . . . . . . 13 |- ( g = u -> ( `' g " ( _V \ { .0. } ) ) = ( `' u " ( _V \ { .0. } ) ) )
40	39	eleq1d 2470	. . . . . . . . . . . 12 |- ( g = u -> ( ( `' g " ( _V \ { .0. } ) ) e. A <-> ( `' u " ( _V \ { .0. } ) ) e. A ) )
41	40	elrab 3052	. . . . . . . . . . 11 |- ( u e. { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } <-> ( u e. B /\ ( `' u " ( _V \ { .0. } ) ) e. A ) )
42	37, 41	syl6bb 253	. . . . . . . . . 10 |- ( ph -> ( u e. U <-> ( u e. B /\ ( `' u " ( _V \ { .0. } ) ) e. A ) ) )
43	42	biimpa 471	. . . . . . . . 9 |- ( ( ph /\ u e. U ) -> ( u e. B /\ ( `' u " ( _V \ { .0. } ) ) e. A ) )
44	43	simpld 446	. . . . . . . 8 |- ( ( ph /\ u e. U ) -> u e. B )
45	44	adantr 452	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> u e. B )
46	1	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ u e. U ) -> U = { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } )
47	46	eleq2d 2471	. . . . . . . . . 10 |- ( ( ph /\ u e. U ) -> ( v e. U <-> v e. { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } ) )
48		cnveq 5005	. . . . . . . . . . . . 13 |- ( g = v -> `' g = `' v )
49	48	imaeq1d 5161	. . . . . . . . . . . 12 |- ( g = v -> ( `' g " ( _V \ { .0. } ) ) = ( `' v " ( _V \ { .0. } ) ) )
50	49	eleq1d 2470	. . . . . . . . . . 11 |- ( g = v -> ( ( `' g " ( _V \ { .0. } ) ) e. A <-> ( `' v " ( _V \ { .0. } ) ) e. A ) )
51	50	elrab 3052	. . . . . . . . . 10 |- ( v e. { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } <-> ( v e. B /\ ( `' v " ( _V \ { .0. } ) ) e. A ) )
52	47, 51	syl6bb 253	. . . . . . . . 9 |- ( ( ph /\ u e. U ) -> ( v e. U <-> ( v e. B /\ ( `' v " ( _V \ { .0. } ) ) e. A ) ) )
53	52	biimpa 471	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( v e. B /\ ( `' v " ( _V \ { .0. } ) ) e. A ) )
54	53	simpld 446	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> v e. B )
55	4, 9, 35, 36, 45, 54	psraddcl 16402	. . . . . 6 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u ( +g ` S ) v ) e. B )
56	43	simprd 450	. . . . . . . . . 10 |- ( ( ph /\ u e. U ) -> ( `' u " ( _V \ { .0. } ) ) e. A )
57	56	adantr 452	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( `' u " ( _V \ { .0. } ) ) e. A )
58	53	simprd 450	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( `' v " ( _V \ { .0. } ) ) e. A )
59		mplsubglem.a	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x u. y ) e. A )
60	59	ralrimivva 2758	. . . . . . . . . 10 |- ( ph -> A. x e. A A. y e. A ( x u. y ) e. A )
61	60	ad2antrr 707	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> A. x e. A A. y e. A ( x u. y ) e. A )
62		uneq1 3454	. . . . . . . . . . 11 |- ( x = ( `' u " ( _V \ { .0. } ) ) -> ( x u. y ) = ( ( `' u " ( _V \ { .0. } ) ) u. y ) )
63	62	eleq1d 2470	. . . . . . . . . 10 |- ( x = ( `' u " ( _V \ { .0. } ) ) -> ( ( x u. y ) e. A <-> ( ( `' u " ( _V \ { .0. } ) ) u. y ) e. A ) )
64		uneq2 3455	. . . . . . . . . . 11 |- ( y = ( `' v " ( _V \ { .0. } ) ) -> ( ( `' u " ( _V \ { .0. } ) ) u. y ) = ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) )
65	64	eleq1d 2470	. . . . . . . . . 10 |- ( y = ( `' v " ( _V \ { .0. } ) ) -> ( ( ( `' u " ( _V \ { .0. } ) ) u. y ) e. A <-> ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) e. A ) )
66	63, 65	rspc2va 3019	. . . . . . . . 9 |- ( ( ( ( `' u " ( _V \ { .0. } ) ) e. A /\ ( `' v " ( _V \ { .0. } ) ) e. A ) /\ A. x e. A A. y e. A ( x u. y ) e. A ) -> ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) e. A )
67	57, 58, 61, 66	syl21anc 1183	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) e. A )
68	4, 11, 7, 9, 55	psrelbas 16399	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u ( +g ` S ) v ) : D --> ( Base ` R ) )
69		eqid 2404	. . . . . . . . . . . . 13 |- ( +g ` R ) = ( +g ` R )
70	4, 9, 69, 35, 45, 54	psradd 16401	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u ( +g ` S ) v ) = ( u o F ( +g ` R ) v ) )
71	70	fveq1d 5689	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) ` k ) = ( ( u o F ( +g ` R ) v ) ` k ) )
72	71	adantr 452	. . . . . . . . . 10 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) ) -> ( ( u ( +g ` S ) v ) ` k ) = ( ( u o F ( +g ` R ) v ) ` k ) )
73		eldifi 3429	. . . . . . . . . . 11 |- ( k e. ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) -> k e. D )
74	4, 11, 7, 9, 44	psrelbas 16399	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. U ) -> u : D --> ( Base ` R ) )
75	74	adantr 452	. . . . . . . . . . . . 13 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> u : D --> ( Base ` R ) )
76		ffn 5550	. . . . . . . . . . . . 13 |- ( u : D --> ( Base ` R ) -> u Fn D )
77	75, 76	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> u Fn D )
78	4, 11, 7, 9, 54	psrelbas 16399	. . . . . . . . . . . . 13 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> v : D --> ( Base ` R ) )
79		ffn 5550	. . . . . . . . . . . . 13 |- ( v : D --> ( Base ` R ) -> v Fn D )
80	78, 79	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> v Fn D )
81		ovex 6065	. . . . . . . . . . . . . . 15 |- ( NN0 ^m I ) e. _V
82	81	rabex 4314	. . . . . . . . . . . . . 14 |- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
83	7, 82	eqeltri 2474	. . . . . . . . . . . . 13 |- D e. _V
84	83	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> D e. _V )
85		inidm 3510	. . . . . . . . . . . 12 |- ( D i^i D ) = D
86		eqidd 2405	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. D ) -> ( u ` k ) = ( u ` k ) )
87		eqidd 2405	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. D ) -> ( v ` k ) = ( v ` k ) )
88	77, 80, 84, 84, 85, 86, 87	ofval 6273	. . . . . . . . . . 11 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. D ) -> ( ( u o F ( +g ` R ) v ) ` k ) = ( ( u ` k ) ( +g ` R ) ( v ` k ) ) )
89	73, 88	sylan2 461	. . . . . . . . . 10 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) ) -> ( ( u o F ( +g ` R ) v ) ` k ) = ( ( u ` k ) ( +g ` R ) ( v ` k ) ) )
90		ssun1 3470	. . . . . . . . . . . . . . 15 |- ( `' u " ( _V \ { .0. } ) ) C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) )
91		sscon 3441	. . . . . . . . . . . . . . 15 |- ( ( `' u " ( _V \ { .0. } ) ) C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) C_ ( D \ ( `' u " ( _V \ { .0. } ) ) ) )
92	90, 91	ax-mp 8	. . . . . . . . . . . . . 14 |- ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) C_ ( D \ ( `' u " ( _V \ { .0. } ) ) )
93	92	sseli 3304	. . . . . . . . . . . . 13 |- ( k e. ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) -> k e. ( D \ ( `' u " ( _V \ { .0. } ) ) ) )
94		ssid 3327	. . . . . . . . . . . . . . . 16 |- ( `' u " ( _V \ { .0. } ) ) C_ ( `' u " ( _V \ { .0. } ) )
95	94	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. U ) -> ( `' u " ( _V \ { .0. } ) ) C_ ( `' u " ( _V \ { .0. } ) ) )
96	74, 95	suppssr 5823	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( `' u " ( _V \ { .0. } ) ) ) ) -> ( u ` k ) = .0. )
97	96	adantlr 696	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( `' u " ( _V \ { .0. } ) ) ) ) -> ( u ` k ) = .0. )
98	93, 97	sylan2 461	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) ) -> ( u ` k ) = .0. )
99		ssun2 3471	. . . . . . . . . . . . . . 15 |- ( `' v " ( _V \ { .0. } ) ) C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) )
100		sscon 3441	. . . . . . . . . . . . . . 15 |- ( ( `' v " ( _V \ { .0. } ) ) C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) C_ ( D \ ( `' v " ( _V \ { .0. } ) ) ) )
101	99, 100	ax-mp 8	. . . . . . . . . . . . . 14 |- ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) C_ ( D \ ( `' v " ( _V \ { .0. } ) ) )
102	101	sseli 3304	. . . . . . . . . . . . 13 |- ( k e. ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) -> k e. ( D \ ( `' v " ( _V \ { .0. } ) ) ) )
103		ssid 3327	. . . . . . . . . . . . . . 15 |- ( `' v " ( _V \ { .0. } ) ) C_ ( `' v " ( _V \ { .0. } ) )
104	103	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( `' v " ( _V \ { .0. } ) ) C_ ( `' v " ( _V \ { .0. } ) ) )
105	78, 104	suppssr 5823	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( `' v " ( _V \ { .0. } ) ) ) ) -> ( v ` k ) = .0. )
106	102, 105	sylan2 461	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) ) -> ( v ` k ) = .0. )
107	98, 106	oveq12d 6058	. . . . . . . . . . 11 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) ) -> ( ( u ` k ) ( +g ` R ) ( v ` k ) ) = ( .0. ( +g ` R ) .0. ) )
108	11, 69, 8	grplid 14790	. . . . . . . . . . . . . 14 |- ( ( R e. Grp /\ .0. e. ( Base ` R ) ) -> ( .0. ( +g ` R ) .0. ) = .0. )
109	12, 108	mpdan 650	. . . . . . . . . . . . 13 |- ( R e. Grp -> ( .0. ( +g ` R ) .0. ) = .0. )
110	36, 109	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( .0. ( +g ` R ) .0. ) = .0. )
111	110	adantr 452	. . . . . . . . . . 11 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) ) -> ( .0. ( +g ` R ) .0. ) = .0. )
112	107, 111	eqtrd 2436	. . . . . . . . . 10 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) ) -> ( ( u ` k ) ( +g ` R ) ( v ` k ) ) = .0. )
113	72, 89, 112	3eqtrd 2440	. . . . . . . . 9 |- ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ k e. ( D \ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) ) -> ( ( u ( +g ` S ) v ) ` k ) = .0. )
114	68, 113	suppss 5822	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) )
115	67, 114	ssexd 4310	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) e. _V )
116		mplsubglem.y	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. A /\ y C_ x ) ) -> y e. A )
117	116	expr 599	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( y C_ x -> y e. A ) )
118	117	alrimiv 1638	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> A. y ( y C_ x -> y e. A ) )
119	118	ralrimiva 2749	. . . . . . . . 9 |- ( ph -> A. x e. A A. y ( y C_ x -> y e. A ) )
120	119	ad2antrr 707	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> A. x e. A A. y ( y C_ x -> y e. A ) )
121		sseq2 3330	. . . . . . . . . . 11 |- ( x = ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> ( y C_ x <-> y C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) )
122	121	imbi1d 309	. . . . . . . . . 10 |- ( x = ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> ( ( y C_ x -> y e. A ) <-> ( y C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> y e. A ) ) )
123	122	albidv 1632	. . . . . . . . 9 |- ( x = ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> ( A. y ( y C_ x -> y e. A ) <-> A. y ( y C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> y e. A ) ) )
124	123	rspcv 3008	. . . . . . . 8 |- ( ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) e. A -> ( A. x e. A A. y ( y C_ x -> y e. A ) -> A. y ( y C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> y e. A ) ) )
125	67, 120, 124	sylc 58	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> A. y ( y C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> y e. A ) )
126		sseq1 3329	. . . . . . . . 9 |- ( y = ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) -> ( y C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) <-> ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) ) )
127		eleq1 2464	. . . . . . . . 9 |- ( y = ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) -> ( y e. A <-> ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) e. A ) )
128	126, 127	imbi12d 312	. . . . . . . 8 |- ( y = ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) -> ( ( y C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> y e. A ) <-> ( ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) e. A ) ) )
129	128	spcgv 2996	. . . . . . 7 |- ( ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) e. _V -> ( A. y ( y C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> y e. A ) -> ( ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) C_ ( ( `' u " ( _V \ { .0. } ) ) u. ( `' v " ( _V \ { .0. } ) ) ) -> ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) e. A ) ) )
130	115, 125, 114, 129	syl3c 59	. . . . . 6 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) e. A )
131	1	ad2antrr 707	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> U = { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } )
132	131	eleq2d 2471	. . . . . . 7 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) e. U <-> ( u ( +g ` S ) v ) e. { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } ) )
133		cnveq 5005	. . . . . . . . . 10 |- ( g = ( u ( +g ` S ) v ) -> `' g = `' ( u ( +g ` S ) v ) )
134	133	imaeq1d 5161	. . . . . . . . 9 |- ( g = ( u ( +g ` S ) v ) -> ( `' g " ( _V \ { .0. } ) ) = ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) )
135	134	eleq1d 2470	. . . . . . . 8 |- ( g = ( u ( +g ` S ) v ) -> ( ( `' g " ( _V \ { .0. } ) ) e. A <-> ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) e. A ) )
136	135	elrab 3052	. . . . . . 7 |- ( ( u ( +g ` S ) v ) e. { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } <-> ( ( u ( +g ` S ) v ) e. B /\ ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) e. A ) )
137	132, 136	syl6bb 253	. . . . . 6 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( u ( +g ` S ) v ) e. U <-> ( ( u ( +g ` S ) v ) e. B /\ ( `' ( u ( +g ` S ) v ) " ( _V \ { .0. } ) ) e. A ) ) )
138	55, 130, 137	mpbir2and 889	. . . . 5 |- ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( u ( +g ` S ) v ) e. U )
139	138	ralrimiva 2749	. . . 4 |- ( ( ph /\ u e. U ) -> A. v e. U ( u ( +g ` S ) v ) e. U )
140	4, 5, 6	psrgrp 16417	. . . . . . 7 |- ( ph -> S e. Grp )
141		eqid 2404	. . . . . . . 8 |- ( inv g ` S ) = ( inv g ` S )
142	9, 141	grpinvcl 14805	. . . . . . 7 |- ( ( S e. Grp /\ u e. B ) -> ( ( inv g ` S ) ` u ) e. B )
143	140, 142	sylan 458	. . . . . 6 |- ( ( ph /\ u e. B ) -> ( ( inv g ` S ) ` u ) e. B )
144	44, 143	syldan 457	. . . . 5 |- ( ( ph /\ u e. U ) -> ( ( inv g ` S ) ` u ) e. B )
145	4, 11, 7, 9, 144	psrelbas 16399	. . . . . . . 8 |- ( ( ph /\ u e. U ) -> ( ( inv g ` S ) ` u ) : D --> ( Base ` R ) )
146	5	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ u e. U ) -> I e. W )
147	6	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ u e. U ) -> R e. Grp )
148		eqid 2404	. . . . . . . . . . . 12 |- ( inv g ` R ) = ( inv g ` R )
149	4, 146, 147, 7, 148, 9, 141, 44	psrneg 16419	. . . . . . . . . . 11 |- ( ( ph /\ u e. U ) -> ( ( inv g ` S ) ` u ) = ( ( inv g ` R ) o. u ) )
150	149	adantr 452	. . . . . . . . . 10 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( `' u " ( _V \ { .0. } ) ) ) ) -> ( ( inv g ` S ) ` u ) = ( ( inv g ` R ) o. u ) )
151	150	fveq1d 5689	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( `' u " ( _V \ { .0. } ) ) ) ) -> ( ( ( inv g ` S ) ` u ) ` k ) = ( ( ( inv g ` R ) o. u ) ` k ) )
152		eldifi 3429	. . . . . . . . . 10 |- ( k e. ( D \ ( `' u " ( _V \ { .0. } ) ) ) -> k e. D )
153		fvco3 5759	. . . . . . . . . 10 |- ( ( u : D --> ( Base ` R ) /\ k e. D ) -> ( ( ( inv g ` R ) o. u ) ` k ) = ( ( inv g ` R ) ` ( u ` k ) ) )
154	74, 152, 153	syl2an 464	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( `' u " ( _V \ { .0. } ) ) ) ) -> ( ( ( inv g ` R ) o. u ) ` k ) = ( ( inv g ` R ) ` ( u ` k ) ) )
155	96	fveq2d 5691	. . . . . . . . . 10 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( `' u " ( _V \ { .0. } ) ) ) ) -> ( ( inv g ` R ) ` ( u ` k ) ) = ( ( inv g ` R ) ` .0. ) )
156	8, 148	grpinvid 14811	. . . . . . . . . . . 12 |- ( R e. Grp -> ( ( inv g ` R ) ` .0. ) = .0. )
157	147, 156	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ u e. U ) -> ( ( inv g ` R ) ` .0. ) = .0. )
158	157	adantr 452	. . . . . . . . . 10 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( `' u " ( _V \ { .0. } ) ) ) ) -> ( ( inv g ` R ) ` .0. ) = .0. )
159	155, 158	eqtrd 2436	. . . . . . . . 9 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( `' u " ( _V \ { .0. } ) ) ) ) -> ( ( inv g ` R ) ` ( u ` k ) ) = .0. )
160	151, 154, 159	3eqtrd 2440	. . . . . . . 8 |- ( ( ( ph /\ u e. U ) /\ k e. ( D \ ( `' u " ( _V \ { .0. } ) ) ) ) -> ( ( ( inv g ` S ) ` u ) ` k ) = .0. )
161	145, 160	suppss 5822	. . . . . . 7 |- ( ( ph /\ u e. U ) -> ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) C_ ( `' u " ( _V \ { .0. } ) ) )
162	56, 161	ssexd 4310	. . . . . 6 |- ( ( ph /\ u e. U ) -> ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) e. _V )
163	119	adantr 452	. . . . . . 7 |- ( ( ph /\ u e. U ) -> A. x e. A A. y ( y C_ x -> y e. A ) )
164		sseq2 3330	. . . . . . . . . 10 |- ( x = ( `' u " ( _V \ { .0. } ) ) -> ( y C_ x <-> y C_ ( `' u " ( _V \ { .0. } ) ) ) )
165	164	imbi1d 309	. . . . . . . . 9 |- ( x = ( `' u " ( _V \ { .0. } ) ) -> ( ( y C_ x -> y e. A ) <-> ( y C_ ( `' u " ( _V \ { .0. } ) ) -> y e. A ) ) )
166	165	albidv 1632	. . . . . . . 8 |- ( x = ( `' u " ( _V \ { .0. } ) ) -> ( A. y ( y C_ x -> y e. A ) <-> A. y ( y C_ ( `' u " ( _V \ { .0. } ) ) -> y e. A ) ) )
167	166	rspcv 3008	. . . . . . 7 |- ( ( `' u " ( _V \ { .0. } ) ) e. A -> ( A. x e. A A. y ( y C_ x -> y e. A ) -> A. y ( y C_ ( `' u " ( _V \ { .0. } ) ) -> y e. A ) ) )
168	56, 163, 167	sylc 58	. . . . . 6 |- ( ( ph /\ u e. U ) -> A. y ( y C_ ( `' u " ( _V \ { .0. } ) ) -> y e. A ) )
169		sseq1 3329	. . . . . . . 8 |- ( y = ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) -> ( y C_ ( `' u " ( _V \ { .0. } ) ) <-> ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) C_ ( `' u " ( _V \ { .0. } ) ) ) )
170		eleq1 2464	. . . . . . . 8 |- ( y = ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) -> ( y e. A <-> ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) e. A ) )
171	169, 170	imbi12d 312	. . . . . . 7 |- ( y = ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) -> ( ( y C_ ( `' u " ( _V \ { .0. } ) ) -> y e. A ) <-> ( ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) C_ ( `' u " ( _V \ { .0. } ) ) -> ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) e. A ) ) )
172	171	spcgv 2996	. . . . . 6 |- ( ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) e. _V -> ( A. y ( y C_ ( `' u " ( _V \ { .0. } ) ) -> y e. A ) -> ( ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) C_ ( `' u " ( _V \ { .0. } ) ) -> ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) e. A ) ) )
173	162, 168, 161, 172	syl3c 59	. . . . 5 |- ( ( ph /\ u e. U ) -> ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) e. A )
174	46	eleq2d 2471	. . . . . 6 |- ( ( ph /\ u e. U ) -> ( ( ( inv g ` S ) ` u ) e. U <-> ( ( inv g ` S ) ` u ) e. { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } ) )
175		cnveq 5005	. . . . . . . . 9 |- ( g = ( ( inv g ` S ) ` u ) -> `' g = `' ( ( inv g ` S ) ` u ) )
176	175	imaeq1d 5161	. . . . . . . 8 |- ( g = ( ( inv g ` S ) ` u ) -> ( `' g " ( _V \ { .0. } ) ) = ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) )
177	176	eleq1d 2470	. . . . . . 7 |- ( g = ( ( inv g ` S ) ` u ) -> ( ( `' g " ( _V \ { .0. } ) ) e. A <-> ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) e. A ) )
178	177	elrab 3052	. . . . . 6 |- ( ( ( inv g ` S ) ` u ) e. { g e. B | ( `' g " ( _V \ { .0. } ) ) e. A } <-> ( ( ( inv g ` S ) ` u ) e. B /\ ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) e. A ) )
179	174, 178	syl6bb 253	. . . . 5 |- ( ( ph /\ u e. U ) -> ( ( ( inv g ` S ) ` u ) e. U <-> ( ( ( inv g ` S ) ` u ) e. B /\ ( `' ( ( inv g ` S ) ` u ) " ( _V \ { .0. } ) ) e. A ) ) )
180	144, 173, 179	mpbir2and 889	. . . 4 |- ( ( ph /\ u e. U ) -> ( ( inv g ` S ) ` u ) e. U )
181	139, 180	jca 519	. . 3 |- ( ( ph /\ u e. U ) -> ( A. v e. U ( u ( +g ` S ) v ) e. U /\ ( ( inv g ` S ) ` u ) e. U ) )
182	181	ralrimiva 2749	. 2 |- ( ph -> A. u e. U ( A. v e. U ( u ( +g ` S ) v ) e. U /\ ( ( inv g ` S ) ` u ) e. U ) )
183	9, 35, 141	issubg2 14914	. . 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 /\ ( ( inv g ` S ) ` u ) e. U ) ) ) )
184	140, 183	syl 16	. 2 |- ( ph -> ( U e. (SubGrp ` S ) <-> ( U C_ B /\ U =/= (/) /\ A. u e. U ( A. v e. U ( u ( +g ` S ) v ) e. U /\ ( ( inv g ` S ) ` u ) e. U ) ) ) )
185	3, 34, 182, 184	mpbir3and 1137	1 |- ( ph -> U e. (SubGrp ` S ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   A.wal 1546   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   {crab 2670   _Vcvv 2916   \ cdif 3277   u. cun 3278   C_ wss 3280   (/)c0 3588   {csn 3774   X. cxp 4835   `'ccnv 4836   "cima 4840   o. ccom 4841   Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040   o Fcof 6262   ^m cmap 6977   Fincfn 7068   NNcn 9956   NN0cn0 10177   Basecbs 13424   +g cplusg 13484   0gc0g 13678   Grpcgrp 14640   inv gcminusg 14641  SubGrpcsubg 14893   mPwSer cmps 16361

This theorem is referenced by:  mpllsslem  16454  mplsubg  16455

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-n0 10178  df-z 10239  df-uz 10445  df-fz 11000  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-sca 13500  df-vsca 13501  df-tset 13503  df-0g 13682  df-mnd 14645  df-grp 14767  df-minusg 14768  df-subg 14896  df-psr 16372