Theorem dprddisj

Description: The function S is a family having trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	dprdcntz.1	|- ( ph -> G dom DProd S )
	dprdcntz.2	|- ( ph -> dom S = I )
	dprdcntz.3	|- ( ph -> X e. I )
	dprddisj.0	|- .0. = ( 0g ` G )
	dprddisj.k	|- K = ( mrCls ` ( SubGrp ` G ) )
Assertion	dprddisj	|- ( ph -> ( ( S ` X ) i^i ( K ` U. ( S " ( I \ { X } ) ) ) ) = { .0. } )

Proof

Step	Hyp	Ref	Expression
1		dprdcntz.1	|- ( ph -> G dom DProd S )
2		dprdcntz.2	|- ( ph -> dom S = I )
3		dprdcntz.3	|- ( ph -> X e. I )
4		dprddisj.0	|- .0. = ( 0g ` G )
5		dprddisj.k	|- K = ( mrCls ` ( SubGrp ` G ) )
6		fveq2	|- ( x = X -> ( S ` x ) = ( S ` X ) )
7		sneq	|- ( x = X -> { x } = { X } )
8	7	difeq2d	|- ( x = X -> ( I \ { x } ) = ( I \ { X } ) )
9	8	imaeq2d	|- ( x = X -> ( S " ( I \ { x } ) ) = ( S " ( I \ { X } ) ) )
10	9	unieqd	|- ( x = X -> U. ( S " ( I \ { x } ) ) = U. ( S " ( I \ { X } ) ) )
11	10	fveq2d	|- ( x = X -> ( K ` U. ( S " ( I \ { x } ) ) ) = ( K ` U. ( S " ( I \ { X } ) ) ) )
12	6 11	ineq12d	|- ( x = X -> ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = ( ( S ` X ) i^i ( K ` U. ( S " ( I \ { X } ) ) ) ) )
13	12	eqeq1d	|- ( x = X -> ( ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } <-> ( ( S ` X ) i^i ( K ` U. ( S " ( I \ { X } ) ) ) ) = { .0. } ) )
14	1 2	dprddomcld	|- ( ph -> I e. _V )
15		eqid	|- ( Cntz ` G ) = ( Cntz ` G )
16	15 4 5	dmdprd	|- ( ( I e. _V /\ dom S = I ) -> ( G dom DProd S <-> ( G e. Grp /\ S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )
17	14 2 16	syl2anc	|- ( ph -> ( G dom DProd S <-> ( G e. Grp /\ S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )
18	1 17	mpbid	|- ( ph -> ( G e. Grp /\ S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) )
19	18	simp3d	|- ( ph -> A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) )
20		simpr	|- ( ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } )
21	20	ralimi	|- ( A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) -> A. x e. I ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } )
22	19 21	syl	|- ( ph -> A. x e. I ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } )
23	13 22 3	rspcdva	|- ( ph -> ( ( S ` X ) i^i ( K ` U. ( S " ( I \ { X } ) ) ) ) = { .0. } )