Metamath Proof Explorer

Theorem dprdsplit

Description: The direct product is the binary subgroup product ("sum") of the direct products of the partition. (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 ) )
dprdsplit.s 
|- .(+) = ( LSSum ` G )
dprdsplit.1 
|- ( ph -> G dom DProd S )
Assertion dprdsplit 
|- ( ph -> ( G DProd S ) = ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )

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 dprdsplit.s 
 |-  .(+) = ( LSSum ` G )
5 dprdsplit.1 
 |-  ( ph -> G dom DProd S )
6 1 fdmd 
 |-  ( ph -> dom S = I )
7 ssun1 
 |-  C C_ ( C u. D )
8 7 3 sseqtrrid 
 |-  ( ph -> C C_ I )
9 5 6 8 dprdres 
 |-  ( ph -> ( G dom DProd ( S |` C ) /\ ( G DProd ( S |` C ) ) C_ ( G DProd S ) ) )
10 9 simpld 
 |-  ( ph -> G dom DProd ( S |` C ) )
11 dprdsubg 
 |-  ( G dom DProd ( S |` C ) -> ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) )
12 10 11 syl 
 |-  ( ph -> ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) )
13 ssun2 
 |-  D C_ ( C u. D )
14 13 3 sseqtrrid 
 |-  ( ph -> D C_ I )
15 5 6 14 dprdres 
 |-  ( ph -> ( G dom DProd ( S |` D ) /\ ( G DProd ( S |` D ) ) C_ ( G DProd S ) ) )
16 15 simpld 
 |-  ( ph -> G dom DProd ( S |` D ) )
17 dprdsubg 
 |-  ( G dom DProd ( S |` D ) -> ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) )
18 16 17 syl 
 |-  ( ph -> ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) )
19 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
20 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
21 1 2 3 19 20 dmdprdsplit 
 |-  ( ph -> ( G dom DProd S <-> ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( ( Cntz ` G ) ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { ( 0g ` G ) } ) ) )
22 5 21 mpbid 
 |-  ( ph -> ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( ( Cntz ` G ) ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { ( 0g ` G ) } ) )
23 22 simp2d 
 |-  ( ph -> ( G DProd ( S |` C ) ) C_ ( ( Cntz ` G ) ` ( G DProd ( S |` D ) ) ) )
24 4 19 lsmsubg 
 |-  ( ( ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) /\ ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) /\ ( G DProd ( S |` C ) ) C_ ( ( Cntz ` G ) ` ( G DProd ( S |` D ) ) ) ) -> ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) e. ( SubGrp ` G ) )
25 12 18 23 24 syl3anc 
 |-  ( ph -> ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) e. ( SubGrp ` G ) )
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 28 biimpa 
 |-  ( ( ph /\ x e. I ) -> ( x e. C \/ x e. D ) )
30 fvres 
 |-  ( x e. C -> ( ( S |` C ) ` x ) = ( S ` x ) )
31 30 adantl 
 |-  ( ( ph /\ x e. C ) -> ( ( S |` C ) ` x ) = ( S ` x ) )
32 10 adantr 
 |-  ( ( ph /\ x e. C ) -> G dom DProd ( S |` C ) )
33 1 8 fssresd 
 |-  ( ph -> ( S |` C ) : C --> ( SubGrp ` G ) )
34 33 fdmd 
 |-  ( ph -> dom ( S |` C ) = C )
35 34 adantr 
 |-  ( ( ph /\ x e. C ) -> dom ( S |` C ) = C )
36 simpr 
 |-  ( ( ph /\ x e. C ) -> x e. C )
37 32 35 36 dprdub 
 |-  ( ( ph /\ x e. C ) -> ( ( S |` C ) ` x ) C_ ( G DProd ( S |` C ) ) )
38 31 37 eqsstrrd 
 |-  ( ( ph /\ x e. C ) -> ( S ` x ) C_ ( G DProd ( S |` C ) ) )
39 4 lsmub1 
 |-  ( ( ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) /\ ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) ) -> ( G DProd ( S |` C ) ) C_ ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )
40 12 18 39 syl2anc 
 |-  ( ph -> ( G DProd ( S |` C ) ) C_ ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )
41 40 adantr 
 |-  ( ( ph /\ x e. C ) -> ( G DProd ( S |` C ) ) C_ ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )
42 38 41 sstrd 
 |-  ( ( ph /\ x e. C ) -> ( S ` x ) C_ ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )
43 fvres 
 |-  ( x e. D -> ( ( S |` D ) ` x ) = ( S ` x ) )
44 43 adantl 
 |-  ( ( ph /\ x e. D ) -> ( ( S |` D ) ` x ) = ( S ` x ) )
45 16 adantr 
 |-  ( ( ph /\ x e. D ) -> G dom DProd ( S |` D ) )
46 1 14 fssresd 
 |-  ( ph -> ( S |` D ) : D --> ( SubGrp ` G ) )
47 46 fdmd 
 |-  ( ph -> dom ( S |` D ) = D )
48 47 adantr 
 |-  ( ( ph /\ x e. D ) -> dom ( S |` D ) = D )
49 simpr 
 |-  ( ( ph /\ x e. D ) -> x e. D )
50 45 48 49 dprdub 
 |-  ( ( ph /\ x e. D ) -> ( ( S |` D ) ` x ) C_ ( G DProd ( S |` D ) ) )
51 44 50 eqsstrrd 
 |-  ( ( ph /\ x e. D ) -> ( S ` x ) C_ ( G DProd ( S |` D ) ) )
52 4 lsmub2 
 |-  ( ( ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) /\ ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) ) -> ( G DProd ( S |` D ) ) C_ ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )
53 12 18 52 syl2anc 
 |-  ( ph -> ( G DProd ( S |` D ) ) C_ ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )
54 53 adantr 
 |-  ( ( ph /\ x e. D ) -> ( G DProd ( S |` D ) ) C_ ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )
55 51 54 sstrd 
 |-  ( ( ph /\ x e. D ) -> ( S ` x ) C_ ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )
56 42 55 jaodan 
 |-  ( ( ph /\ ( x e. C \/ x e. D ) ) -> ( S ` x ) C_ ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )
57 29 56 syldan 
 |-  ( ( ph /\ x e. I ) -> ( S ` x ) C_ ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )
58 5 6 25 57 dprdlub 
 |-  ( ph -> ( G DProd S ) C_ ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )
59 9 simprd 
 |-  ( ph -> ( G DProd ( S |` C ) ) C_ ( G DProd S ) )
60 15 simprd 
 |-  ( ph -> ( G DProd ( S |` D ) ) C_ ( G DProd S ) )
61 dprdsubg 
 |-  ( G dom DProd S -> ( G DProd S ) e. ( SubGrp ` G ) )
62 5 61 syl 
 |-  ( ph -> ( G DProd S ) e. ( SubGrp ` G ) )
63 4 lsmlub 
 |-  ( ( ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) /\ ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) /\ ( G DProd S ) e. ( SubGrp ` G ) ) -> ( ( ( G DProd ( S |` C ) ) C_ ( G DProd S ) /\ ( G DProd ( S |` D ) ) C_ ( G DProd S ) ) <-> ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) C_ ( G DProd S ) ) )
64 12 18 62 63 syl3anc 
 |-  ( ph -> ( ( ( G DProd ( S |` C ) ) C_ ( G DProd S ) /\ ( G DProd ( S |` D ) ) C_ ( G DProd S ) ) <-> ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) C_ ( G DProd S ) ) )
65 59 60 64 mpbi2and 
 |-  ( ph -> ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) C_ ( G DProd S ) )
66 58 65 eqssd 
 |-  ( ph -> ( G DProd S ) = ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )