Metamath Proof Explorer

Theorem dmdprdsplit

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 ‘ 𝐺 )
Assertion dmdprdsplit ( 𝜑 → ( 𝐺 dom DProd 𝑆 ↔ ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 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 simpr ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → 𝐺 dom DProd 𝑆 )
7 1 fdmd ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → dom 𝑆 = 𝐼 )
9 ssun1 ⊢ 𝐶 ⊆ ( 𝐶 ∪ 𝐷 )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → 𝐼 = ( 𝐶 ∪ 𝐷 ) )
11 9 10 sseqtrrid ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → 𝐶 ⊆ 𝐼 )
12 6 8 11 dprdres ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )
13 12 simpld ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) )
14 ssun2 ⊢ 𝐷 ⊆ ( 𝐶 ∪ 𝐷 )
15 14 10 sseqtrrid ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → 𝐷 ⊆ 𝐼 )
16 6 8 15 dprdres ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → ( 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )
17 16 simpld ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) )
18 13 17 jca ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) )
19 2 adantr ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → ( 𝐶 ∩ 𝐷 ) = ∅ )
20 6 8 11 15 19 4 dprdcntz2 ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
21 6 8 11 15 19 5 dprddisj2 ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } )
22 18 20 21 3jca ⊢ ( ( 𝜑 ∧ 𝐺 dom DProd 𝑆 ) → ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } ) )
23 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } ) ) → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
24 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } ) ) → ( 𝐶 ∩ 𝐷 ) = ∅ )
25 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } ) ) → 𝐼 = ( 𝐶 ∪ 𝐷 ) )
26 simpr1l ⊢ ( ( 𝜑 ∧ ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } ) ) → 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) )
27 simpr1r ⊢ ( ( 𝜑 ∧ ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } ) ) → 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) )
28 simpr2 ⊢ ( ( 𝜑 ∧ ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } ) ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
29 simpr3 ⊢ ( ( 𝜑 ∧ ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } ) ) → ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } )
30 23 24 25 4 5 26 27 28 29 dmdprdsplit2 ⊢ ( ( 𝜑 ∧ ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } ) ) → 𝐺 dom DProd 𝑆 )
31 22 30 impbida ⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑆 ↔ ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } ) ) )