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 φ S : I SubGrp G
dprdsplit.i φ C D =
dprdsplit.u φ I = C D
dprdsplit.s ˙ = LSSum G
dprdsplit.1 φ G dom DProd S
Assertion dprdsplit φ G DProd S = G DProd S C ˙ G DProd S D

Proof

Step Hyp Ref Expression
1 dprdsplit.2 φ S : I SubGrp G
2 dprdsplit.i φ C D =
3 dprdsplit.u φ I = C D
4 dprdsplit.s ˙ = LSSum G
5 dprdsplit.1 φ G dom DProd S
6 1 fdmd φ dom S = I
7 ssun1 C C D
8 7 3 sseqtrrid φ C I
9 5 6 8 dprdres φ G dom DProd S C G DProd S C G DProd S
10 9 simpld φ G dom DProd S C
11 dprdsubg G dom DProd S C G DProd S C SubGrp G
12 10 11 syl φ G DProd S C SubGrp G
13 ssun2 D C D
14 13 3 sseqtrrid φ D I
15 5 6 14 dprdres φ G dom DProd S D G DProd S D G DProd S
16 15 simpld φ G dom DProd S D
17 dprdsubg G dom DProd S D G DProd S D SubGrp G
18 16 17 syl φ G DProd S D SubGrp G
19 eqid Cntz G = Cntz G
20 eqid 0 G = 0 G
21 1 2 3 19 20 dmdprdsplit φ G dom DProd S G dom DProd S C G dom DProd S D G DProd S C Cntz G G DProd S D G DProd S C G DProd S D = 0 G
22 5 21 mpbid φ G dom DProd S C G dom DProd S D G DProd S C Cntz G G DProd S D G DProd S C G DProd S D = 0 G
23 22 simp2d φ G DProd S C Cntz G G DProd S D
24 4 19 lsmsubg G DProd S C SubGrp G G DProd S D SubGrp G G DProd S C Cntz G G DProd S D G DProd S C ˙ G DProd S D SubGrp G
25 12 18 23 24 syl3anc φ G DProd S C ˙ G DProd S D SubGrp G
26 3 eleq2d φ x I x C D
27 elun x C D x C x D
28 26 27 bitrdi φ x I x C x D
29 28 biimpa φ x I x C x D
30 fvres x C S C x = S x
31 30 adantl φ x C S C x = S x
32 10 adantr φ x C G dom DProd S C
33 1 8 fssresd φ S C : C SubGrp G
34 33 fdmd φ dom S C = C
35 34 adantr φ x C dom S C = C
36 simpr φ x C x C
37 32 35 36 dprdub φ x C S C x G DProd S C
38 31 37 eqsstrrd φ x C S x G DProd S C
39 4 lsmub1 G DProd S C SubGrp G G DProd S D SubGrp G G DProd S C G DProd S C ˙ G DProd S D
40 12 18 39 syl2anc φ G DProd S C G DProd S C ˙ G DProd S D
41 40 adantr φ x C G DProd S C G DProd S C ˙ G DProd S D
42 38 41 sstrd φ x C S x G DProd S C ˙ G DProd S D
43 fvres x D S D x = S x
44 43 adantl φ x D S D x = S x
45 16 adantr φ x D G dom DProd S D
46 1 14 fssresd φ S D : D SubGrp G
47 46 fdmd φ dom S D = D
48 47 adantr φ x D dom S D = D
49 simpr φ x D x D
50 45 48 49 dprdub φ x D S D x G DProd S D
51 44 50 eqsstrrd φ x D S x G DProd S D
52 4 lsmub2 G DProd S C SubGrp G G DProd S D SubGrp G G DProd S D G DProd S C ˙ G DProd S D
53 12 18 52 syl2anc φ G DProd S D G DProd S C ˙ G DProd S D
54 53 adantr φ x D G DProd S D G DProd S C ˙ G DProd S D
55 51 54 sstrd φ x D S x G DProd S C ˙ G DProd S D
56 42 55 jaodan φ x C x D S x G DProd S C ˙ G DProd S D
57 29 56 syldan φ x I S x G DProd S C ˙ G DProd S D
58 5 6 25 57 dprdlub φ G DProd S G DProd S C ˙ G DProd S D
59 9 simprd φ G DProd S C G DProd S
60 15 simprd φ G DProd S D G DProd S
61 dprdsubg G dom DProd S G DProd S SubGrp G
62 5 61 syl φ G DProd S SubGrp G
63 4 lsmlub G DProd S C SubGrp G G DProd S D SubGrp G G DProd S SubGrp G G DProd S C G DProd S G DProd S D G DProd S G DProd S C ˙ G DProd S D G DProd S
64 12 18 62 63 syl3anc φ G DProd S C G DProd S G DProd S D G DProd S G DProd S C ˙ G DProd S D G DProd S
65 59 60 64 mpbi2and φ G DProd S C ˙ G DProd S D G DProd S
66 58 65 eqssd φ G DProd S = G DProd S C ˙ G DProd S D