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 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑋 ) ∈ ( 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 } ) )