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 
|- ( 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 )
dmdprdsplit2.1 
|- ( ph -> G dom DProd ( S |` C ) )
dmdprdsplit2.2 
|- ( ph -> G dom DProd ( S |` D ) )
dmdprdsplit2.3 
|- ( ph -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
dmdprdsplit2.4 
|- ( ph -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )
Assertion dmdprdsplit2 
|- ( ph -> G dom DProd S )

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 dmdprdsplit2.1 
 |-  ( ph -> G dom DProd ( S |` C ) )
7 dmdprdsplit2.2 
 |-  ( ph -> G dom DProd ( S |` D ) )
8 dmdprdsplit2.3 
 |-  ( ph -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
9 dmdprdsplit2.4 
 |-  ( ph -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )
10 eqid 
 |-  ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
11 dprdgrp 
 |-  ( G dom DProd ( S |` C ) -> G e. Grp )
12 6 11 syl 
 |-  ( ph -> G e. Grp )
13 ssun1 
 |-  C C_ ( C u. D )
14 13 3 sseqtrrid 
 |-  ( ph -> C C_ I )
15 1 14 fssresd 
 |-  ( ph -> ( S |` C ) : C --> ( SubGrp ` G ) )
16 15 fdmd 
 |-  ( ph -> dom ( S |` C ) = C )
17 6 16 dprddomcld 
 |-  ( ph -> C e. _V )
18 ssun2 
 |-  D C_ ( C u. D )
19 18 3 sseqtrrid 
 |-  ( ph -> D C_ I )
20 1 19 fssresd 
 |-  ( ph -> ( S |` D ) : D --> ( SubGrp ` G ) )
21 20 fdmd 
 |-  ( ph -> dom ( S |` D ) = D )
22 7 21 dprddomcld 
 |-  ( ph -> D e. _V )
23 unexg 
 |-  ( ( C e. _V /\ D e. _V ) -> ( C u. D ) e. _V )
24 17 22 23 syl2anc 
 |-  ( ph -> ( C u. D ) e. _V )
25 3 24 eqeltrd 
 |-  ( ph -> I e. _V )
26 3 eleq2d 
 |-  ( ph -> ( x e. I <-> x e. ( C u. D ) ) )
27 elun 
 |-  ( x e. ( C u. D ) <-> ( x e. C \/ x e. D ) )
28 26 27 bitrdi 
 |-  ( ph -> ( x e. I <-> ( x e. C \/ x e. D ) ) )
29 1 2 3 4 5 6 7 8 9 10 dmdprdsplit2lem 
 |-  ( ( ph /\ x e. C ) -> ( ( y e. I -> ( x =/= y -> ( S ` x ) C_ ( Z ` ( S ` y ) ) ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) C_ { .0. } ) )
30 incom 
 |-  ( C i^i D ) = ( D i^i C )
31 30 2 eqtr3id 
 |-  ( ph -> ( D i^i C ) = (/) )
32 uncom 
 |-  ( C u. D ) = ( D u. C )
33 3 32 eqtrdi 
 |-  ( ph -> I = ( D u. C ) )
34 dprdsubg 
 |-  ( G dom DProd ( S |` C ) -> ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) )
35 6 34 syl 
 |-  ( ph -> ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) )
36 dprdsubg 
 |-  ( G dom DProd ( S |` D ) -> ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) )
37 7 36 syl 
 |-  ( ph -> ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) )
38 4 35 37 8 cntzrecd 
 |-  ( ph -> ( G DProd ( S |` D ) ) C_ ( Z ` ( G DProd ( S |` C ) ) ) )
39 incom 
 |-  ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = ( ( G DProd ( S |` D ) ) i^i ( G DProd ( S |` C ) ) )
40 39 9 eqtr3id 
 |-  ( ph -> ( ( G DProd ( S |` D ) ) i^i ( G DProd ( S |` C ) ) ) = { .0. } )
41 1 31 33 4 5 7 6 38 40 10 dmdprdsplit2lem 
 |-  ( ( ph /\ x e. D ) -> ( ( y e. I -> ( x =/= y -> ( S ` x ) C_ ( Z ` ( S ` y ) ) ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) C_ { .0. } ) )
42 29 41 jaodan 
 |-  ( ( ph /\ ( x e. C \/ x e. D ) ) -> ( ( y e. I -> ( x =/= y -> ( S ` x ) C_ ( Z ` ( S ` y ) ) ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) C_ { .0. } ) )
43 42 simpld 
 |-  ( ( ph /\ ( x e. C \/ x e. D ) ) -> ( y e. I -> ( x =/= y -> ( S ` x ) C_ ( Z ` ( S ` y ) ) ) ) )
44 43 ex 
 |-  ( ph -> ( ( x e. C \/ x e. D ) -> ( y e. I -> ( x =/= y -> ( S ` x ) C_ ( Z ` ( S ` y ) ) ) ) ) )
45 28 44 sylbid 
 |-  ( ph -> ( x e. I -> ( y e. I -> ( x =/= y -> ( S ` x ) C_ ( Z ` ( S ` y ) ) ) ) ) )
46 45 3imp2 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> ( S ` x ) C_ ( Z ` ( S ` y ) ) )
47 28 biimpa 
 |-  ( ( ph /\ x e. I ) -> ( x e. C \/ x e. D ) )
48 29 simprd 
 |-  ( ( ph /\ x e. C ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) C_ { .0. } )
49 41 simprd 
 |-  ( ( ph /\ x e. D ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) C_ { .0. } )
50 48 49 jaodan 
 |-  ( ( ph /\ ( x e. C \/ x e. D ) ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) C_ { .0. } )
51 47 50 syldan 
 |-  ( ( ph /\ x e. I ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) C_ { .0. } )
52 4 5 10 12 25 1 46 51 dmdprdd 
 |-  ( ph -> G dom DProd S )