Theorem dpjdisj

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

	Ref	Expression
Hypotheses	dpjfval.1	|- ( ph -> G dom DProd S )
	dpjfval.2	|- ( ph -> dom S = I )
	dpjlem.3	|- ( ph -> X e. I )
	dpjdisj.0	|- .0. = ( 0g ` G )
Assertion	dpjdisj	|- ( ph -> ( ( S ` X ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) = { .0. } )

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	|- ( ph -> G dom DProd S )
2		dpjfval.2	|- ( ph -> dom S = I )
3		dpjlem.3	|- ( ph -> X e. I )
4		dpjdisj.0	|- .0. = ( 0g ` G )
5	1 2 3	dpjlem	|- ( ph -> ( G DProd ( S |` { X } ) ) = ( S ` X ) )
6	5	ineq1d	|- ( ph -> ( ( G DProd ( S |` { X } ) ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) = ( ( S ` X ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) )
7	1 2	dprdf2	|- ( ph -> S : I --> ( SubGrp ` G ) )
8		disjdif	|- ( { X } i^i ( I \ { X } ) ) = (/)
9	8	a1i	|- ( ph -> ( { X } i^i ( I \ { X } ) ) = (/) )
10		undif2	|- ( { X } u. ( I \ { X } ) ) = ( { X } u. I )
11	3	snssd	|- ( ph -> { X } C_ I )
12		ssequn1	|- ( { X } C_ I <-> ( { X } u. I ) = I )
13	11 12	sylib	|- ( ph -> ( { X } u. I ) = I )
14	10 13	eqtr2id	|- ( ph -> I = ( { X } u. ( I \ { X } ) ) )
15		eqid	|- ( Cntz ` G ) = ( Cntz ` G )
16	7 9 14 15 4	dmdprdsplit	|- ( ph -> ( G dom DProd S <-> ( ( G dom DProd ( S |` { X } ) /\ G dom DProd ( S |` ( I \ { X } ) ) ) /\ ( G DProd ( S |` { X } ) ) C_ ( ( Cntz ` G ) ` ( G DProd ( S |` ( I \ { X } ) ) ) ) /\ ( ( G DProd ( S |` { X } ) ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) = { .0. } ) ) )
17	1 16	mpbid	|- ( ph -> ( ( G dom DProd ( S |` { X } ) /\ G dom DProd ( S |` ( I \ { X } ) ) ) /\ ( G DProd ( S |` { X } ) ) C_ ( ( Cntz ` G ) ` ( G DProd ( S |` ( I \ { X } ) ) ) ) /\ ( ( G DProd ( S |` { X } ) ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) = { .0. } ) )
18	17	simp3d	|- ( ph -> ( ( G DProd ( S |` { X } ) ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) = { .0. } )
19	6 18	eqtr3d	|- ( ph -> ( ( S ` X ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) = { .0. } )