Step |
Hyp |
Ref |
Expression |
1 |
|
dprdres.1 |
|- ( ph -> G dom DProd S ) |
2 |
|
dprdres.2 |
|- ( ph -> dom S = I ) |
3 |
|
dprdres.3 |
|- ( ph -> A C_ I ) |
4 |
|
dprdgrp |
|- ( G dom DProd S -> G e. Grp ) |
5 |
1 4
|
syl |
|- ( ph -> G e. Grp ) |
6 |
1 2
|
dprdf2 |
|- ( ph -> S : I --> ( SubGrp ` G ) ) |
7 |
6 3
|
fssresd |
|- ( ph -> ( S |` A ) : A --> ( SubGrp ` G ) ) |
8 |
1
|
ad2antrr |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> G dom DProd S ) |
9 |
2
|
ad2antrr |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> dom S = I ) |
10 |
3
|
ad2antrr |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> A C_ I ) |
11 |
|
simplr |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> x e. A ) |
12 |
10 11
|
sseldd |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> x e. I ) |
13 |
|
eldifi |
|- ( y e. ( A \ { x } ) -> y e. A ) |
14 |
13
|
adantl |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> y e. A ) |
15 |
10 14
|
sseldd |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> y e. I ) |
16 |
|
eldifsni |
|- ( y e. ( A \ { x } ) -> y =/= x ) |
17 |
16
|
adantl |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> y =/= x ) |
18 |
17
|
necomd |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> x =/= y ) |
19 |
|
eqid |
|- ( Cntz ` G ) = ( Cntz ` G ) |
20 |
8 9 12 15 18 19
|
dprdcntz |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) ) |
21 |
11
|
fvresd |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> ( ( S |` A ) ` x ) = ( S ` x ) ) |
22 |
14
|
fvresd |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> ( ( S |` A ) ` y ) = ( S ` y ) ) |
23 |
22
|
fveq2d |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) = ( ( Cntz ` G ) ` ( S ` y ) ) ) |
24 |
20 21 23
|
3sstr4d |
|- ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> ( ( S |` A ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) ) |
25 |
24
|
ralrimiva |
|- ( ( ph /\ x e. A ) -> A. y e. ( A \ { x } ) ( ( S |` A ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) ) |
26 |
|
fvres |
|- ( x e. A -> ( ( S |` A ) ` x ) = ( S ` x ) ) |
27 |
26
|
adantl |
|- ( ( ph /\ x e. A ) -> ( ( S |` A ) ` x ) = ( S ` x ) ) |
28 |
27
|
ineq1d |
|- ( ( ph /\ x e. A ) -> ( ( ( S |` A ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) ) |
29 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
30 |
29
|
subgacs |
|- ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) ) |
31 |
|
acsmre |
|- ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) ) |
32 |
5 30 31
|
3syl |
|- ( ph -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) ) |
33 |
32
|
adantr |
|- ( ( ph /\ x e. A ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) ) |
34 |
|
eqid |
|- ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) ) |
35 |
|
resss |
|- ( S |` A ) C_ S |
36 |
|
imass1 |
|- ( ( S |` A ) C_ S -> ( ( S |` A ) " ( A \ { x } ) ) C_ ( S " ( A \ { x } ) ) ) |
37 |
35 36
|
ax-mp |
|- ( ( S |` A ) " ( A \ { x } ) ) C_ ( S " ( A \ { x } ) ) |
38 |
3
|
adantr |
|- ( ( ph /\ x e. A ) -> A C_ I ) |
39 |
|
ssdif |
|- ( A C_ I -> ( A \ { x } ) C_ ( I \ { x } ) ) |
40 |
|
imass2 |
|- ( ( A \ { x } ) C_ ( I \ { x } ) -> ( S " ( A \ { x } ) ) C_ ( S " ( I \ { x } ) ) ) |
41 |
38 39 40
|
3syl |
|- ( ( ph /\ x e. A ) -> ( S " ( A \ { x } ) ) C_ ( S " ( I \ { x } ) ) ) |
42 |
37 41
|
sstrid |
|- ( ( ph /\ x e. A ) -> ( ( S |` A ) " ( A \ { x } ) ) C_ ( S " ( I \ { x } ) ) ) |
43 |
42
|
unissd |
|- ( ( ph /\ x e. A ) -> U. ( ( S |` A ) " ( A \ { x } ) ) C_ U. ( S " ( I \ { x } ) ) ) |
44 |
|
imassrn |
|- ( S " ( I \ { x } ) ) C_ ran S |
45 |
6
|
frnd |
|- ( ph -> ran S C_ ( SubGrp ` G ) ) |
46 |
29
|
subgss |
|- ( x e. ( SubGrp ` G ) -> x C_ ( Base ` G ) ) |
47 |
|
velpw |
|- ( x e. ~P ( Base ` G ) <-> x C_ ( Base ` G ) ) |
48 |
46 47
|
sylibr |
|- ( x e. ( SubGrp ` G ) -> x e. ~P ( Base ` G ) ) |
49 |
48
|
ssriv |
|- ( SubGrp ` G ) C_ ~P ( Base ` G ) |
50 |
45 49
|
sstrdi |
|- ( ph -> ran S C_ ~P ( Base ` G ) ) |
51 |
50
|
adantr |
|- ( ( ph /\ x e. A ) -> ran S C_ ~P ( Base ` G ) ) |
52 |
44 51
|
sstrid |
|- ( ( ph /\ x e. A ) -> ( S " ( I \ { x } ) ) C_ ~P ( Base ` G ) ) |
53 |
|
sspwuni |
|- ( ( S " ( I \ { x } ) ) C_ ~P ( Base ` G ) <-> U. ( S " ( I \ { x } ) ) C_ ( Base ` G ) ) |
54 |
52 53
|
sylib |
|- ( ( ph /\ x e. A ) -> U. ( S " ( I \ { x } ) ) C_ ( Base ` G ) ) |
55 |
33 34 43 54
|
mrcssd |
|- ( ( ph /\ x e. A ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) |
56 |
|
sslin |
|- ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) C_ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) ) |
57 |
55 56
|
syl |
|- ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) C_ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) ) |
58 |
1
|
adantr |
|- ( ( ph /\ x e. A ) -> G dom DProd S ) |
59 |
2
|
adantr |
|- ( ( ph /\ x e. A ) -> dom S = I ) |
60 |
3
|
sselda |
|- ( ( ph /\ x e. A ) -> x e. I ) |
61 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
62 |
58 59 60 61 34
|
dprddisj |
|- ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) |
63 |
57 62
|
sseqtrd |
|- ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) C_ { ( 0g ` G ) } ) |
64 |
6
|
ffvelrnda |
|- ( ( ph /\ x e. I ) -> ( S ` x ) e. ( SubGrp ` G ) ) |
65 |
60 64
|
syldan |
|- ( ( ph /\ x e. A ) -> ( S ` x ) e. ( SubGrp ` G ) ) |
66 |
61
|
subg0cl |
|- ( ( S ` x ) e. ( SubGrp ` G ) -> ( 0g ` G ) e. ( S ` x ) ) |
67 |
65 66
|
syl |
|- ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( S ` x ) ) |
68 |
43 54
|
sstrd |
|- ( ( ph /\ x e. A ) -> U. ( ( S |` A ) " ( A \ { x } ) ) C_ ( Base ` G ) ) |
69 |
34
|
mrccl |
|- ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ( ( S |` A ) " ( A \ { x } ) ) C_ ( Base ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) e. ( SubGrp ` G ) ) |
70 |
33 68 69
|
syl2anc |
|- ( ( ph /\ x e. A ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) e. ( SubGrp ` G ) ) |
71 |
61
|
subg0cl |
|- ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) e. ( SubGrp ` G ) -> ( 0g ` G ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) |
72 |
70 71
|
syl |
|- ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) |
73 |
67 72
|
elind |
|- ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) ) |
74 |
73
|
snssd |
|- ( ( ph /\ x e. A ) -> { ( 0g ` G ) } C_ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) ) |
75 |
63 74
|
eqssd |
|- ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = { ( 0g ` G ) } ) |
76 |
28 75
|
eqtrd |
|- ( ( ph /\ x e. A ) -> ( ( ( S |` A ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = { ( 0g ` G ) } ) |
77 |
25 76
|
jca |
|- ( ( ph /\ x e. A ) -> ( A. y e. ( A \ { x } ) ( ( S |` A ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) /\ ( ( ( S |` A ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) |
78 |
77
|
ralrimiva |
|- ( ph -> A. x e. A ( A. y e. ( A \ { x } ) ( ( S |` A ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) /\ ( ( ( S |` A ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) |
79 |
1 2
|
dprddomcld |
|- ( ph -> I e. _V ) |
80 |
79 3
|
ssexd |
|- ( ph -> A e. _V ) |
81 |
7
|
fdmd |
|- ( ph -> dom ( S |` A ) = A ) |
82 |
19 61 34
|
dmdprd |
|- ( ( A e. _V /\ dom ( S |` A ) = A ) -> ( G dom DProd ( S |` A ) <-> ( G e. Grp /\ ( S |` A ) : A --> ( SubGrp ` G ) /\ A. x e. A ( A. y e. ( A \ { x } ) ( ( S |` A ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) /\ ( ( ( S |` A ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) ) |
83 |
80 81 82
|
syl2anc |
|- ( ph -> ( G dom DProd ( S |` A ) <-> ( G e. Grp /\ ( S |` A ) : A --> ( SubGrp ` G ) /\ A. x e. A ( A. y e. ( A \ { x } ) ( ( S |` A ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) /\ ( ( ( S |` A ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) ) |
84 |
5 7 78 83
|
mpbir3and |
|- ( ph -> G dom DProd ( S |` A ) ) |
85 |
|
rnss |
|- ( ( S |` A ) C_ S -> ran ( S |` A ) C_ ran S ) |
86 |
|
uniss |
|- ( ran ( S |` A ) C_ ran S -> U. ran ( S |` A ) C_ U. ran S ) |
87 |
35 85 86
|
mp2b |
|- U. ran ( S |` A ) C_ U. ran S |
88 |
87
|
a1i |
|- ( ph -> U. ran ( S |` A ) C_ U. ran S ) |
89 |
|
sspwuni |
|- ( ran S C_ ~P ( Base ` G ) <-> U. ran S C_ ( Base ` G ) ) |
90 |
50 89
|
sylib |
|- ( ph -> U. ran S C_ ( Base ` G ) ) |
91 |
32 34 88 90
|
mrcssd |
|- ( ph -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran ( S |` A ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) ) |
92 |
34
|
dprdspan |
|- ( G dom DProd ( S |` A ) -> ( G DProd ( S |` A ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran ( S |` A ) ) ) |
93 |
84 92
|
syl |
|- ( ph -> ( G DProd ( S |` A ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran ( S |` A ) ) ) |
94 |
34
|
dprdspan |
|- ( G dom DProd S -> ( G DProd S ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) ) |
95 |
1 94
|
syl |
|- ( ph -> ( G DProd S ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) ) |
96 |
91 93 95
|
3sstr4d |
|- ( ph -> ( G DProd ( S |` A ) ) C_ ( G DProd S ) ) |
97 |
84 96
|
jca |
|- ( ph -> ( G dom DProd ( S |` A ) /\ ( G DProd ( S |` A ) ) C_ ( G DProd S ) ) ) |