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

Metamath Proof Explorer

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