Metamath Proof Explorer


Theorem dmdprdsplit2lem

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

Ref Expression
Hypotheses dprdsplit.2 ( 𝜑𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
dprdsplit.i ( 𝜑 → ( 𝐶𝐷 ) = ∅ )
dprdsplit.u ( 𝜑𝐼 = ( 𝐶𝐷 ) )
dmdprdsplit.z 𝑍 = ( Cntz ‘ 𝐺 )
dmdprdsplit.0 0 = ( 0g𝐺 )
dmdprdsplit2.1 ( 𝜑𝐺 dom DProd ( 𝑆𝐶 ) )
dmdprdsplit2.2 ( 𝜑𝐺 dom DProd ( 𝑆𝐷 ) )
dmdprdsplit2.3 ( 𝜑 → ( 𝐺 DProd ( 𝑆𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆𝐷 ) ) ) )
dmdprdsplit2.4 ( 𝜑 → ( ( 𝐺 DProd ( 𝑆𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆𝐷 ) ) ) = { 0 } )
dmdprdsplit2lem.k 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion dmdprdsplit2lem ( ( 𝜑𝑋𝐶 ) → ( ( 𝑌𝐼 → ( 𝑋𝑌 → ( 𝑆𝑋 ) ⊆ ( 𝑍 ‘ ( 𝑆𝑌 ) ) ) ) ∧ ( ( 𝑆𝑋 ) ∩ ( 𝐾 ( 𝑆 “ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ⊆ { 0 } ) )

Proof

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