Step |
Hyp |
Ref |
Expression |
1 |
|
subgdprd.1 |
|- H = ( G |`s A ) |
2 |
|
subgdprd.2 |
|- ( ph -> A e. ( SubGrp ` G ) ) |
3 |
|
subgdprd.3 |
|- ( ph -> G dom DProd S ) |
4 |
|
subgdprd.4 |
|- ( ph -> ran S C_ ~P A ) |
5 |
1
|
subggrp |
|- ( A e. ( SubGrp ` G ) -> H e. Grp ) |
6 |
2 5
|
syl |
|- ( ph -> H e. Grp ) |
7 |
|
eqid |
|- ( Base ` H ) = ( Base ` H ) |
8 |
7
|
subgacs |
|- ( H e. Grp -> ( SubGrp ` H ) e. ( ACS ` ( Base ` H ) ) ) |
9 |
|
acsmre |
|- ( ( SubGrp ` H ) e. ( ACS ` ( Base ` H ) ) -> ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) ) |
10 |
6 8 9
|
3syl |
|- ( ph -> ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) ) |
11 |
|
subgrcl |
|- ( A e. ( SubGrp ` G ) -> G e. Grp ) |
12 |
2 11
|
syl |
|- ( ph -> G e. Grp ) |
13 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
14 |
13
|
subgacs |
|- ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) ) |
15 |
|
acsmre |
|- ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) ) |
16 |
12 14 15
|
3syl |
|- ( ph -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) ) |
17 |
|
eqid |
|- ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) ) |
18 |
|
dprdf |
|- ( G dom DProd S -> S : dom S --> ( SubGrp ` G ) ) |
19 |
|
frn |
|- ( S : dom S --> ( SubGrp ` G ) -> ran S C_ ( SubGrp ` G ) ) |
20 |
3 18 19
|
3syl |
|- ( ph -> ran S C_ ( SubGrp ` G ) ) |
21 |
|
mresspw |
|- ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) ) |
22 |
16 21
|
syl |
|- ( ph -> ( SubGrp ` G ) C_ ~P ( Base ` G ) ) |
23 |
20 22
|
sstrd |
|- ( ph -> ran S C_ ~P ( Base ` G ) ) |
24 |
|
sspwuni |
|- ( ran S C_ ~P ( Base ` G ) <-> U. ran S C_ ( Base ` G ) ) |
25 |
23 24
|
sylib |
|- ( ph -> U. ran S C_ ( Base ` G ) ) |
26 |
16 17 25
|
mrcssidd |
|- ( ph -> U. ran S C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) ) |
27 |
17
|
mrccl |
|- ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ran S C_ ( Base ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) e. ( SubGrp ` G ) ) |
28 |
16 25 27
|
syl2anc |
|- ( ph -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) e. ( SubGrp ` G ) ) |
29 |
|
sspwuni |
|- ( ran S C_ ~P A <-> U. ran S C_ A ) |
30 |
4 29
|
sylib |
|- ( ph -> U. ran S C_ A ) |
31 |
17
|
mrcsscl |
|- ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ran S C_ A /\ A e. ( SubGrp ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) C_ A ) |
32 |
16 30 2 31
|
syl3anc |
|- ( ph -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) C_ A ) |
33 |
1
|
subsubg |
|- ( A e. ( SubGrp ` G ) -> ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) e. ( SubGrp ` H ) <-> ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) e. ( SubGrp ` G ) /\ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) C_ A ) ) ) |
34 |
2 33
|
syl |
|- ( ph -> ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) e. ( SubGrp ` H ) <-> ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) e. ( SubGrp ` G ) /\ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) C_ A ) ) ) |
35 |
28 32 34
|
mpbir2and |
|- ( ph -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) e. ( SubGrp ` H ) ) |
36 |
|
eqid |
|- ( mrCls ` ( SubGrp ` H ) ) = ( mrCls ` ( SubGrp ` H ) ) |
37 |
36
|
mrcsscl |
|- ( ( ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) /\ U. ran S C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) /\ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) e. ( SubGrp ` H ) ) -> ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) ) |
38 |
10 26 35 37
|
syl3anc |
|- ( ph -> ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) ) |
39 |
1
|
subgdmdprd |
|- ( A e. ( SubGrp ` G ) -> ( H dom DProd S <-> ( G dom DProd S /\ ran S C_ ~P A ) ) ) |
40 |
2 39
|
syl |
|- ( ph -> ( H dom DProd S <-> ( G dom DProd S /\ ran S C_ ~P A ) ) ) |
41 |
3 4 40
|
mpbir2and |
|- ( ph -> H dom DProd S ) |
42 |
|
eqidd |
|- ( ph -> dom S = dom S ) |
43 |
41 42
|
dprdf2 |
|- ( ph -> S : dom S --> ( SubGrp ` H ) ) |
44 |
43
|
frnd |
|- ( ph -> ran S C_ ( SubGrp ` H ) ) |
45 |
|
mresspw |
|- ( ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) -> ( SubGrp ` H ) C_ ~P ( Base ` H ) ) |
46 |
10 45
|
syl |
|- ( ph -> ( SubGrp ` H ) C_ ~P ( Base ` H ) ) |
47 |
44 46
|
sstrd |
|- ( ph -> ran S C_ ~P ( Base ` H ) ) |
48 |
|
sspwuni |
|- ( ran S C_ ~P ( Base ` H ) <-> U. ran S C_ ( Base ` H ) ) |
49 |
47 48
|
sylib |
|- ( ph -> U. ran S C_ ( Base ` H ) ) |
50 |
10 36 49
|
mrcssidd |
|- ( ph -> U. ran S C_ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) ) |
51 |
36
|
mrccl |
|- ( ( ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) /\ U. ran S C_ ( Base ` H ) ) -> ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) e. ( SubGrp ` H ) ) |
52 |
10 49 51
|
syl2anc |
|- ( ph -> ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) e. ( SubGrp ` H ) ) |
53 |
1
|
subsubg |
|- ( A e. ( SubGrp ` G ) -> ( ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) e. ( SubGrp ` H ) <-> ( ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) e. ( SubGrp ` G ) /\ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) C_ A ) ) ) |
54 |
2 53
|
syl |
|- ( ph -> ( ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) e. ( SubGrp ` H ) <-> ( ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) e. ( SubGrp ` G ) /\ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) C_ A ) ) ) |
55 |
52 54
|
mpbid |
|- ( ph -> ( ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) e. ( SubGrp ` G ) /\ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) C_ A ) ) |
56 |
55
|
simpld |
|- ( ph -> ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) e. ( SubGrp ` G ) ) |
57 |
17
|
mrcsscl |
|- ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ran S C_ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) /\ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) e. ( SubGrp ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) C_ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) ) |
58 |
16 50 56 57
|
syl3anc |
|- ( ph -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) C_ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) ) |
59 |
38 58
|
eqssd |
|- ( ph -> ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) ) |
60 |
36
|
dprdspan |
|- ( H dom DProd S -> ( H DProd S ) = ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) ) |
61 |
41 60
|
syl |
|- ( ph -> ( H DProd S ) = ( ( mrCls ` ( SubGrp ` H ) ) ` U. ran S ) ) |
62 |
17
|
dprdspan |
|- ( G dom DProd S -> ( G DProd S ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) ) |
63 |
3 62
|
syl |
|- ( ph -> ( G DProd S ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) ) |
64 |
59 61 63
|
3eqtr4d |
|- ( ph -> ( H DProd S ) = ( G DProd S ) ) |