Metamath Proof Explorer

Theorem dprdss

Description: Create a direct product by finding subgroups inside each factor of another direct product. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdss.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑇 )
dprdss.2 ⊢ ( 𝜑 → dom 𝑇 = 𝐼 )
dprdss.3 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
dprdss.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) )
Assertion dprdss ( 𝜑 → ( 𝐺 dom DProd 𝑆 ∧ ( 𝐺 DProd 𝑆 ) ⊆ ( 𝐺 DProd 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 dprdss.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑇 )
2 dprdss.2 ⊢ ( 𝜑 → dom 𝑇 = 𝐼 )
3 dprdss.3 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
4 dprdss.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) )
5 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
6 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7 eqid ⊢ ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
8 dprdgrp ⊢ ( 𝐺 dom DProd 𝑇 → 𝐺 ∈ Grp )
9 1 8 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
10 1 2 dprddomcld ⊢ ( 𝜑 → 𝐼 ∈ V )
11 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) )
12 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝑆 ‘ 𝑘 ) = ( 𝑆 ‘ 𝑥 ) )
13 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝑇 ‘ 𝑘 ) = ( 𝑇 ‘ 𝑥 ) )
14 12 13 sseq12d ⊢ ( 𝑘 = 𝑥 → ( ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) ↔ ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑇 ‘ 𝑥 ) ) )
15 14 rspcv ⊢ ( 𝑥 ∈ 𝐼 → ( ∀ 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑇 ‘ 𝑥 ) ) )
16 11 15 mpan9 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑇 ‘ 𝑥 ) )
17 16 3ad2antr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑇 ‘ 𝑥 ) )
18 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → 𝐺 dom DProd 𝑇 )
19 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → dom 𝑇 = 𝐼 )
20 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ 𝐼 )
21 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ 𝐼 )
22 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ≠ 𝑦 )
23 18 19 20 21 22 5 dprdcntz ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑇 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑇 ‘ 𝑦 ) ) )
24 1 2 dprdf2 ⊢ ( 𝜑 → 𝑇 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → 𝑇 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
26 25 21 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑇 ‘ 𝑦 ) ∈ ( SubGrp ‘ 𝐺 ) )
27 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
28 27 subgss ⊢ ( ( 𝑇 ‘ 𝑦 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑇 ‘ 𝑦 ) ⊆ ( Base ‘ 𝐺 ) )
29 26 28 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑇 ‘ 𝑦 ) ⊆ ( Base ‘ 𝐺 ) )
30 fveq2 ⊢ ( 𝑘 = 𝑦 → ( 𝑆 ‘ 𝑘 ) = ( 𝑆 ‘ 𝑦 ) )
31 fveq2 ⊢ ( 𝑘 = 𝑦 → ( 𝑇 ‘ 𝑘 ) = ( 𝑇 ‘ 𝑦 ) )
32 30 31 sseq12d ⊢ ( 𝑘 = 𝑦 → ( ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) ↔ ( 𝑆 ‘ 𝑦 ) ⊆ ( 𝑇 ‘ 𝑦 ) ) )
33 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → ∀ 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) )
34 32 33 21 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑆 ‘ 𝑦 ) ⊆ ( 𝑇 ‘ 𝑦 ) )
35 27 5 cntz2ss ⊢ ( ( ( 𝑇 ‘ 𝑦 ) ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝑆 ‘ 𝑦 ) ⊆ ( 𝑇 ‘ 𝑦 ) ) → ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑇 ‘ 𝑦 ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) )
36 29 34 35 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑇 ‘ 𝑦 ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) )
37 23 36 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑇 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) )
38 17 37 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) )
39 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐺 ∈ Grp )
40 27 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
41 acsmre ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
42 39 40 41 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
43 difss ⊢ ( 𝐼 ∖ { 𝑥 } ) ⊆ 𝐼
44 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∀ 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) )
45 ssralv ⊢ ( ( 𝐼 ∖ { 𝑥 } ) ⊆ 𝐼 → ( ∀ 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) → ∀ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) ) )
46 43 44 45 mpsyl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∀ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) )
47 ss2iun ⊢ ( ∀ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) → ∪ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑘 ) ⊆ ∪ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑇 ‘ 𝑘 ) )
48 46 47 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∪ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑘 ) ⊆ ∪ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑇 ‘ 𝑘 ) )
49 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
50 ffun ⊢ ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) → Fun 𝑆 )
51 funiunfv ⊢ ( Fun 𝑆 → ∪ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑘 ) = ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) )
52 49 50 51 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∪ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑘 ) = ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) )
53 24 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑇 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
54 ffun ⊢ ( 𝑇 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) → Fun 𝑇 )
55 funiunfv ⊢ ( Fun 𝑇 → ∪ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑇 ‘ 𝑘 ) = ∪ ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) )
56 53 54 55 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∪ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑇 ‘ 𝑘 ) = ∪ ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) )
57 48 52 56 3sstr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ∪ ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) )
58 imassrn ⊢ ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ran 𝑇
59 53 frnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ran 𝑇 ⊆ ( SubGrp ‘ 𝐺 ) )
60 mresspw ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
61 42 60 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( SubGrp ‘ 𝐺 ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
62 59 61 sstrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ran 𝑇 ⊆ 𝒫 ( Base ‘ 𝐺 ) )
63 58 62 sstrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
64 sspwuni ⊢ ( ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) ↔ ∪ ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐺 ) )
65 63 64 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∪ ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐺 ) )
66 42 7 57 65 mrcssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) ) )
67 ss2in ⊢ ( ( ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑇 ‘ 𝑥 ) ∧ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ ( ( 𝑇 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
68 16 66 67 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ ( ( 𝑇 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
69 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐺 dom DProd 𝑇 )
70 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → dom 𝑇 = 𝐼 )
71 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
72 69 70 71 6 7 dprddisj ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑇 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑇 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } )
73 68 72 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { ( 0g ‘ 𝐺 ) } )
74 5 6 7 9 10 3 38 73 dmdprdd ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
75 1 a1d ⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑆 → 𝐺 dom DProd 𝑇 ) )
76 ss2ixp ⊢ ( ∀ 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑇 ‘ 𝑘 ) → X 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑇 ‘ 𝑘 ) )
77 11 76 syl ⊢ ( 𝜑 → X 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑇 ‘ 𝑘 ) )
78 rabss2 ⊢ ( X 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝑇 ‘ 𝑘 ) → { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ⊆ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑇 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } )
79 ssrexv ⊢ ( { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ⊆ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑇 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } → ( ∃ 𝑓 ∈ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑎 = ( 𝐺 Σg 𝑓 ) → ∃ 𝑓 ∈ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑇 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑎 = ( 𝐺 Σg 𝑓 ) ) )
80 77 78 79 3syl ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑎 = ( 𝐺 Σg 𝑓 ) → ∃ 𝑓 ∈ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑇 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑎 = ( 𝐺 Σg 𝑓 ) ) )
81 75 80 anim12d ⊢ ( 𝜑 → ( ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑎 = ( 𝐺 Σg 𝑓 ) ) → ( 𝐺 dom DProd 𝑇 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑇 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑎 = ( 𝐺 Σg 𝑓 ) ) ) )
82 fdm ⊢ ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) → dom 𝑆 = 𝐼 )
83 eqid ⊢ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } = { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) }
84 6 83 eldprd ⊢ ( dom 𝑆 = 𝐼 → ( 𝑎 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑎 = ( 𝐺 Σg 𝑓 ) ) ) )
85 3 82 84 3syl ⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑆 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑎 = ( 𝐺 Σg 𝑓 ) ) ) )
86 eqid ⊢ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑇 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } = { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑇 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) }
87 6 86 eldprd ⊢ ( dom 𝑇 = 𝐼 → ( 𝑎 ∈ ( 𝐺 DProd 𝑇 ) ↔ ( 𝐺 dom DProd 𝑇 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑇 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑎 = ( 𝐺 Σg 𝑓 ) ) ) )
88 2 87 syl ⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐺 DProd 𝑇 ) ↔ ( 𝐺 dom DProd 𝑇 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑘 ∈ 𝐼 ( 𝑇 ‘ 𝑘 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑎 = ( 𝐺 Σg 𝑓 ) ) ) )
89 81 85 88 3imtr4d ⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐺 DProd 𝑆 ) → 𝑎 ∈ ( 𝐺 DProd 𝑇 ) ) )
90 89 ssrdv ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) ⊆ ( 𝐺 DProd 𝑇 ) )
91 74 90 jca ⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑆 ∧ ( 𝐺 DProd 𝑆 ) ⊆ ( 𝐺 DProd 𝑇 ) ) )