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 
|- ( ph -> S : I --> ( SubGrp ` G ) )
dprdsplit.i 
|- ( ph -> ( C i^i D ) = (/) )
dprdsplit.u 
|- ( ph -> I = ( C u. D ) )
dmdprdsplit.z 
|- Z = ( Cntz ` G )
dmdprdsplit.0 
|- .0. = ( 0g ` G )
Assertion dmdprdsplit 
|- ( ph -> ( G dom DProd S <-> ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } ) ) )

Proof

Step Hyp Ref Expression
1 dprdsplit.2 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
2 dprdsplit.i 
 |-  ( ph -> ( C i^i D ) = (/) )
3 dprdsplit.u 
 |-  ( ph -> I = ( C u. D ) )
4 dmdprdsplit.z 
 |-  Z = ( Cntz ` G )
5 dmdprdsplit.0 
 |-  .0. = ( 0g ` G )
6 simpr 
 |-  ( ( ph /\ G dom DProd S ) -> G dom DProd S )
7 1 fdmd 
 |-  ( ph -> dom S = I )
8 7 adantr 
 |-  ( ( ph /\ G dom DProd S ) -> dom S = I )
9 ssun1 
 |-  C C_ ( C u. D )
10 3 adantr 
 |-  ( ( ph /\ G dom DProd S ) -> I = ( C u. D ) )
11 9 10 sseqtrrid 
 |-  ( ( ph /\ G dom DProd S ) -> C C_ I )
12 6 8 11 dprdres 
 |-  ( ( ph /\ G dom DProd S ) -> ( G dom DProd ( S |` C ) /\ ( G DProd ( S |` C ) ) C_ ( G DProd S ) ) )
13 12 simpld 
 |-  ( ( ph /\ G dom DProd S ) -> G dom DProd ( S |` C ) )
14 ssun2 
 |-  D C_ ( C u. D )
15 14 10 sseqtrrid 
 |-  ( ( ph /\ G dom DProd S ) -> D C_ I )
16 6 8 15 dprdres 
 |-  ( ( ph /\ G dom DProd S ) -> ( G dom DProd ( S |` D ) /\ ( G DProd ( S |` D ) ) C_ ( G DProd S ) ) )
17 16 simpld 
 |-  ( ( ph /\ G dom DProd S ) -> G dom DProd ( S |` D ) )
18 13 17 jca 
 |-  ( ( ph /\ G dom DProd S ) -> ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) )
19 2 adantr 
 |-  ( ( ph /\ G dom DProd S ) -> ( C i^i D ) = (/) )
20 6 8 11 15 19 4 dprdcntz2 
 |-  ( ( ph /\ G dom DProd S ) -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
21 6 8 11 15 19 5 dprddisj2 
 |-  ( ( ph /\ G dom DProd S ) -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )
22 18 20 21 3jca 
 |-  ( ( ph /\ G dom DProd S ) -> ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } ) )
23 1 adantr 
 |-  ( ( ph /\ ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } ) ) -> S : I --> ( SubGrp ` G ) )
24 2 adantr 
 |-  ( ( ph /\ ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } ) ) -> ( C i^i D ) = (/) )
25 3 adantr 
 |-  ( ( ph /\ ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } ) ) -> I = ( C u. D ) )
26 simpr1l 
 |-  ( ( ph /\ ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } ) ) -> G dom DProd ( S |` C ) )
27 simpr1r 
 |-  ( ( ph /\ ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } ) ) -> G dom DProd ( S |` D ) )
28 simpr2 
 |-  ( ( ph /\ ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } ) ) -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
29 simpr3 
 |-  ( ( ph /\ ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } ) ) -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )
30 23 24 25 4 5 26 27 28 29 dmdprdsplit2 
 |-  ( ( ph /\ ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } ) ) -> G dom DProd S )
31 22 30 impbida 
 |-  ( ph -> ( G dom DProd S <-> ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } ) ) )