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 𝑆 )