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