Step |
Hyp |
Ref |
Expression |
1 |
|
reldmdprd |
|- Rel dom DProd |
2 |
1
|
brrelex2i |
|- ( G dom DProd S -> S e. _V ) |
3 |
2
|
dmexd |
|- ( G dom DProd S -> dom S e. _V ) |
4 |
|
eqid |
|- dom S = dom S |
5 |
|
eqid |
|- ( Cntz ` G ) = ( Cntz ` G ) |
6 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
7 |
|
eqid |
|- ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) ) |
8 |
5 6 7
|
dmdprd |
|- ( ( dom S e. _V /\ dom S = dom S ) -> ( G dom DProd S <-> ( G e. Grp /\ S : dom S --> ( SubGrp ` G ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) ) |
9 |
3 4 8
|
sylancl |
|- ( G dom DProd S -> ( G dom DProd S <-> ( G e. Grp /\ S : dom S --> ( SubGrp ` G ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) ) |
10 |
9
|
ibi |
|- ( G dom DProd S -> ( G e. Grp /\ S : dom S --> ( SubGrp ` G ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) |
11 |
10
|
simp1d |
|- ( G dom DProd S -> G e. Grp ) |