Metamath Proof Explorer


Theorem dpjcntz

Description: The two subgroups that appear in dpjval commute. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dpjfval.1 φ G dom DProd S
dpjfval.2 φ dom S = I
dpjlem.3 φ X I
dpjcntz.z Z = Cntz G
Assertion dpjcntz φ S X Z G DProd S I X

Proof

Step Hyp Ref Expression
1 dpjfval.1 φ G dom DProd S
2 dpjfval.2 φ dom S = I
3 dpjlem.3 φ X I
4 dpjcntz.z Z = Cntz G
5 1 2 3 dpjlem φ G DProd S X = S X
6 1 2 dprdf2 φ S : I SubGrp G
7 disjdif X I X =
8 7 a1i φ X I X =
9 undif2 X I X = X I
10 3 snssd φ X I
11 ssequn1 X I X I = I
12 10 11 sylib φ X I = I
13 9 12 eqtr2id φ I = X I X
14 eqid 0 G = 0 G
15 6 8 13 4 14 dmdprdsplit φ G dom DProd S G dom DProd S X G dom DProd S I X G DProd S X Z G DProd S I X G DProd S X G DProd S I X = 0 G
16 1 15 mpbid φ G dom DProd S X G dom DProd S I X G DProd S X Z G DProd S I X G DProd S X G DProd S I X = 0 G
17 16 simp2d φ G DProd S X Z G DProd S I X
18 5 17 eqsstrrd φ S X Z G DProd S I X