Theorem dmdprdsplit2lem

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

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

Step	Hyp	Ref	Expression
1		dprdsplit.2	|- ( ph -> S : I --> ( SubGrp ` G ) )
2		dprdsplit.i	|- ( ph -> ( C i^i D ) = (/) )
3		dprdsplit.u	|- ( ph -> I = ( C u. D ) )
4		dmdprdsplit.z	|- Z = ( Cntz ` G )
5		dmdprdsplit.0	|- .0. = ( 0g ` G )
6		dmdprdsplit2.1	|- ( ph -> G dom DProd ( S |` C ) )
7		dmdprdsplit2.2	|- ( ph -> G dom DProd ( S |` D ) )
8		dmdprdsplit2.3	|- ( ph -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
9		dmdprdsplit2.4	|- ( ph -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )
10		dmdprdsplit2lem.k	|- K = ( mrCls ` ( SubGrp ` G ) )
11	3	adantr	|- ( ( ph /\ X e. C ) -> I = ( C u. D ) )
12	11	eleq2d	|- ( ( ph /\ X e. C ) -> ( Y e. I <-> Y e. ( C u. D ) ) )
13		elun	|- ( Y e. ( C u. D ) <-> ( Y e. C \/ Y e. D ) )
14	12 13	bitrdi	|- ( ( ph /\ X e. C ) -> ( Y e. I <-> ( Y e. C \/ Y e. D ) ) )
15	6	ad2antrr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> G dom DProd ( S |` C ) )
16		ssun1	|- C C_ ( C u. D )
17	16 3	sseqtrrid	|- ( ph -> C C_ I )
18	1 17	fssresd	|- ( ph -> ( S |` C ) : C --> ( SubGrp ` G ) )
19	18	fdmd	|- ( ph -> dom ( S |` C ) = C )
20	19	ad2antrr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> dom ( S |` C ) = C )
21		simplr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> X e. C )
22		simprl	|- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> Y e. C )
23		simprr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> X =/= Y )
24	15 20 21 22 23 4	dprdcntz	|- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> ( ( S |` C ) ` X ) C_ ( Z ` ( ( S |` C ) ` Y ) ) )
25		fvres	|- ( X e. C -> ( ( S |` C ) ` X ) = ( S ` X ) )
26	25	ad2antlr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> ( ( S |` C ) ` X ) = ( S ` X ) )
27		fvres	|- ( Y e. C -> ( ( S |` C ) ` Y ) = ( S ` Y ) )
28	27	ad2antrl	|- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> ( ( S |` C ) ` Y ) = ( S ` Y ) )
29	28	fveq2d	|- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> ( Z ` ( ( S |` C ) ` Y ) ) = ( Z ` ( S ` Y ) ) )
30	24 26 29	3sstr3d	|- ( ( ( ph /\ X e. C ) /\ ( Y e. C /\ X =/= Y ) ) -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) )
31	30	exp32	|- ( ( ph /\ X e. C ) -> ( Y e. C -> ( X =/= Y -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) ) )
32	25	ad2antlr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( ( S |` C ) ` X ) = ( S ` X ) )
33	6	ad2antrr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> G dom DProd ( S |` C ) )
34	19	ad2antrr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> dom ( S |` C ) = C )
35		simplr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> X e. C )
36	33 34 35	dprdub	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( ( S |` C ) ` X ) C_ ( G DProd ( S |` C ) ) )
37	32 36	eqsstrrd	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( S ` X ) C_ ( G DProd ( S |` C ) ) )
38	8	ad2antrr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
39		eqid	|- ( Base ` G ) = ( Base ` G )
40	39	dprdssv	|- ( G DProd ( S |` D ) ) C_ ( Base ` G )
41		fvres	|- ( Y e. D -> ( ( S |` D ) ` Y ) = ( S ` Y ) )
42	41	ad2antrl	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( ( S |` D ) ` Y ) = ( S ` Y ) )
43	7	ad2antrr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> G dom DProd ( S |` D ) )
44		ssun2	|- D C_ ( C u. D )
45	44 3	sseqtrrid	|- ( ph -> D C_ I )
46	1 45	fssresd	|- ( ph -> ( S |` D ) : D --> ( SubGrp ` G ) )
47	46	fdmd	|- ( ph -> dom ( S |` D ) = D )
48	47	ad2antrr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> dom ( S |` D ) = D )
49		simprl	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> Y e. D )
50	43 48 49	dprdub	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( ( S |` D ) ` Y ) C_ ( G DProd ( S |` D ) ) )
51	42 50	eqsstrrd	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( S ` Y ) C_ ( G DProd ( S |` D ) ) )
52	39 4	cntz2ss	|- ( ( ( G DProd ( S |` D ) ) C_ ( Base ` G ) /\ ( S ` Y ) C_ ( G DProd ( S |` D ) ) ) -> ( Z ` ( G DProd ( S |` D ) ) ) C_ ( Z ` ( S ` Y ) ) )
53	40 51 52	sylancr	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( Z ` ( G DProd ( S |` D ) ) ) C_ ( Z ` ( S ` Y ) ) )
54	38 53	sstrd	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( G DProd ( S |` C ) ) C_ ( Z ` ( S ` Y ) ) )
55	37 54	sstrd	|- ( ( ( ph /\ X e. C ) /\ ( Y e. D /\ X =/= Y ) ) -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) )
56	55	exp32	|- ( ( ph /\ X e. C ) -> ( Y e. D -> ( X =/= Y -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) ) )
57	31 56	jaod	|- ( ( ph /\ X e. C ) -> ( ( Y e. C \/ Y e. D ) -> ( X =/= Y -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) ) )
58	14 57	sylbid	|- ( ( ph /\ X e. C ) -> ( Y e. I -> ( X =/= Y -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) ) )
59		dprdgrp	|- ( G dom DProd ( S |` C ) -> G e. Grp )
60	6 59	syl	|- ( ph -> G e. Grp )
61	60	adantr	|- ( ( ph /\ X e. C ) -> G e. Grp )
62	39	subgacs	|- ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
63		acsmre	|- ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
64	61 62 63	3syl	|- ( ( ph /\ X e. C ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
65		difundir	|- ( ( C u. D ) \ { X } ) = ( ( C \ { X } ) u. ( D \ { X } ) )
66	11	difeq1d	|- ( ( ph /\ X e. C ) -> ( I \ { X } ) = ( ( C u. D ) \ { X } ) )
67		simpr	|- ( ( ph /\ X e. C ) -> X e. C )
68	67	snssd	|- ( ( ph /\ X e. C ) -> { X } C_ C )
69		sslin	|- ( { X } C_ C -> ( D i^i { X } ) C_ ( D i^i C ) )
70	68 69	syl	|- ( ( ph /\ X e. C ) -> ( D i^i { X } ) C_ ( D i^i C ) )
71		incom	|- ( C i^i D ) = ( D i^i C )
72	2	adantr	|- ( ( ph /\ X e. C ) -> ( C i^i D ) = (/) )
73	71 72	syl5eqr	|- ( ( ph /\ X e. C ) -> ( D i^i C ) = (/) )
74		sseq0	|- ( ( ( D i^i { X } ) C_ ( D i^i C ) /\ ( D i^i C ) = (/) ) -> ( D i^i { X } ) = (/) )
75	70 73 74	syl2anc	|- ( ( ph /\ X e. C ) -> ( D i^i { X } ) = (/) )
76		disj3	|- ( ( D i^i { X } ) = (/) <-> D = ( D \ { X } ) )
77	75 76	sylib	|- ( ( ph /\ X e. C ) -> D = ( D \ { X } ) )
78	77	uneq2d	|- ( ( ph /\ X e. C ) -> ( ( C \ { X } ) u. D ) = ( ( C \ { X } ) u. ( D \ { X } ) ) )
79	65 66 78	3eqtr4a	|- ( ( ph /\ X e. C ) -> ( I \ { X } ) = ( ( C \ { X } ) u. D ) )
80	79	imaeq2d	|- ( ( ph /\ X e. C ) -> ( S " ( I \ { X } ) ) = ( S " ( ( C \ { X } ) u. D ) ) )
81		imaundi	|- ( S " ( ( C \ { X } ) u. D ) ) = ( ( S " ( C \ { X } ) ) u. ( S " D ) )
82	80 81	eqtrdi	|- ( ( ph /\ X e. C ) -> ( S " ( I \ { X } ) ) = ( ( S " ( C \ { X } ) ) u. ( S " D ) ) )
83	82	unieqd	|- ( ( ph /\ X e. C ) -> U. ( S " ( I \ { X } ) ) = U. ( ( S " ( C \ { X } ) ) u. ( S " D ) ) )
84		uniun	|- U. ( ( S " ( C \ { X } ) ) u. ( S " D ) ) = ( U. ( S " ( C \ { X } ) ) u. U. ( S " D ) )
85	83 84	eqtrdi	|- ( ( ph /\ X e. C ) -> U. ( S " ( I \ { X } ) ) = ( U. ( S " ( C \ { X } ) ) u. U. ( S " D ) ) )
86		difss	|- ( C \ { X } ) C_ C
87		imass2	|- ( ( C \ { X } ) C_ C -> ( S " ( C \ { X } ) ) C_ ( S " C ) )
88		uniss	|- ( ( S " ( C \ { X } ) ) C_ ( S " C ) -> U. ( S " ( C \ { X } ) ) C_ U. ( S " C ) )
89	86 87 88	mp2b	|- U. ( S " ( C \ { X } ) ) C_ U. ( S " C )
90		imassrn	|- ( S " C ) C_ ran S
91	1	frnd	|- ( ph -> ran S C_ ( SubGrp ` G ) )
92	91	adantr	|- ( ( ph /\ X e. C ) -> ran S C_ ( SubGrp ` G ) )
93		mresspw	|- ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
94	64 93	syl	|- ( ( ph /\ X e. C ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
95	92 94	sstrd	|- ( ( ph /\ X e. C ) -> ran S C_ ~P ( Base ` G ) )
96	90 95	sstrid	|- ( ( ph /\ X e. C ) -> ( S " C ) C_ ~P ( Base ` G ) )
97		sspwuni	|- ( ( S " C ) C_ ~P ( Base ` G ) <-> U. ( S " C ) C_ ( Base ` G ) )
98	96 97	sylib	|- ( ( ph /\ X e. C ) -> U. ( S " C ) C_ ( Base ` G ) )
99	89 98	sstrid	|- ( ( ph /\ X e. C ) -> U. ( S " ( C \ { X } ) ) C_ ( Base ` G ) )
100	64 10 99	mrcssidd	|- ( ( ph /\ X e. C ) -> U. ( S " ( C \ { X } ) ) C_ ( K ` U. ( S " ( C \ { X } ) ) ) )
101		imassrn	|- ( S " D ) C_ ran S
102	101 95	sstrid	|- ( ( ph /\ X e. C ) -> ( S " D ) C_ ~P ( Base ` G ) )
103		sspwuni	|- ( ( S " D ) C_ ~P ( Base ` G ) <-> U. ( S " D ) C_ ( Base ` G ) )
104	102 103	sylib	|- ( ( ph /\ X e. C ) -> U. ( S " D ) C_ ( Base ` G ) )
105	64 10 104	mrcssidd	|- ( ( ph /\ X e. C ) -> U. ( S " D ) C_ ( K ` U. ( S " D ) ) )
106	10	dprdspan	|- ( G dom DProd ( S |` D ) -> ( G DProd ( S |` D ) ) = ( K ` U. ran ( S |` D ) ) )
107	7 106	syl	|- ( ph -> ( G DProd ( S |` D ) ) = ( K ` U. ran ( S |` D ) ) )
108		df-ima	|- ( S " D ) = ran ( S |` D )
109	108	unieqi	|- U. ( S " D ) = U. ran ( S |` D )
110	109	fveq2i	|- ( K ` U. ( S " D ) ) = ( K ` U. ran ( S |` D ) )
111	107 110	eqtr4di	|- ( ph -> ( G DProd ( S |` D ) ) = ( K ` U. ( S " D ) ) )
112	111	adantr	|- ( ( ph /\ X e. C ) -> ( G DProd ( S |` D ) ) = ( K ` U. ( S " D ) ) )
113	105 112	sseqtrrd	|- ( ( ph /\ X e. C ) -> U. ( S " D ) C_ ( G DProd ( S |` D ) ) )
114		unss12	|- ( ( 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 ) ) ) )
115	100 113 114	syl2anc	|- ( ( ph /\ X e. C ) -> ( U. ( S " ( C \ { X } ) ) u. U. ( S " D ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) u. ( G DProd ( S |` D ) ) ) )
116	10	mrccl	|- ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ( S " ( C \ { X } ) ) C_ ( Base ` G ) ) -> ( K ` U. ( S " ( C \ { X } ) ) ) e. ( SubGrp ` G ) )
117	64 99 116	syl2anc	|- ( ( ph /\ X e. C ) -> ( K ` U. ( S " ( C \ { X } ) ) ) e. ( SubGrp ` G ) )
118		dprdsubg	|- ( G dom DProd ( S |` D ) -> ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) )
119	7 118	syl	|- ( ph -> ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) )
120	119	adantr	|- ( ( ph /\ X e. C ) -> ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) )
121		eqid	|- ( LSSum ` G ) = ( LSSum ` G )
122	121	lsmunss	|- ( ( ( 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 ) ) ) )
123	117 120 122	syl2anc	|- ( ( 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 ) ) ) )
124	115 123	sstrd	|- ( ( ph /\ X e. C ) -> ( U. ( S " ( C \ { X } ) ) u. U. ( S " D ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) )
125	85 124	eqsstrd	|- ( ( ph /\ X e. C ) -> U. ( S " ( I \ { X } ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) )
126	89	a1i	|- ( ( ph /\ X e. C ) -> U. ( S " ( C \ { X } ) ) C_ U. ( S " C ) )
127	64 10 126 98	mrcssd	|- ( ( ph /\ X e. C ) -> ( K ` U. ( S " ( C \ { X } ) ) ) C_ ( K ` U. ( S " C ) ) )
128	10	dprdspan	|- ( G dom DProd ( S |` C ) -> ( G DProd ( S |` C ) ) = ( K ` U. ran ( S |` C ) ) )
129	6 128	syl	|- ( ph -> ( G DProd ( S |` C ) ) = ( K ` U. ran ( S |` C ) ) )
130		df-ima	|- ( S " C ) = ran ( S |` C )
131	130	unieqi	|- U. ( S " C ) = U. ran ( S |` C )
132	131	fveq2i	|- ( K ` U. ( S " C ) ) = ( K ` U. ran ( S |` C ) )
133	129 132	eqtr4di	|- ( ph -> ( G DProd ( S |` C ) ) = ( K ` U. ( S " C ) ) )
134	133	adantr	|- ( ( ph /\ X e. C ) -> ( G DProd ( S |` C ) ) = ( K ` U. ( S " C ) ) )
135	127 134	sseqtrrd	|- ( ( ph /\ X e. C ) -> ( K ` U. ( S " ( C \ { X } ) ) ) C_ ( G DProd ( S |` C ) ) )
136	8	adantr	|- ( ( ph /\ X e. C ) -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
137	135 136	sstrd	|- ( ( ph /\ X e. C ) -> ( K ` U. ( S " ( C \ { X } ) ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
138	121 4	lsmsubg	|- ( ( ( 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 ) )
139	117 120 137 138	syl3anc	|- ( ( ph /\ X e. C ) -> ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) e. ( SubGrp ` G ) )
140	10	mrcsscl	|- ( ( ( 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 ) ) ) )
141	64 125 139 140	syl3anc	|- ( ( ph /\ X e. C ) -> ( K ` U. ( S " ( I \ { X } ) ) ) C_ ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) )
142		sslin	|- ( ( 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 ) ) ) ) )
143	141 142	syl	|- ( ( 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 ) ) ) ) )
144	17	sselda	|- ( ( ph /\ X e. C ) -> X e. I )
145	1	ffvelrnda	|- ( ( ph /\ X e. I ) -> ( S ` X ) e. ( SubGrp ` G ) )
146	144 145	syldan	|- ( ( ph /\ X e. C ) -> ( S ` X ) e. ( SubGrp ` G ) )
147	25	adantl	|- ( ( ph /\ X e. C ) -> ( ( S |` C ) ` X ) = ( S ` X ) )
148	6	adantr	|- ( ( ph /\ X e. C ) -> G dom DProd ( S |` C ) )
149	19	adantr	|- ( ( ph /\ X e. C ) -> dom ( S |` C ) = C )
150	148 149 67	dprdub	|- ( ( ph /\ X e. C ) -> ( ( S |` C ) ` X ) C_ ( G DProd ( S |` C ) ) )
151	147 150	eqsstrrd	|- ( ( ph /\ X e. C ) -> ( S ` X ) C_ ( G DProd ( S |` C ) ) )
152		dprdsubg	|- ( G dom DProd ( S |` C ) -> ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) )
153	6 152	syl	|- ( ph -> ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) )
154	153	adantr	|- ( ( ph /\ X e. C ) -> ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) )
155	121	lsmlub	|- ( ( ( 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 ) ) ) )
156	146 117 154 155	syl3anc	|- ( ( 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 ) ) ) )
157	151 135 156	mpbi2and	|- ( ( ph /\ X e. C ) -> ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) C_ ( G DProd ( S |` C ) ) )
158	157	ssrind	|- ( ( 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 ) ) ) )
159	9	adantr	|- ( ( ph /\ X e. C ) -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )
160	158 159	sseqtrd	|- ( ( ph /\ X e. C ) -> ( ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) i^i ( G DProd ( S |` D ) ) ) C_ { .0. } )
161	121	lsmub1	|- ( ( ( 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 } ) ) ) ) )
162	146 117 161	syl2anc	|- ( ( ph /\ X e. C ) -> ( S ` X ) C_ ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) )
163	5	subg0cl	|- ( ( S ` X ) e. ( SubGrp ` G ) -> .0. e. ( S ` X ) )
164	146 163	syl	|- ( ( ph /\ X e. C ) -> .0. e. ( S ` X ) )
165	162 164	sseldd	|- ( ( ph /\ X e. C ) -> .0. e. ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) )
166	5	subg0cl	|- ( ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) -> .0. e. ( G DProd ( S |` D ) ) )
167	120 166	syl	|- ( ( ph /\ X e. C ) -> .0. e. ( G DProd ( S |` D ) ) )
168	165 167	elind	|- ( ( ph /\ X e. C ) -> .0. e. ( ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) i^i ( G DProd ( S |` D ) ) ) )
169	168	snssd	|- ( ( ph /\ X e. C ) -> { .0. } C_ ( ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) i^i ( G DProd ( S |` D ) ) ) )
170	160 169	eqssd	|- ( ( ph /\ X e. C ) -> ( ( ( S ` X ) ( LSSum ` G ) ( K ` U. ( S " ( C \ { X } ) ) ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )
171		resima2	|- ( ( C \ { X } ) C_ C -> ( ( S |` C ) " ( C \ { X } ) ) = ( S " ( C \ { X } ) ) )
172	86 171	mp1i	|- ( ( ph /\ X e. C ) -> ( ( S |` C ) " ( C \ { X } ) ) = ( S " ( C \ { X } ) ) )
173	172	unieqd	|- ( ( ph /\ X e. C ) -> U. ( ( S |` C ) " ( C \ { X } ) ) = U. ( S " ( C \ { X } ) ) )
174	173	fveq2d	|- ( ( ph /\ X e. C ) -> ( K ` U. ( ( S |` C ) " ( C \ { X } ) ) ) = ( K ` U. ( S " ( C \ { X } ) ) ) )
175	147 174	ineq12d	|- ( ( ph /\ X e. C ) -> ( ( ( S |` C ) ` X ) i^i ( K ` U. ( ( S |` C ) " ( C \ { X } ) ) ) ) = ( ( S ` X ) i^i ( K ` U. ( S " ( C \ { X } ) ) ) ) )
176	148 149 67 5 10	dprddisj	|- ( ( ph /\ X e. C ) -> ( ( ( S |` C ) ` X ) i^i ( K ` U. ( ( S |` C ) " ( C \ { X } ) ) ) ) = { .0. } )
177	175 176	eqtr3d	|- ( ( ph /\ X e. C ) -> ( ( S ` X ) i^i ( K ` U. ( S " ( C \ { X } ) ) ) ) = { .0. } )
178	1	adantr	|- ( ( ph /\ X e. C ) -> S : I --> ( SubGrp ` G ) )
179		ffun	|- ( S : I --> ( SubGrp ` G ) -> Fun S )
180		funiunfv	|- ( Fun S -> U_ y e. ( C \ { X } ) ( S ` y ) = U. ( S " ( C \ { X } ) ) )
181	178 179 180	3syl	|- ( ( ph /\ X e. C ) -> U_ y e. ( C \ { X } ) ( S ` y ) = U. ( S " ( C \ { X } ) ) )
182	6	ad2antrr	|- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> G dom DProd ( S |` C ) )
183	19	ad2antrr	|- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> dom ( S |` C ) = C )
184		eldifi	|- ( y e. ( C \ { X } ) -> y e. C )
185	184	adantl	|- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> y e. C )
186		simplr	|- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> X e. C )
187		eldifsni	|- ( y e. ( C \ { X } ) -> y =/= X )
188	187	adantl	|- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> y =/= X )
189	182 183 185 186 188 4	dprdcntz	|- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> ( ( S |` C ) ` y ) C_ ( Z ` ( ( S |` C ) ` X ) ) )
190	185	fvresd	|- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> ( ( S |` C ) ` y ) = ( S ` y ) )
191	25	ad2antlr	|- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> ( ( S |` C ) ` X ) = ( S ` X ) )
192	191	fveq2d	|- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> ( Z ` ( ( S |` C ) ` X ) ) = ( Z ` ( S ` X ) ) )
193	189 190 192	3sstr3d	|- ( ( ( ph /\ X e. C ) /\ y e. ( C \ { X } ) ) -> ( S ` y ) C_ ( Z ` ( S ` X ) ) )
194	193	ralrimiva	|- ( ( ph /\ X e. C ) -> A. y e. ( C \ { X } ) ( S ` y ) C_ ( Z ` ( S ` X ) ) )
195		iunss	|- ( U_ y e. ( C \ { X } ) ( S ` y ) C_ ( Z ` ( S ` X ) ) <-> A. y e. ( C \ { X } ) ( S ` y ) C_ ( Z ` ( S ` X ) ) )
196	194 195	sylibr	|- ( ( ph /\ X e. C ) -> U_ y e. ( C \ { X } ) ( S ` y ) C_ ( Z ` ( S ` X ) ) )
197	181 196	eqsstrrd	|- ( ( ph /\ X e. C ) -> U. ( S " ( C \ { X } ) ) C_ ( Z ` ( S ` X ) ) )
198	39	subgss	|- ( ( S ` X ) e. ( SubGrp ` G ) -> ( S ` X ) C_ ( Base ` G ) )
199	146 198	syl	|- ( ( ph /\ X e. C ) -> ( S ` X ) C_ ( Base ` G ) )
200	39 4	cntzsubg	|- ( ( G e. Grp /\ ( S ` X ) C_ ( Base ` G ) ) -> ( Z ` ( S ` X ) ) e. ( SubGrp ` G ) )
201	61 199 200	syl2anc	|- ( ( ph /\ X e. C ) -> ( Z ` ( S ` X ) ) e. ( SubGrp ` G ) )
202	10	mrcsscl	|- ( ( ( 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 ) ) )
203	64 197 201 202	syl3anc	|- ( ( ph /\ X e. C ) -> ( K ` U. ( S " ( C \ { X } ) ) ) C_ ( Z ` ( S ` X ) ) )
204	4 117 146 203	cntzrecd	|- ( ( ph /\ X e. C ) -> ( S ` X ) C_ ( Z ` ( K ` U. ( S " ( C \ { X } ) ) ) ) )
205	121 146 117 120 5 170 177 4 204	lsmdisj3	|- ( ( ph /\ X e. C ) -> ( ( S ` X ) i^i ( ( K ` U. ( S " ( C \ { X } ) ) ) ( LSSum ` G ) ( G DProd ( S |` D ) ) ) ) = { .0. } )
206	143 205	sseqtrd	|- ( ( ph /\ X e. C ) -> ( ( S ` X ) i^i ( K ` U. ( S " ( I \ { X } ) ) ) ) C_ { .0. } )
207	58 206	jca	|- ( ( 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. } ) )