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 φ S : I SubGrp G
dprdsplit.i φ C D =
dprdsplit.u φ I = C D
dmdprdsplit.z Z = Cntz G
dmdprdsplit.0 0 ˙ = 0 G
Assertion dmdprdsplit φ G dom DProd S G dom DProd S C G dom DProd S D G DProd S C Z G DProd S D G DProd S C G DProd S D = 0 ˙

Proof

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