Metamath Proof Explorer

Theorem subgdprd

Description: A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses subgdprd.1 
|- H = ( G |`s A )
subgdprd.2 
|- ( ph -> A e. ( SubGrp ` G ) )
subgdprd.3 
|- ( ph -> G dom DProd S )
subgdprd.4 
|- ( ph -> ran S C_ ~P A )
Assertion subgdprd 
|- ( ph -> ( H DProd S ) = ( G DProd S ) )

Proof

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