Metamath Proof Explorer


Theorem dmdprdsplit2

Description: The direct product splits into the direct product of any partition of the index set. (Contributed by Mario Carneiro, 25-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 } )
Assertion dmdprdsplit2 ( 𝜑𝐺 dom DProd 𝑆 )

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 eqid ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
11 dprdgrp ( 𝐺 dom DProd ( 𝑆𝐶 ) → 𝐺 ∈ Grp )
12 6 11 syl ( 𝜑𝐺 ∈ Grp )
13 ssun1 𝐶 ⊆ ( 𝐶𝐷 )
14 13 3 sseqtrrid ( 𝜑𝐶𝐼 )
15 1 14 fssresd ( 𝜑 → ( 𝑆𝐶 ) : 𝐶 ⟶ ( SubGrp ‘ 𝐺 ) )
16 15 fdmd ( 𝜑 → dom ( 𝑆𝐶 ) = 𝐶 )
17 6 16 dprddomcld ( 𝜑𝐶 ∈ V )
18 ssun2 𝐷 ⊆ ( 𝐶𝐷 )
19 18 3 sseqtrrid ( 𝜑𝐷𝐼 )
20 1 19 fssresd ( 𝜑 → ( 𝑆𝐷 ) : 𝐷 ⟶ ( SubGrp ‘ 𝐺 ) )
21 20 fdmd ( 𝜑 → dom ( 𝑆𝐷 ) = 𝐷 )
22 7 21 dprddomcld ( 𝜑𝐷 ∈ V )
23 unexg ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝐶𝐷 ) ∈ V )
24 17 22 23 syl2anc ( 𝜑 → ( 𝐶𝐷 ) ∈ V )
25 3 24 eqeltrd ( 𝜑𝐼 ∈ V )
26 3 eleq2d ( 𝜑 → ( 𝑥𝐼𝑥 ∈ ( 𝐶𝐷 ) ) )
27 elun ( 𝑥 ∈ ( 𝐶𝐷 ) ↔ ( 𝑥𝐶𝑥𝐷 ) )
28 26 27 bitrdi ( 𝜑 → ( 𝑥𝐼 ↔ ( 𝑥𝐶𝑥𝐷 ) ) )
29 1 2 3 4 5 6 7 8 9 10 dmdprdsplit2lem ( ( 𝜑𝑥𝐶 ) → ( ( 𝑦𝐼 → ( 𝑥𝑦 → ( 𝑆𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆𝑦 ) ) ) ) ∧ ( ( 𝑆𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } ) )
30 incom ( 𝐶𝐷 ) = ( 𝐷𝐶 )
31 30 2 eqtr3id ( 𝜑 → ( 𝐷𝐶 ) = ∅ )
32 uncom ( 𝐶𝐷 ) = ( 𝐷𝐶 )
33 3 32 eqtrdi ( 𝜑𝐼 = ( 𝐷𝐶 ) )
34 dprdsubg ( 𝐺 dom DProd ( 𝑆𝐶 ) → ( 𝐺 DProd ( 𝑆𝐶 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
35 6 34 syl ( 𝜑 → ( 𝐺 DProd ( 𝑆𝐶 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
36 dprdsubg ( 𝐺 dom DProd ( 𝑆𝐷 ) → ( 𝐺 DProd ( 𝑆𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
37 7 36 syl ( 𝜑 → ( 𝐺 DProd ( 𝑆𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
38 4 35 37 8 cntzrecd ( 𝜑 → ( 𝐺 DProd ( 𝑆𝐷 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆𝐶 ) ) ) )
39 incom ( ( 𝐺 DProd ( 𝑆𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆𝐷 ) ) ) = ( ( 𝐺 DProd ( 𝑆𝐷 ) ) ∩ ( 𝐺 DProd ( 𝑆𝐶 ) ) )
40 39 9 eqtr3id ( 𝜑 → ( ( 𝐺 DProd ( 𝑆𝐷 ) ) ∩ ( 𝐺 DProd ( 𝑆𝐶 ) ) ) = { 0 } )
41 1 31 33 4 5 7 6 38 40 10 dmdprdsplit2lem ( ( 𝜑𝑥𝐷 ) → ( ( 𝑦𝐼 → ( 𝑥𝑦 → ( 𝑆𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆𝑦 ) ) ) ) ∧ ( ( 𝑆𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } ) )
42 29 41 jaodan ( ( 𝜑 ∧ ( 𝑥𝐶𝑥𝐷 ) ) → ( ( 𝑦𝐼 → ( 𝑥𝑦 → ( 𝑆𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆𝑦 ) ) ) ) ∧ ( ( 𝑆𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } ) )
43 42 simpld ( ( 𝜑 ∧ ( 𝑥𝐶𝑥𝐷 ) ) → ( 𝑦𝐼 → ( 𝑥𝑦 → ( 𝑆𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆𝑦 ) ) ) ) )
44 43 ex ( 𝜑 → ( ( 𝑥𝐶𝑥𝐷 ) → ( 𝑦𝐼 → ( 𝑥𝑦 → ( 𝑆𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆𝑦 ) ) ) ) ) )
45 28 44 sylbid ( 𝜑 → ( 𝑥𝐼 → ( 𝑦𝐼 → ( 𝑥𝑦 → ( 𝑆𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆𝑦 ) ) ) ) ) )
46 45 3imp2 ( ( 𝜑 ∧ ( 𝑥𝐼𝑦𝐼𝑥𝑦 ) ) → ( 𝑆𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆𝑦 ) ) )
47 28 biimpa ( ( 𝜑𝑥𝐼 ) → ( 𝑥𝐶𝑥𝐷 ) )
48 29 simprd ( ( 𝜑𝑥𝐶 ) → ( ( 𝑆𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } )
49 41 simprd ( ( 𝜑𝑥𝐷 ) → ( ( 𝑆𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } )
50 48 49 jaodan ( ( 𝜑 ∧ ( 𝑥𝐶𝑥𝐷 ) ) → ( ( 𝑆𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } )
51 47 50 syldan ( ( 𝜑𝑥𝐼 ) → ( ( 𝑆𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } )
52 4 5 10 12 25 1 46 51 dmdprdd ( 𝜑𝐺 dom DProd 𝑆 )