This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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