Metamath Proof Explorer


Theorem dpjdisj

Description: The two subgroups that appear in dpjval are disjoint. (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
dpjdisj.0 0 ˙ = 0 G
Assertion dpjdisj φ S X G DProd S I X = 0 ˙

Proof

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