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

Metamath Proof Explorer

Theorem dprdres

Description: Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdres.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dprdres.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dprdres.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐼 )
Assertion dprdres ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ↾ 𝐴 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐴 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 dprdres.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dprdres.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dprdres.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐼 )
4 dprdgrp ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
5 1 4 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
6 1 2 dprdf2 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
7 6 3 fssresd ⊢ ( 𝜑 → ( 𝑆 ↾ 𝐴 ) : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) )
8 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → 𝐺 dom DProd 𝑆 )
9 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → dom 𝑆 = 𝐼 )
10 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → 𝐴 ⊆ 𝐼 )
11 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → 𝑥 ∈ 𝐴 )
12 10 11 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → 𝑥 ∈ 𝐼 )
13 eldifi ⊢ ( 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) → 𝑦 ∈ 𝐴 )
14 13 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → 𝑦 ∈ 𝐴 )
15 10 14 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → 𝑦 ∈ 𝐼 )
16 eldifsni ⊢ ( 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) → 𝑦 ≠ 𝑥 )
17 16 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → 𝑦 ≠ 𝑥 )
18 17 necomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → 𝑥 ≠ 𝑦 )
19 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
20 8 9 12 15 18 19 dprdcntz ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) )
21 11 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
22 14 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝑆 ‘ 𝑦 ) )
23 22 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → ( ( Cntz ‘ 𝐺 ) ‘ ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑦 ) ) = ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) )
24 20 21 23 3sstr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑦 ) ) )
25 24 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑦 ) ) )
26 fvres ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
28 27 ineq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) = ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) )
29 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
30 29 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
31 acsmre ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
32 5 30 31 3syl ⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
34 eqid ⊢ ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
35 resss ⊢ ( 𝑆 ↾ 𝐴 ) ⊆ 𝑆
36 imass1 ⊢ ( ( 𝑆 ↾ 𝐴 ) ⊆ 𝑆 → ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ⊆ ( 𝑆 “ ( 𝐴 ∖ { 𝑥 } ) ) )
37 35 36 ax-mp ⊢ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ⊆ ( 𝑆 “ ( 𝐴 ∖ { 𝑥 } ) )
38 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ 𝐼 )
39 ssdif ⊢ ( 𝐴 ⊆ 𝐼 → ( 𝐴 ∖ { 𝑥 } ) ⊆ ( 𝐼 ∖ { 𝑥 } ) )
40 imass2 ⊢ ( ( 𝐴 ∖ { 𝑥 } ) ⊆ ( 𝐼 ∖ { 𝑥 } ) → ( 𝑆 “ ( 𝐴 ∖ { 𝑥 } ) ) ⊆ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) )
41 38 39 40 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑆 “ ( 𝐴 ∖ { 𝑥 } ) ) ⊆ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) )
42 37 41 sstrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ⊆ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) )
43 42 unissd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ⊆ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) )
44 imassrn ⊢ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ran 𝑆
45 6 frnd ⊢ ( 𝜑 → ran 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) )
46 29 subgss ⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) → 𝑥 ⊆ ( Base ‘ 𝐺 ) )
47 velpw ⊢ ( 𝑥 ∈ 𝒫 ( Base ‘ 𝐺 ) ↔ 𝑥 ⊆ ( Base ‘ 𝐺 ) )
48 46 47 sylibr ⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) → 𝑥 ∈ 𝒫 ( Base ‘ 𝐺 ) )
49 48 ssriv ⊢ ( SubGrp ‘ 𝐺 ) ⊆ 𝒫 ( Base ‘ 𝐺 )
50 45 49 sstrdi ⊢ ( 𝜑 → ran 𝑆 ⊆ 𝒫 ( Base ‘ 𝐺 ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ran 𝑆 ⊆ 𝒫 ( Base ‘ 𝐺 ) )
52 44 51 sstrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
53 sspwuni ⊢ ( ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) ↔ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐺 ) )
54 52 53 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐺 ) )
55 33 34 43 54 mrcssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) )
56 sslin ⊢ ( ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) ⊆ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
57 55 56 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) ⊆ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
58 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐺 dom DProd 𝑆 )
59 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → dom 𝑆 = 𝐼 )
60 3 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐼 )
61 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
62 58 59 60 61 34 dprddisj ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } )
63 57 62 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) ⊆ { ( 0g ‘ 𝐺 ) } )
64 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) )
65 60 64 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) )
66 61 subg0cl ⊢ ( ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ ( 𝑆 ‘ 𝑥 ) )
67 65 66 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0g ‘ 𝐺 ) ∈ ( 𝑆 ‘ 𝑥 ) )
68 43 54 sstrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐺 ) )
69 34 mrccl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐺 ) ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
70 33 68 69 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
71 61 subg0cl ⊢ ( ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) )
72 70 71 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0g ‘ 𝐺 ) ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) )
73 67 72 elind ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0g ‘ 𝐺 ) ∈ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) )
74 73 snssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → { ( 0g ‘ 𝐺 ) } ⊆ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) )
75 63 74 eqssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } )
76 28 75 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } )
77 25 76 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ ( ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) )
78 77 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ ( ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) )
79 1 2 dprddomcld ⊢ ( 𝜑 → 𝐼 ∈ V )
80 79 3 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
81 7 fdmd ⊢ ( 𝜑 → dom ( 𝑆 ↾ 𝐴 ) = 𝐴 )
82 19 61 34 dmdprd ⊢ ( ( 𝐴 ∈ V ∧ dom ( 𝑆 ↾ 𝐴 ) = 𝐴 ) → ( 𝐺 dom DProd ( 𝑆 ↾ 𝐴 ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑆 ↾ 𝐴 ) : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ ( ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
83 80 81 82 syl2anc ⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ↾ 𝐴 ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑆 ↾ 𝐴 ) : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ ( 𝐴 ∖ { 𝑥 } ) ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ ( ( ( 𝑆 ↾ 𝐴 ) ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ↾ 𝐴 ) “ ( 𝐴 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
84 5 7 78 83 mpbir3and ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ↾ 𝐴 ) )
85 rnss ⊢ ( ( 𝑆 ↾ 𝐴 ) ⊆ 𝑆 → ran ( 𝑆 ↾ 𝐴 ) ⊆ ran 𝑆 )
86 uniss ⊢ ( ran ( 𝑆 ↾ 𝐴 ) ⊆ ran 𝑆 → ∪ ran ( 𝑆 ↾ 𝐴 ) ⊆ ∪ ran 𝑆 )
87 35 85 86 mp2b ⊢ ∪ ran ( 𝑆 ↾ 𝐴 ) ⊆ ∪ ran 𝑆
88 87 a1i ⊢ ( 𝜑 → ∪ ran ( 𝑆 ↾ 𝐴 ) ⊆ ∪ ran 𝑆 )
89 sspwuni ⊢ ( ran 𝑆 ⊆ 𝒫 ( Base ‘ 𝐺 ) ↔ ∪ ran 𝑆 ⊆ ( Base ‘ 𝐺 ) )
90 50 89 sylib ⊢ ( 𝜑 → ∪ ran 𝑆 ⊆ ( Base ‘ 𝐺 ) )
91 32 34 88 90 mrcssd ⊢ ( 𝜑 → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ran ( 𝑆 ↾ 𝐴 ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ran 𝑆 ) )
92 34 dprdspan ⊢ ( 𝐺 dom DProd ( 𝑆 ↾ 𝐴 ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐴 ) ) = ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ran ( 𝑆 ↾ 𝐴 ) ) )
93 84 92 syl ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐴 ) ) = ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ran ( 𝑆 ↾ 𝐴 ) ) )
94 34 dprdspan ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) = ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ran 𝑆 ) )
95 1 94 syl ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ran 𝑆 ) )
96 91 93 95 3sstr4d ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐴 ) ) ⊆ ( 𝐺 DProd 𝑆 ) )
97 84 96 jca ⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ↾ 𝐴 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐴 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )