This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	\|- ( 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. } )