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