Metamath Proof Explorer


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 eqtr3id
 |-  ( ( 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. } ) )