Theorem dmdprdsplit2lem 17671

Description: Lemma for dmdprdsplit 17673. (Contributed by Mario Carneiro, 26-Apr-2016.)

Hypotheses

Ref	Expression
dprdsplit.2	|- ( ph -> S : I --> (SubGrp ` G ) )
dprdsplit.i	|- ( ph -> ( C i^i D ) = (/) )
dprdsplit.u	|- ( ph -> I = ( C u. D ) )
dmdprdsplit.z	|- Z = (Cntz ` G )
dmdprdsplit.0	|- .0. = ( 0g ` G )
dmdprdsplit2.1	|- ( ph -> G dom DProd ( S |` C ) )
dmdprdsplit2.2	|- ( ph -> G dom DProd ( S |` D ) )
dmdprdsplit2.3	|- ( ph -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
dmdprdsplit2.4	|- ( ph -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )
dmdprdsplit2lem.k	|- K = (mrCls ` (SubGrp ` G ) )

Assertion

Ref	Expression
dmdprdsplit2lem	|- ( ( ph /\ X e. C ) -> ( ( Y e. I -> ( X =/= Y -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) ) /\ ( ( S ` X ) i^i ( K ` U. ( S " ( I \ { X } ) ) ) ) C_ { .0. } ) )

Proof of Theorem dmdprdsplit2lem

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dprdsplit.u	. . . . . 6 |- ( ph -> I = ( C u. D ) )
2	1	adantr 467	. . . . 5 |- ( ( ph /\ X e. C ) -> I = ( C u. D ) )
3	2	eleq2d 2493	. . . 4 |- ( ( ph /\ X e. C ) -> ( Y e. I <-> Y e. ( C u. D ) ) )
4		elun 3607	. . . 4 |- ( Y e. ( C u. D ) <-> ( Y e. C \/ Y e. D ) )
5	3, 4	syl6bb 265	. . 3 |- ( ( ph /\ X e. C ) -> ( Y e. I <-> ( Y e. C \/ Y e. D ) ) )
6		dmdprdsplit2.1	. . . . . . . 8 |- ( ph -> G dom DProd ( S |` C ) )
7	6	ad2antrr 731	. . . . . . 7 |- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> G dom DProd ( S |` C ) )
8		dprdsplit.2	. . . . . . . . . 10 |- ( ph -> S : I --> (SubGrp ` G ) )
9		ssun1 3630	. . . . . . . . . . 11 |- C C_ ( C u. D )
10	9, 1	syl5sseqr 3514	. . . . . . . . . 10 |- ( ph -> C C_ I )
11	8, 10	fssresd 5765	. . . . . . . . 9 |- ( ph -> ( S |` C ) : C --> (SubGrp ` G ) )
12		fdm 5748	. . . . . . . . 9 |- ( ( S |` C ) : C --> (SubGrp ` G ) -> dom ( S |` C ) = C )
13	11, 12	syl 17	. . . . . . . 8 |- ( ph -> dom ( S |` C ) = C )
14	13	ad2antrr 731	. . . . . . 7 |- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> dom ( S |` C ) = C )
15		simplr 761	. . . . . . 7 |- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> X e. C )
16		simprl 763	. . . . . . 7 |- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> Y e. C )
17		simprr 765	. . . . . . 7 |- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> X =/= Y )
18		dmdprdsplit.z	. . . . . . 7 |- Z = (Cntz ` G )
19	7, 14, 15, 16, 17, 18	dprdcntz 17633	. . . . . 6 |- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> ( ( S |` C ) ` X ) C_ ( Z ` ( ( S |` C ) ` Y ) ) )
20		fvres 5893	. . . . . . 7 |- ( X e. C -> ( ( S |` C ) ` X ) = ( S ` X ) )
21	20	ad2antlr 732	. . . . . 6 |- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> ( ( S |` C ) ` X ) = ( S ` X ) )
22		fvres 5893	. . . . . . . 8 |- ( Y e. C -> ( ( S |` C ) ` Y ) = ( S ` Y ) )
23	22	ad2antrl 733	. . . . . . 7 |- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> ( ( S |` C ) ` Y ) = ( S ` Y ) )
24	23	fveq2d 5883	. . . . . 6 |- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> ( Z ` ( ( S |` C ) ` Y ) ) = ( Z ` ( S ` Y ) ) )
25	19, 21, 24	3sstr3d 3507	. . . . 5 |- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) )
26	25	exp32 609	. . . 4 |- ( ( ph /\ X e. C ) -> ( Y e. C -> ( X =/= Y -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) ) )
27	20	ad2antlr 732	. . . . . . 7 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( ( S |` C ) ` X ) = ( S ` X ) )
28	6	ad2antrr 731	. . . . . . . 8 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> G dom DProd ( S |` C ) )
29	13	ad2antrr 731	. . . . . . . 8 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> dom ( S |` C ) = C )
30		simplr 761	. . . . . . . 8 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> X e. C )
31	28, 29, 30	dprdub 17651	. . . . . . 7 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( ( S |` C ) ` X ) C_ ( G DProd ( S |` C ) ) )
32	27, 31	eqsstr3d 3500	. . . . . 6 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( S ` X ) C_ ( G DProd ( S |` C ) ) )
33		dmdprdsplit2.3	. . . . . . . 8 |- ( ph -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
34	33	ad2antrr 731	. . . . . . 7 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
35		eqid 2423	. . . . . . . . 9 |- ( Base ` G ) = ( Base ` G )
36	35	dprdssv 17642	. . . . . . . 8 |- ( G DProd ( S |` D ) ) C_ ( Base ` G )
37		fvres 5893	. . . . . . . . . 10 |- ( Y e. D -> ( ( S |` D ) ` Y ) = ( S ` Y ) )
38	37	ad2antrl 733	. . . . . . . . 9 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( ( S |` D ) ` Y ) = ( S ` Y ) )
39		dmdprdsplit2.2	. . . . . . . . . . 11 |- ( ph -> G dom DProd ( S |` D ) )
40	39	ad2antrr 731	. . . . . . . . . 10 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> G dom DProd ( S |` D ) )
41		ssun2 3631	. . . . . . . . . . . . . 14 |- D C_ ( C u. D )
42	41, 1	syl5sseqr 3514	. . . . . . . . . . . . 13 |- ( ph -> D C_ I )
43	8, 42	fssresd 5765	. . . . . . . . . . . 12 |- ( ph -> ( S |` D ) : D --> (SubGrp ` G ) )
44		fdm 5748	. . . . . . . . . . . 12 |- ( ( S |` D ) : D --> (SubGrp ` G ) -> dom ( S |` D ) = D )
45	43, 44	syl 17	. . . . . . . . . . 11 |- ( ph -> dom ( S |` D ) = D )
46	45	ad2antrr 731	. . . . . . . . . 10 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> dom ( S |` D ) = D )
47		simprl 763	. . . . . . . . . 10 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> Y e. D )
48	40, 46, 47	dprdub 17651	. . . . . . . . 9 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( ( S |` D ) ` Y ) C_ ( G DProd ( S |` D ) ) )
49	38, 48	eqsstr3d 3500	. . . . . . . 8 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( S ` Y ) C_ ( G DProd ( S |` D ) ) )
50	35, 18	cntz2ss 16979	. . . . . . . 8 |- ( ( ( G DProd ( S |` D ) ) C_ ( Base ` G ) /\ ( S ` Y ) C_ ( G DProd ( S |` D ) ) ) -> ( Z ` ( G DProd ( S |` D ) ) ) C_ ( Z ` ( S ` Y ) ) )
51	36, 49, 50	sylancr 668	. . . . . . 7 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( Z ` ( G DProd ( S |` D ) ) ) C_ ( Z ` ( S ` Y ) ) )
52	34, 51	sstrd 3475	. . . . . 6 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( G DProd ( S |` C ) ) C_ ( Z ` ( S ` Y ) ) )
53	32, 52	sstrd 3475	. . . . 5 |- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) )
54	53	exp32 609	. . . 4 |- ( ( ph /\ X e. C ) -> ( Y e. D -> ( X =/= Y -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) ) )
55	26, 54	jaod 382	. . 3 |- ( ( ph /\ X e. C ) -> ( ( Y e. C \/ Y e. D ) -> ( X =/= Y -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) ) )
56	5, 55	sylbid 219	. 2 |- ( ( ph /\ X e. C ) -> ( Y e. I -> ( X =/= Y -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) ) )
57		dprdgrp 17630	. . . . . . . 8 |- ( G dom DProd ( S |` C ) -> G e. Grp )
58	6, 57	syl 17	. . . . . . 7 |- ( ph -> G e. Grp )
59	58	adantr 467	. . . . . 6 |- ( ( ph /\ X e. C ) -> G e. Grp )
60	35	subgacs 16845	. . . . . 6 |- ( G e. Grp -> (SubGrp ` G ) e. (ACS ` ( Base ` G ) ) )
61		acsmre 15551	. . . . . 6 |- ( (SubGrp ` G ) e. (ACS ` ( Base ` G ) ) -> (SubGrp ` G ) e. (Moore ` ( Base ` G ) ) )
62	59, 60, 61	3syl 18	. . . . 5 |- ( ( ph /\ X e. C ) -> (SubGrp ` G ) e. (Moore ` ( Base ` G ) ) )
63		difundir 3727	. . . . . . . . . . 11 |- ( ( C u. D ) \ { X } ) = ( ( C \ { X } ) u. ( D \ { X } ) )
64	2	difeq1d 3583	. . . . . . . . . . 11 |- ( ( ph /\ X e. C ) -> ( I \ { X } ) = ( ( C u. D ) \ { X } ) )
65		simpr 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ X e. C ) -> X e. C )
66	65	snssd 4143	. . . . . . . . . . . . . . 15 |- ( ( ph /\ X e. C ) -> { X } C_ C )
67		sslin 3689	. . . . . . . . . . . . . . 15 |- ( { X } C_ C -> ( D i^i { X } ) C_ ( D i^i C ) )
68	66, 67	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ X e. C ) -> ( D i^i { X } ) C_ ( D i^i C ) )
69		incom 3656	. . . . . . . . . . . . . . 15 |- ( C i^i D ) = ( D i^i C )
70		dprdsplit.i	. . . . . . . . . . . . . . . 16 |- ( ph -> ( C i^i D ) = (/) )
71	70	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ X e. C ) -> ( C i^i D ) = (/) )
72	69, 71	syl5eqr 2478	. . . . . . . . . . . . . 14 |- ( ( ph /\ X e. C ) -> ( D i^i C ) = (/) )
73		sseq0 3795	. . . . . . . . . . . . . 14 |- ( ( ( D i^i { X } ) C_ ( D i^i C ) /\ ( D i^i C ) = (/) ) -> ( D i^i { X } ) = (/) )
74	68, 72, 73	syl2anc 666	. . . . . . . . . . . . 13 |- ( ( ph /\ X e. C ) -> ( D i^i { X } ) = (/) )
75		disj3 3838	. . . . . . . . . . . . 13 |- ( ( D i^i { X } ) = (/) <-> D = ( D \ { X } ) )
76	74, 75	sylib 200	. . . . . . . . . . . 12 |- ( ( ph /\ X e. C ) -> D = ( D \ { X } ) )
77	76	uneq2d 3621	. . . . . . . . . . 11 |- ( ( ph /\ X e. C ) -> ( ( C \ { X } ) u. D ) = ( ( C \ { X } ) u. ( D \ { X } ) ) )
78	63, 64, 77	3eqtr4a 2490	. . . . . . . . . 10 |- ( ( ph /\ X e. C ) -> ( I \ { X } ) = ( ( C \ { X } ) u. D ) )
79	78	imaeq2d 5185	. . . . . . . . 9 |- ( ( ph /\ X e. C ) -> ( S " ( I \ { X } ) ) = ( S " ( ( C \ { X } ) u. D ) ) )
80		imaundi 5265	. . . . . . . . 9 |- ( S " ( ( C \ { X } ) u. D ) ) = ( ( S " ( C \ { X } ) ) u. ( S " D ) )
81	79, 80	syl6eq 2480	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> ( S " ( I \ { X } ) ) = ( ( S " ( C \ { X } ) ) u. ( S " D ) ) )
82	81	unieqd 4227	. . . . . . 7 |- ( ( ph /\ X e. C ) -> U. ( S " ( I \ { X } ) ) = U. ( ( S " ( C \ { X } ) ) u. ( S " D ) ) )
83		uniun 4236	. . . . . . 7 |- U. ( ( S " ( C \ { X } ) ) u. ( S " D ) ) = ( U. ( S " ( C \ { X } ) ) u. U. ( S " D ) )
84	82, 83	syl6eq 2480	. . . . . 6 |- ( ( ph /\ X e. C ) -> U. ( S " ( I \ { X } ) ) = ( U. ( S " ( C \ { X } ) ) u. U. ( S " D ) ) )
85		dmdprdsplit2lem.k	. . . . . . . . 9 |- K = (mrCls ` (SubGrp ` G ) )
86		difss 3593	. . . . . . . . . . 11 |- ( C \ { X } ) C_ C
87		imass2 5221	. . . . . . . . . . 11 |- ( ( C \ { X } ) C_ C -> ( S " ( C \ { X } ) ) C_ ( S " C ) )
88		uniss 4238	. . . . . . . . . . 11 |- ( ( S " ( C \ { X } ) ) C_ ( S " C ) -> U. ( S " ( C \ { X } ) ) C_ U. ( S " C ) )
89	86, 87, 88	mp2b 10	. . . . . . . . . 10 |- U. ( S " ( C \ { X } ) ) C_ U. ( S " C )
90		imassrn 5196	. . . . . . . . . . . 12 |- ( S " C ) C_ ran S
91		frn 5750	. . . . . . . . . . . . . . 15 |- ( S : I --> (SubGrp ` G ) -> ran S C_ (SubGrp ` G ) )
92	8, 91	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ran S C_ (SubGrp ` G ) )
93	92	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ X e. C ) -> ran S C_ (SubGrp ` G ) )
94		mresspw 15491	. . . . . . . . . . . . . 14 |- ( (SubGrp ` G ) e. (Moore ` ( Base ` G ) ) -> (SubGrp ` G ) C_ ~P ( Base ` G ) )
95	62, 94	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ X e. C ) -> (SubGrp ` G ) C_ ~P ( Base ` G ) )
96	93, 95	sstrd 3475	. . . . . . . . . . . 12 |- ( ( ph /\ X e. C ) -> ran S C_ ~P ( Base ` G ) )
97	90, 96	syl5ss 3476	. . . . . . . . . . 11 |- ( ( ph /\ X e. C ) -> ( S " C ) C_ ~P ( Base ` G ) )
98		sspwuni 4386	. . . . . . . . . . 11 |- ( ( S " C ) C_ ~P ( Base ` G ) <-> U. ( S " C ) C_ ( Base ` G ) )
99	97, 98	sylib 200	. . . . . . . . . 10 |- ( ( ph /\ X e. C ) -> U. ( S " C ) C_ ( Base ` G ) )
100	89, 99	syl5ss 3476	. . . . . . . . 9 |- ( ( ph /\ X e. C ) -> U. ( S " ( C \ { X } ) ) C_ ( Base ` G ) )
101	62, 85, 100	mrcssidd 15524	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> U. ( S " ( C \ { X } ) ) C_ ( K ` U. ( S " ( C \ { X } ) ) ) )
102		imassrn 5196	. . . . . . . . . . . 12 |- ( S " D ) C_ ran S
103	102, 96	syl5ss 3476	. . . . . . . . . . 11 |- ( ( ph /\ X e. C ) -> ( S " D ) C_ ~P ( Base ` G ) )
104		sspwuni 4386	. . . . . . . . . . 11 |- ( ( S " D ) C_ ~P ( Base ` G ) <-> U. ( S " D ) C_ ( Base ` G ) )
105	103, 104	sylib 200	. . . . . . . . . 10 |- ( ( ph /\ X e. C ) -> U. ( S " D ) C_ ( Base ` G ) )
106	62, 85, 105	mrcssidd 15524	. . . . . . . . 9 |- ( ( ph /\ X e. C ) -> U. ( S " D ) C_ ( K ` U. ( S " D ) ) )
107	85	dprdspan 17653	. . . . . . . . . . . 12 |- ( G dom DProd ( S |` D ) -> ( G DProd ( S |` D ) ) = ( K ` U. ran ( S |` D ) ) )
108	39, 107	syl 17	. . . . . . . . . . 11 |- ( ph -> ( G DProd ( S |` D ) ) = ( K ` U. ran ( S |` D ) ) )
109		df-ima 4864	. . . . . . . . . . . . 13 |- ( S " D ) = ran ( S |` D )
110	109	unieqi 4226	. . . . . . . . . . . 12 |- U. ( S " D ) = U. ran ( S |` D )
111	110	fveq2i 5882	. . . . . . . . . . 11 |- ( K ` U. ( S " D ) ) = ( K ` U. ran ( S |` D ) )
112	108, 111	syl6eqr 2482	. . . . . . . . . 10 |- ( ph -> ( G DProd ( S |` D ) ) = ( K ` U. ( S " D ) ) )
113	112	adantr 467	. . . . . . . . 9 |- ( ( ph /\ X e. C ) -> ( G DProd ( S |` D ) ) = ( K ` U. ( S " D ) ) )
114	106, 113	sseqtr4d 3502	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> U. ( S " D ) C_ ( G DProd ( S |` D ) ) )
115		unss12 3639	. . . . . . . 8 |- ( ( U. ( S " ( C \ { X } ) ) C_ ( K ` U. ( S " ( C \ { X } ) ) ) /\ U. ( S " D ) C_ ( G DProd ( S |` D ) ) ) -> ( U. ( S " ( C \ { X } ) ) u. U. ( S " D ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) u. ( G DProd ( S |` D ) ) ) )
116	101, 114, 115	syl2anc 666	. . . . . . 7 |- ( ( ph /\ X e. C ) -> ( U. ( S " ( C \ { X } ) ) u. U. ( S " D ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) u. ( G DProd ( S |` D ) ) ) )
117	85	mrccl 15510	. . . . . . . . 9 |- ( ( (SubGrp ` G ) e. (Moore ` ( Base ` G ) ) /\ U. ( S " ( C \ { X } ) ) C_ ( Base ` G ) ) -> ( K ` U. ( S " ( C \ { X } ) ) ) e. (SubGrp ` G ) )
118	62, 100, 117	syl2anc 666	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> ( K ` U. ( S " ( C \ { X } ) ) ) e. (SubGrp ` G ) )
119		dprdsubg 17650	. . . . . . . . . 10 |- ( G dom DProd ( S |` D ) -> ( G DProd ( S |` D ) ) e. (SubGrp ` G ) )
120	39, 119	syl 17	. . . . . . . . 9 |- ( ph -> ( G DProd ( S |` D ) ) e. (SubGrp ` G ) )
121	120	adantr 467	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> ( G DProd ( S |` D ) ) e. (SubGrp ` G ) )
122		eqid 2423	. . . . . . . . 9 |- ( LSSum ` G ) = ( LSSum ` G )
123	122	lsmunss 17303	. . . . . . . 8 |- ( ( ( K ` U. ( S " ( C \ { X } ) ) ) e. (SubGrp ` G ) /\ ( G DProd ( S |` D ) ) e. (SubGrp ` G ) ) -> ( ( K ` U. ( S " ( C \ { X } ) ) ) u. ( G DProd ( S |` D ) ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) )
124	118, 121, 123	syl2anc 666	. . . . . . 7 |- ( ( ph /\ X e. C ) -> ( ( K ` U. ( S " ( C \ { X } ) ) ) u. ( G DProd ( S |` D ) ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) )
125	116, 124	sstrd 3475	. . . . . 6 |- ( ( ph /\ X e. C ) -> ( U. ( S " ( C \ { X } ) ) u. U. ( S " D ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) )
126	84, 125	eqsstrd 3499	. . . . 5 |- ( ( ph /\ X e. C ) -> U. ( S " ( I \ { X } ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) )
127	89	a1i 11	. . . . . . . . 9 |- ( ( ph /\ X e. C ) -> U. ( S " ( C \ { X } ) ) C_ U. ( S " C ) )
128	62, 85, 127, 99	mrcssd 15523	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> ( K ` U. ( S " ( C \ { X } ) ) ) C_ ( K ` U. ( S " C ) ) )
129	85	dprdspan 17653	. . . . . . . . . . 11 |- ( G dom DProd ( S |` C ) -> ( G DProd ( S |` C ) ) = ( K ` U. ran ( S |` C ) ) )
130	6, 129	syl 17	. . . . . . . . . 10 |- ( ph -> ( G DProd ( S |` C ) ) = ( K ` U. ran ( S |` C ) ) )
131		df-ima 4864	. . . . . . . . . . . 12 |- ( S " C ) = ran ( S |` C )
132	131	unieqi 4226	. . . . . . . . . . 11 |- U. ( S " C ) = U. ran ( S |` C )
133	132	fveq2i 5882	. . . . . . . . . 10 |- ( K ` U. ( S " C ) ) = ( K ` U. ran ( S |` C ) )
134	130, 133	syl6eqr 2482	. . . . . . . . 9 |- ( ph -> ( G DProd ( S |` C ) ) = ( K ` U. ( S " C ) ) )
135	134	adantr 467	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> ( G DProd ( S |` C ) ) = ( K ` U. ( S " C ) ) )
136	128, 135	sseqtr4d 3502	. . . . . . 7 |- ( ( ph /\ X e. C ) -> ( K ` U. ( S " ( C \ { X } ) ) ) C_ ( G DProd ( S |` C ) ) )
137	33	adantr 467	. . . . . . 7 |- ( ( ph /\ X e. C ) -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
138	136, 137	sstrd 3475	. . . . . 6 |- ( ( ph /\ X e. C ) -> ( K ` U. ( S " ( C \ { X } ) ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
139	122, 18	lsmsubg 17299	. . . . . 6 |- ( ( ( K ` U. ( S " ( C \ { X } ) ) ) e. (SubGrp ` G ) /\ ( G DProd ( S |` D ) ) e. (SubGrp ` G ) /\ ( K ` U. ( S " ( C \ { X } ) ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) ) -> ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) e. (SubGrp ` G ) )
140	118, 121, 138, 139	syl3anc 1265	. . . . 5 |- ( ( ph /\ X e. C ) -> ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) e. (SubGrp ` G ) )
141	85	mrcsscl 15519	. . . . 5 |- ( ( (SubGrp ` G ) e. (Moore ` ( Base ` G ) ) /\ U. ( S " ( I \ { X } ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) /\ ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) e. (SubGrp ` G ) ) -> ( K ` U. ( S " ( I \ { X } ) ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) )
142	62, 126, 140, 141	syl3anc 1265	. . . 4 |- ( ( ph /\ X e. C ) -> ( K ` U. ( S " ( I \ { X } ) ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) )
143		sslin 3689	. . . 4 |- ( ( K ` U. ( S " ( I \ { X } ) ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) -> ( ( S ` X ) i^i ( K ` U. ( S " ( I \ { X } ) ) ) ) C_ ( ( S ` X ) i^i ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) ) )
144	142, 143	syl 17	. . 3 |- ( ( ph /\ X e. C ) -> ( ( S ` X ) i^i ( K ` U. ( S " ( I \ { X } ) ) ) ) C_ ( ( S ` X ) i^i ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) ) )
145	10	sselda 3465	. . . . 5 |- ( ( ph /\ X e. C ) -> X e. I )
146	8	ffvelrnda 6035	. . . . 5 |- ( ( ph /\ X e. I ) -> ( S ` X ) e. (SubGrp ` G ) )
147	145, 146	syldan 473	. . . 4 |- ( ( ph /\ X e. C ) -> ( S ` X ) e. (SubGrp ` G ) )
148		dmdprdsplit.0	. . . 4 |- .0. = ( 0g ` G )
149	20	adantl 468	. . . . . . . . 9 |- ( ( ph /\ X e. C ) -> ( ( S |` C ) ` X ) = ( S ` X ) )
150	6	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ X e. C ) -> G dom DProd ( S |` C ) )
151	13	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ X e. C ) -> dom ( S |` C ) = C )
152	150, 151, 65	dprdub 17651	. . . . . . . . 9 |- ( ( ph /\ X e. C ) -> ( ( S |` C ) ` X ) C_ ( G DProd ( S |` C ) ) )
153	149, 152	eqsstr3d 3500	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> ( S ` X ) C_ ( G DProd ( S |` C ) ) )
154		dprdsubg 17650	. . . . . . . . . . 11 |- ( G dom DProd ( S |` C ) -> ( G DProd ( S |` C ) ) e. (SubGrp ` G ) )
155	6, 154	syl 17	. . . . . . . . . 10 |- ( ph -> ( G DProd ( S |` C ) ) e. (SubGrp ` G ) )
156	155	adantr 467	. . . . . . . . 9 |- ( ( ph /\ X e. C ) -> ( G DProd ( S |` C ) ) e. (SubGrp ` G ) )
157	122	lsmlub 17308	. . . . . . . . 9 |- ( ( ( S ` X ) e. (SubGrp ` G ) /\ ( K ` U. ( S " ( C \ { X } ) ) ) e. (SubGrp ` G ) /\ ( G DProd ( S |` C ) ) e. (SubGrp ` G ) ) -> ( ( ( S ` X ) C_ ( G DProd ( S |` C ) ) /\ ( K ` U. ( S " ( C \ { X } ) ) ) C_ ( G DProd ( S |` C ) ) ) <-> ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) C_ ( G DProd ( S |` C ) ) ) )
158	147, 118, 156, 157	syl3anc 1265	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> ( ( ( S ` X ) C_ ( G DProd ( S |` C ) ) /\ ( K ` U. ( S " ( C \ { X } ) ) ) C_ ( G DProd ( S |` C ) ) ) <-> ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) C_ ( G DProd ( S |` C ) ) ) )
159	153, 136, 158	mpbi2and 930	. . . . . . 7 |- ( ( ph /\ X e. C ) -> ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) C_ ( G DProd ( S |` C ) ) )
160		ssrin 3688	. . . . . . 7 |- ( ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) C_ ( G DProd ( S |` C ) ) -> ( ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) i^i ( G DProd ( S |` D ) ) ) C_ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) )
161	159, 160	syl 17	. . . . . 6 |- ( ( ph /\ X e. C ) -> ( ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) i^i ( G DProd ( S |` D ) ) ) C_ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) )
162		dmdprdsplit2.4	. . . . . . 7 |- ( ph -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )
163	162	adantr 467	. . . . . 6 |- ( ( ph /\ X e. C ) -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )
164	161, 163	sseqtrd 3501	. . . . 5 |- ( ( ph /\ X e. C ) -> ( ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) i^i ( G DProd ( S |` D ) ) ) C_ { .0. } )
165	122	lsmub1 17301	. . . . . . . . 9 |- ( ( ( S ` X ) e. (SubGrp ` G ) /\ ( K ` U. ( S " ( C \ { X } ) ) ) e. (SubGrp ` G ) ) -> ( S ` X ) C_ ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) )
166	147, 118, 165	syl2anc 666	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> ( S ` X ) C_ ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) )
167	148	subg0cl 16818	. . . . . . . . 9 |- ( ( S ` X ) e. (SubGrp ` G ) -> .0. e. ( S ` X ) )
168	147, 167	syl 17	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> .0. e. ( S ` X ) )
169	166, 168	sseldd 3466	. . . . . . 7 |- ( ( ph /\ X e. C ) -> .0. e. ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) )
170	148	subg0cl 16818	. . . . . . . 8 |- ( ( G DProd ( S |` D ) ) e. (SubGrp ` G ) -> .0. e. ( G DProd ( S |` D ) ) )
171	121, 170	syl 17	. . . . . . 7 |- ( ( ph /\ X e. C ) -> .0. e. ( G DProd ( S |` D ) ) )
172	169, 171	elind 3651	. . . . . 6 |- ( ( ph /\ X e. C ) -> .0. e. ( ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) i^i ( G DProd ( S |` D ) ) ) )
173	172	snssd 4143	. . . . 5 |- ( ( ph /\ X e. C ) -> { .0. } C_ ( ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) i^i ( G DProd ( S |` D ) ) ) )
174	164, 173	eqssd 3482	. . . 4 |- ( ( ph /\ X e. C ) -> ( ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )
175		resima2 5155	. . . . . . . . 9 |- ( ( C \ { X } ) C_ C -> ( ( S |` C ) " ( C \ { X } ) ) = ( S " ( C \ { X } ) ) )
176	86, 175	mp1i 13	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> ( ( S |` C ) " ( C \ { X } ) ) = ( S " ( C \ { X } ) ) )
177	176	unieqd 4227	. . . . . . 7 |- ( ( ph /\ X e. C ) -> U. ( ( S |` C ) " ( C \ { X } ) ) = U. ( S " ( C \ { X } ) ) )
178	177	fveq2d 5883	. . . . . 6 |- ( ( ph /\ X e. C ) -> ( K ` U. ( ( S |` C ) " ( C \ { X } ) ) ) = ( K ` U. ( S " ( C \ { X } ) ) ) )
179	149, 178	ineq12d 3666	. . . . 5 |- ( ( ph /\ X e. C ) -> ( ( ( S |` C ) ` X ) i^i ( K ` U. ( ( S |` C ) " ( C \ { X } ) ) ) ) = ( ( S ` X ) i^i ( K ` U. ( S " ( C \ { X } ) ) ) ) )
180	150, 151, 65, 148, 85	dprddisj 17634	. . . . 5 |- ( ( ph /\ X e. C ) -> ( ( ( S |` C ) ` X ) i^i ( K ` U. ( ( S |` C ) " ( C \ { X } ) ) ) ) = { .0. } )
181	179, 180	eqtr3d 2466	. . . 4 |- ( ( ph /\ X e. C ) -> ( ( S ` X ) i^i ( K ` U. ( S " ( C \ { X } ) ) ) ) = { .0. } )
182	8	adantr 467	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> S : I --> (SubGrp ` G ) )
183		ffun 5746	. . . . . . . 8 |- ( S : I --> (SubGrp ` G ) -> Fun S )
184		funiunfv 6166	. . . . . . . 8 |- ( Fun S -> U_ y e. ( C \ { X } ) ( S ` y ) = U. ( S " ( C \ { X } ) ) )
185	182, 183, 184	3syl 18	. . . . . . 7 |- ( ( ph /\ X e. C ) -> U_ y e. ( C \ { X } ) ( S ` y ) = U. ( S " ( C \ { X } ) ) )
186	6	ad2antrr 731	. . . . . . . . . . 11 |- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> G dom DProd ( S |` C ) )
187	13	ad2antrr 731	. . . . . . . . . . 11 |- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> dom ( S |` C ) = C )
188		eldifi 3588	. . . . . . . . . . . 12 |- ( y e. ( C \ { X } ) -> y e. C )
189	188	adantl 468	. . . . . . . . . . 11 |- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> y e. C )
190		simplr 761	. . . . . . . . . . 11 |- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> X e. C )
191		eldifsni 4124	. . . . . . . . . . . 12 |- ( y e. ( C \ { X } ) -> y =/= X )
192	191	adantl 468	. . . . . . . . . . 11 |- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> y =/= X )
193	186, 187, 189, 190, 192, 18	dprdcntz 17633	. . . . . . . . . 10 |- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> ( ( S |` C ) ` y ) C_ ( Z ` ( ( S |` C ) ` X ) ) )
194		fvres 5893	. . . . . . . . . . 11 |- ( y e. C -> ( ( S |` C ) ` y ) = ( S ` y ) )
195	189, 194	syl 17	. . . . . . . . . 10 |- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> ( ( S |` C ) ` y ) = ( S ` y ) )
196	20	ad2antlr 732	. . . . . . . . . . 11 |- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> ( ( S |` C ) ` X ) = ( S ` X ) )
197	196	fveq2d 5883	. . . . . . . . . 10 |- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> ( Z ` ( ( S |` C ) ` X ) ) = ( Z ` ( S ` X ) ) )
198	193, 195, 197	3sstr3d 3507	. . . . . . . . 9 |- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> ( S ` y ) C_ ( Z ` ( S ` X ) ) )
199	198	ralrimiva 2840	. . . . . . . 8 |- ( ( ph /\ X e. C ) -> A. y e. ( C \ { X } ) ( S ` y ) C_ ( Z ` ( S ` X ) ) )
200		iunss 4338	. . . . . . . 8 |- ( U_ y e. ( C \ { X } ) ( S ` y ) C_ ( Z ` ( S ` X ) ) <-> A. y e. ( C \ { X } ) ( S ` y ) C_ ( Z ` ( S ` X ) ) )
201	199, 200	sylibr 216	. . . . . . 7 |- ( ( ph /\ X e. C ) -> U_ y e. ( C \ { X } ) ( S ` y ) C_ ( Z ` ( S ` X ) ) )
202	185, 201	eqsstr3d 3500	. . . . . 6 |- ( ( ph /\ X e. C ) -> U. ( S " ( C \ { X } ) ) C_ ( Z ` ( S ` X ) ) )
203	35	subgss 16811	. . . . . . . 8 |- ( ( S ` X ) e. (SubGrp ` G ) -> ( S ` X ) C_ ( Base ` G ) )
204	147, 203	syl 17	. . . . . . 7 |- ( ( ph /\ X e. C ) -> ( S ` X ) C_ ( Base ` G ) )
205	35, 18	cntzsubg 16983	. . . . . . 7 |- ( ( G e. Grp /\ ( S ` X ) C_ ( Base ` G ) ) -> ( Z ` ( S ` X ) ) e. (SubGrp ` G ) )
206	59, 204, 205	syl2anc 666	. . . . . 6 |- ( ( ph /\ X e. C ) -> ( Z ` ( S ` X ) ) e. (SubGrp ` G ) )
207	85	mrcsscl 15519	. . . . . 6 |- ( ( (SubGrp ` G ) e. (Moore ` ( Base ` G ) ) /\ U. ( S " ( C \ { X } ) ) C_ ( Z ` ( S ` X ) ) /\ ( Z ` ( S ` X ) ) e. (SubGrp ` G ) ) -> ( K ` U. ( S " ( C \ { X } ) ) ) C_ ( Z ` ( S ` X ) ) )
208	62, 202, 206, 207	syl3anc 1265	. . . . 5 |- ( ( ph /\ X e. C ) -> ( K ` U. ( S " ( C \ { X } ) ) ) C_ ( Z ` ( S ` X ) ) )
209	18, 118, 147, 208	cntzrecd 17321	. . . 4 |- ( ( ph /\ X e. C ) -> ( S ` X ) C_ ( Z ` ( K ` U. ( S " ( C \ { X } ) ) ) ) )
210	122, 147, 118, 121, 148, 174, 181, 18, 209	lsmdisj3 17326	. . 3 |- ( ( ph /\ X e. C ) -> ( ( S ` X ) i^i ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) ) = { .0. } )
211	144, 210	sseqtrd 3501	. 2 |- ( ( ph /\ X e. C ) -> ( ( S ` X ) i^i ( K ` U. ( S " ( I \ { X } ) ) ) ) C_ { .0. } )
212	56, 211	jca 535	1 |- ( ( ph /\ X e. C ) -> ( ( Y e. I -> ( X =/= Y -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) ) /\ ( ( S ` X ) i^i ( K ` U. ( S " ( I \ { X } ) ) ) ) C_ { .0. } ) )

Syntax hints:   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   = wceq 1438   e. wcel 1869   =/= wne 2619   A.wral 2776   \ cdif 3434   u. cun 3435   i^i cin 3436   C_ wss 3437   (/)c0 3762   ~Pcpw 3980   {csn 3997   U.cuni 4217   U_ciun 4297   class class class wbr 4421   dom cdm 4851   ran crn 4852   |` cres 4853   "cima 4854   Fun wfun 5593   -->wf 5595   ` cfv 5599  (class class class)co 6303   Basecbs 15114   0gc0g 15331  Moorecmre 15481  mrClscmrc 15482  ACScacs 15484   Grpcgrp 16662  SubGrpcsubg 16804  Cntzccntz 16962   LSSumclsm 17279   DProd cdprd 17618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-inf2 8150  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-iin 4300  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-se 4811  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-isom 5608  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-of 6543  df-om 6705  df-1st 6805  df-2nd 6806  df-supp 6924  df-tpos 6979  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-oadd 7192  df-er 7369  df-map 7480  df-ixp 7529  df-en 7576  df-dom 7577  df-sdom 7578  df-fin 7579  df-fsupp 7888  df-oi 8029  df-card 8376  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-nn 10612  df-2 10670  df-n0 10872  df-z 10940  df-uz 11162  df-fz 11787  df-fzo 11918  df-seq 12215  df-hash 12517  df-ndx 15117  df-slot 15118  df-base 15119  df-sets 15120  df-ress 15121  df-plusg 15196  df-0g 15333  df-gsum 15334  df-mre 15485  df-mrc 15486  df-acs 15488  df-mgm 16481  df-sgrp 16520  df-mnd 16530  df-mhm 16575  df-submnd 16576  df-grp 16666  df-minusg 16667  df-sbg 16668  df-mulg 16669  df-subg 16807  df-ghm 16874  df-gim 16916  df-cntz 16964  df-oppg 16990  df-lsm 17281  df-cmn 17425  df-dprd 17620

This theorem is referenced by:  dmdprdsplit2  17672