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 |
|
dprdcntz.4 |
|- ( ph -> Y e. I ) |
5 |
|
dprdcntz.5 |
|- ( ph -> X =/= Y ) |
6 |
|
dprdcntz.z |
|- Z = ( Cntz ` G ) |
7 |
|
2fveq3 |
|- ( y = Y -> ( Z ` ( S ` y ) ) = ( Z ` ( S ` Y ) ) ) |
8 |
7
|
sseq2d |
|- ( y = Y -> ( ( S ` X ) C_ ( Z ` ( S ` y ) ) <-> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) ) |
9 |
|
sneq |
|- ( x = X -> { x } = { X } ) |
10 |
9
|
difeq2d |
|- ( x = X -> ( I \ { x } ) = ( I \ { X } ) ) |
11 |
|
fveq2 |
|- ( x = X -> ( S ` x ) = ( S ` X ) ) |
12 |
11
|
sseq1d |
|- ( x = X -> ( ( S ` x ) C_ ( Z ` ( S ` y ) ) <-> ( S ` X ) C_ ( Z ` ( S ` y ) ) ) ) |
13 |
10 12
|
raleqbidv |
|- ( x = X -> ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) <-> A. y e. ( I \ { X } ) ( S ` X ) C_ ( Z ` ( S ` y ) ) ) ) |
14 |
1 2
|
dprddomcld |
|- ( ph -> I e. _V ) |
15 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
16 |
|
eqid |
|- ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) ) |
17 |
6 15 16
|
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_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) ) |
18 |
14 2 17
|
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_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) ) |
19 |
1 18
|
mpbid |
|- ( ph -> ( G e. Grp /\ S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) |
20 |
19
|
simp3d |
|- ( ph -> A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) |
21 |
|
simpl |
|- ( ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) -> A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) ) |
22 |
21
|
ralimi |
|- ( A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) -> A. x e. I A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) ) |
23 |
20 22
|
syl |
|- ( ph -> A. x e. I A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) ) |
24 |
13 23 3
|
rspcdva |
|- ( ph -> A. y e. ( I \ { X } ) ( S ` X ) C_ ( Z ` ( S ` y ) ) ) |
25 |
5
|
necomd |
|- ( ph -> Y =/= X ) |
26 |
|
eldifsn |
|- ( Y e. ( I \ { X } ) <-> ( Y e. I /\ Y =/= X ) ) |
27 |
4 25 26
|
sylanbrc |
|- ( ph -> Y e. ( I \ { X } ) ) |
28 |
8 24 27
|
rspcdva |
|- ( ph -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) |