Metamath Proof Explorer

Theorem subgdmdprd

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

Ref Expression
Hypothesis subgdprd.1 
|- H = ( G |`s A )
Assertion subgdmdprd 
|- ( A e. ( SubGrp ` G ) -> ( H dom DProd S <-> ( G dom DProd S /\ ran S C_ ~P A ) ) )

Proof

Step Hyp Ref Expression
1 subgdprd.1 
 |-  H = ( G |`s A )
2 reldmdprd 
 |-  Rel dom DProd
3 2 brrelex2i 
 |-  ( H dom DProd S -> S e. _V )
4 3 a1i 
 |-  ( A e. ( SubGrp ` G ) -> ( H dom DProd S -> S e. _V ) )
5 2 brrelex2i 
 |-  ( G dom DProd S -> S e. _V )
6 5 adantr 
 |-  ( ( G dom DProd S /\ ran S C_ ~P A ) -> S e. _V )
7 6 a1i 
 |-  ( A e. ( SubGrp ` G ) -> ( ( G dom DProd S /\ ran S C_ ~P A ) -> S e. _V ) )
8 ffvelcdm 
 |-  ( ( S : dom S --> ( SubGrp ` H ) /\ x e. dom S ) -> ( S ` x ) e. ( SubGrp ` H ) )
9 8 ad2ant2lr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> ( S ` x ) e. ( SubGrp ` H ) )
10 eqid 
 |-  ( Base ` H ) = ( Base ` H )
11 10 subgss 
 |-  ( ( S ` x ) e. ( SubGrp ` H ) -> ( S ` x ) C_ ( Base ` H ) )
12 9 11 syl 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> ( S ` x ) C_ ( Base ` H ) )
13 1 subgbas 
 |-  ( A e. ( SubGrp ` G ) -> A = ( Base ` H ) )
14 13 ad2antrr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> A = ( Base ` H ) )
15 12 14 sseqtrrd 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> ( S ` x ) C_ A )
16 15 biantrud 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> ( ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) <-> ( ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( S ` x ) C_ A ) ) )
17 simpll 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> A e. ( SubGrp ` G ) )
18 simplr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> S : dom S --> ( SubGrp ` H ) )
19 eldifi 
 |-  ( y e. ( dom S \ { x } ) -> y e. dom S )
20 19 ad2antll 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> y e. dom S )
21 18 20 ffvelcdmd 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> ( S ` y ) e. ( SubGrp ` H ) )
22 10 subgss 
 |-  ( ( S ` y ) e. ( SubGrp ` H ) -> ( S ` y ) C_ ( Base ` H ) )
23 21 22 syl 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> ( S ` y ) C_ ( Base ` H ) )
24 23 14 sseqtrrd 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> ( S ` y ) C_ A )
25 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
26 eqid 
 |-  ( Cntz ` H ) = ( Cntz ` H )
27 1 25 26 resscntz 
 |-  ( ( A e. ( SubGrp ` G ) /\ ( S ` y ) C_ A ) -> ( ( Cntz ` H ) ` ( S ` y ) ) = ( ( ( Cntz ` G ) ` ( S ` y ) ) i^i A ) )
28 17 24 27 syl2anc 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> ( ( Cntz ` H ) ` ( S ` y ) ) = ( ( ( Cntz ` G ) ` ( S ` y ) ) i^i A ) )
29 28 sseq2d 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> ( ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) <-> ( S ` x ) C_ ( ( ( Cntz ` G ) ` ( S ` y ) ) i^i A ) ) )
30 ssin 
 |-  ( ( ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( S ` x ) C_ A ) <-> ( S ` x ) C_ ( ( ( Cntz ` G ) ` ( S ` y ) ) i^i A ) )
31 29 30 bitr4di 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> ( ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) <-> ( ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( S ` x ) C_ A ) ) )
32 16 31 bitr4d 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ ( x e. dom S /\ y e. ( dom S \ { x } ) ) ) -> ( ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) <-> ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) ) )
33 32 anassrs 
 |-  ( ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) /\ y e. ( dom S \ { x } ) ) -> ( ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) <-> ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) ) )
34 33 ralbidva 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) <-> A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) ) )
35 subgrcl 
 |-  ( A e. ( SubGrp ` G ) -> G e. Grp )
36 35 ad2antrr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> G e. Grp )
37 eqid 
 |-  ( Base ` G ) = ( Base ` G )
38 37 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
39 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
40 36 38 39 3syl 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
41 1 subggrp 
 |-  ( A e. ( SubGrp ` G ) -> H e. Grp )
42 41 ad2antrr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> H e. Grp )
43 10 subgacs 
 |-  ( H e. Grp -> ( SubGrp ` H ) e. ( ACS ` ( Base ` H ) ) )
44 acsmre 
 |-  ( ( SubGrp ` H ) e. ( ACS ` ( Base ` H ) ) -> ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) )
45 42 43 44 3syl 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) )
46 eqid 
 |-  ( mrCls ` ( SubGrp ` H ) ) = ( mrCls ` ( SubGrp ` H ) )
47 imassrn 
 |-  ( S " ( dom S \ { x } ) ) C_ ran S
48 frn 
 |-  ( S : dom S --> ( SubGrp ` H ) -> ran S C_ ( SubGrp ` H ) )
49 48 ad2antlr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ran S C_ ( SubGrp ` H ) )
50 47 49 sstrid 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( S " ( dom S \ { x } ) ) C_ ( SubGrp ` H ) )
51 mresspw 
 |-  ( ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) -> ( SubGrp ` H ) C_ ~P ( Base ` H ) )
52 45 51 syl 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( SubGrp ` H ) C_ ~P ( Base ` H ) )
53 50 52 sstrd 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( S " ( dom S \ { x } ) ) C_ ~P ( Base ` H ) )
54 sspwuni 
 |-  ( ( S " ( dom S \ { x } ) ) C_ ~P ( Base ` H ) <-> U. ( S " ( dom S \ { x } ) ) C_ ( Base ` H ) )
55 53 54 sylib 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> U. ( S " ( dom S \ { x } ) ) C_ ( Base ` H ) )
56 45 46 55 mrcssidd 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> U. ( S " ( dom S \ { x } ) ) C_ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) )
57 46 mrccl 
 |-  ( ( ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) /\ U. ( S " ( dom S \ { x } ) ) C_ ( Base ` H ) ) -> ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` H ) )
58 45 55 57 syl2anc 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` H ) )
59 1 subsubg 
 |-  ( A e. ( SubGrp ` G ) -> ( ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` H ) <-> ( ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` G ) /\ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) C_ A ) ) )
60 59 ad2antrr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` H ) <-> ( ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` G ) /\ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) C_ A ) ) )
61 58 60 mpbid 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` G ) /\ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) C_ A ) )
62 61 simpld 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` G ) )
63 eqid 
 |-  ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
64 63 mrcsscl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ( S " ( dom S \ { x } ) ) C_ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) /\ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) C_ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) )
65 40 56 62 64 syl3anc 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) C_ ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) )
66 13 ad2antrr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> A = ( Base ` H ) )
67 55 66 sseqtrrd 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> U. ( S " ( dom S \ { x } ) ) C_ A )
68 37 subgss 
 |-  ( A e. ( SubGrp ` G ) -> A C_ ( Base ` G ) )
69 68 ad2antrr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> A C_ ( Base ` G ) )
70 67 69 sstrd 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> U. ( S " ( dom S \ { x } ) ) C_ ( Base ` G ) )
71 40 63 70 mrcssidd 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> U. ( S " ( dom S \ { x } ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) )
72 63 mrccl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ( S " ( dom S \ { x } ) ) C_ ( Base ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` G ) )
73 40 70 72 syl2anc 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` G ) )
74 simpll 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> A e. ( SubGrp ` G ) )
75 63 mrcsscl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ( S " ( dom S \ { x } ) ) C_ A /\ A e. ( SubGrp ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) C_ A )
76 40 67 74 75 syl3anc 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) C_ A )
77 1 subsubg 
 |-  ( A e. ( SubGrp ` G ) -> ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` H ) <-> ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` G ) /\ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) C_ A ) ) )
78 77 ad2antrr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` H ) <-> ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` G ) /\ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) C_ A ) ) )
79 73 76 78 mpbir2and 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` H ) )
80 46 mrcsscl 
 |-  ( ( ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) /\ U. ( S " ( dom S \ { x } ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) /\ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) e. ( SubGrp ` H ) ) -> ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) )
81 45 71 79 80 syl3anc 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) )
82 65 81 eqssd 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) = ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) )
83 82 ineq2d 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) )
84 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
85 1 84 subg0 
 |-  ( A e. ( SubGrp ` G ) -> ( 0g ` G ) = ( 0g ` H ) )
86 85 ad2antrr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( 0g ` G ) = ( 0g ` H ) )
87 86 sneqd 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> { ( 0g ` G ) } = { ( 0g ` H ) } )
88 83 87 eqeq12d 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } <-> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` H ) } ) )
89 34 88 anbi12d 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) /\ x e. dom S ) -> ( ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) <-> ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` H ) } ) ) )
90 89 ralbidva 
 |-  ( ( A e. ( SubGrp ` G ) /\ S : dom S --> ( SubGrp ` H ) ) -> ( A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) <-> A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` H ) } ) ) )
91 90 pm5.32da 
 |-  ( A e. ( SubGrp ` G ) -> ( ( S : dom S --> ( SubGrp ` H ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) <-> ( S : dom S --> ( SubGrp ` H ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` H ) } ) ) ) )
92 1 subsubg 
 |-  ( A e. ( SubGrp ` G ) -> ( x e. ( SubGrp ` H ) <-> ( x e. ( SubGrp ` G ) /\ x C_ A ) ) )
93 elin 
 |-  ( x e. ( ( SubGrp ` G ) i^i ~P A ) <-> ( x e. ( SubGrp ` G ) /\ x e. ~P A ) )
94 velpw 
 |-  ( x e. ~P A <-> x C_ A )
95 94 anbi2i 
 |-  ( ( x e. ( SubGrp ` G ) /\ x e. ~P A ) <-> ( x e. ( SubGrp ` G ) /\ x C_ A ) )
96 93 95 bitri 
 |-  ( x e. ( ( SubGrp ` G ) i^i ~P A ) <-> ( x e. ( SubGrp ` G ) /\ x C_ A ) )
97 92 96 bitr4di 
 |-  ( A e. ( SubGrp ` G ) -> ( x e. ( SubGrp ` H ) <-> x e. ( ( SubGrp ` G ) i^i ~P A ) ) )
98 97 eqrdv 
 |-  ( A e. ( SubGrp ` G ) -> ( SubGrp ` H ) = ( ( SubGrp ` G ) i^i ~P A ) )
99 98 sseq2d 
 |-  ( A e. ( SubGrp ` G ) -> ( ran S C_ ( SubGrp ` H ) <-> ran S C_ ( ( SubGrp ` G ) i^i ~P A ) ) )
100 ssin 
 |-  ( ( ran S C_ ( SubGrp ` G ) /\ ran S C_ ~P A ) <-> ran S C_ ( ( SubGrp ` G ) i^i ~P A ) )
101 99 100 bitr4di 
 |-  ( A e. ( SubGrp ` G ) -> ( ran S C_ ( SubGrp ` H ) <-> ( ran S C_ ( SubGrp ` G ) /\ ran S C_ ~P A ) ) )
102 101 anbi2d 
 |-  ( A e. ( SubGrp ` G ) -> ( ( S Fn dom S /\ ran S C_ ( SubGrp ` H ) ) <-> ( S Fn dom S /\ ( ran S C_ ( SubGrp ` G ) /\ ran S C_ ~P A ) ) ) )
103 df-f 
 |-  ( S : dom S --> ( SubGrp ` H ) <-> ( S Fn dom S /\ ran S C_ ( SubGrp ` H ) ) )
104 df-f 
 |-  ( S : dom S --> ( SubGrp ` G ) <-> ( S Fn dom S /\ ran S C_ ( SubGrp ` G ) ) )
105 104 anbi1i 
 |-  ( ( S : dom S --> ( SubGrp ` G ) /\ ran S C_ ~P A ) <-> ( ( S Fn dom S /\ ran S C_ ( SubGrp ` G ) ) /\ ran S C_ ~P A ) )
106 anass 
 |-  ( ( ( S Fn dom S /\ ran S C_ ( SubGrp ` G ) ) /\ ran S C_ ~P A ) <-> ( S Fn dom S /\ ( ran S C_ ( SubGrp ` G ) /\ ran S C_ ~P A ) ) )
107 105 106 bitri 
 |-  ( ( S : dom S --> ( SubGrp ` G ) /\ ran S C_ ~P A ) <-> ( S Fn dom S /\ ( ran S C_ ( SubGrp ` G ) /\ ran S C_ ~P A ) ) )
108 102 103 107 3bitr4g 
 |-  ( A e. ( SubGrp ` G ) -> ( S : dom S --> ( SubGrp ` H ) <-> ( S : dom S --> ( SubGrp ` G ) /\ ran S C_ ~P A ) ) )
109 108 anbi1d 
 |-  ( A e. ( SubGrp ` G ) -> ( ( S : dom S --> ( SubGrp ` H ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) <-> ( ( S : dom S --> ( SubGrp ` G ) /\ ran S C_ ~P A ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) )
110 91 109 bitr3d 
 |-  ( A e. ( SubGrp ` G ) -> ( ( S : dom S --> ( SubGrp ` H ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` H ) } ) ) <-> ( ( S : dom S --> ( SubGrp ` G ) /\ ran S C_ ~P A ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) )
111 110 adantr 
 |-  ( ( A e. ( SubGrp ` G ) /\ S e. _V ) -> ( ( S : dom S --> ( SubGrp ` H ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` H ) } ) ) <-> ( ( S : dom S --> ( SubGrp ` G ) /\ ran S C_ ~P A ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) )
112 dmexg 
 |-  ( S e. _V -> dom S e. _V )
113 112 adantl 
 |-  ( ( A e. ( SubGrp ` G ) /\ S e. _V ) -> dom S e. _V )
114 eqidd 
 |-  ( ( A e. ( SubGrp ` G ) /\ S e. _V ) -> dom S = dom S )
115 41 adantr 
 |-  ( ( A e. ( SubGrp ` G ) /\ S e. _V ) -> H e. Grp )
116 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
117 26 116 46 dmdprd 
 |-  ( ( dom S e. _V /\ dom S = dom S ) -> ( H dom DProd S <-> ( H e. Grp /\ S : dom S --> ( SubGrp ` H ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` H ) } ) ) ) )
118 3anass 
 |-  ( ( H e. Grp /\ S : dom S --> ( SubGrp ` H ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` H ) } ) ) <-> ( H e. Grp /\ ( S : dom S --> ( SubGrp ` H ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` H ) } ) ) ) )
119 117 118 bitrdi 
 |-  ( ( dom S e. _V /\ dom S = dom S ) -> ( H dom DProd S <-> ( H e. Grp /\ ( S : dom S --> ( SubGrp ` H ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` H ) } ) ) ) ) )
120 119 baibd 
 |-  ( ( ( dom S e. _V /\ dom S = dom S ) /\ H e. Grp ) -> ( H dom DProd S <-> ( S : dom S --> ( SubGrp ` H ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` H ) } ) ) ) )
121 113 114 115 120 syl21anc 
 |-  ( ( A e. ( SubGrp ` G ) /\ S e. _V ) -> ( H dom DProd S <-> ( S : dom S --> ( SubGrp ` H ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` H ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` H ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` H ) } ) ) ) )
122 35 adantr 
 |-  ( ( A e. ( SubGrp ` G ) /\ S e. _V ) -> G e. Grp )
123 25 84 63 dmdprd 
 |-  ( ( dom S e. _V /\ dom S = dom S ) -> ( G dom DProd S <-> ( G e. Grp /\ S : dom S --> ( SubGrp ` G ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) )
124 3anass 
 |-  ( ( G e. Grp /\ S : dom S --> ( SubGrp ` G ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) <-> ( G e. Grp /\ ( S : dom S --> ( SubGrp ` G ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) )
125 123 124 bitrdi 
 |-  ( ( dom S e. _V /\ dom S = dom S ) -> ( G dom DProd S <-> ( G e. Grp /\ ( S : dom S --> ( SubGrp ` G ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) ) )
126 125 baibd 
 |-  ( ( ( dom S e. _V /\ dom S = dom S ) /\ G e. Grp ) -> ( G dom DProd S <-> ( S : dom S --> ( SubGrp ` G ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) )
127 113 114 122 126 syl21anc 
 |-  ( ( A e. ( SubGrp ` G ) /\ S e. _V ) -> ( G dom DProd S <-> ( S : dom S --> ( SubGrp ` G ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) )
128 127 anbi1d 
 |-  ( ( A e. ( SubGrp ` G ) /\ S e. _V ) -> ( ( G dom DProd S /\ ran S C_ ~P A ) <-> ( ( S : dom S --> ( SubGrp ` G ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) /\ ran S C_ ~P A ) ) )
129 an32 
 |-  ( ( ( S : dom S --> ( SubGrp ` G ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) /\ ran S C_ ~P A ) <-> ( ( S : dom S --> ( SubGrp ` G ) /\ ran S C_ ~P A ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) )
130 128 129 bitrdi 
 |-  ( ( A e. ( SubGrp ` G ) /\ S e. _V ) -> ( ( G dom DProd S /\ ran S C_ ~P A ) <-> ( ( S : dom S --> ( SubGrp ` G ) /\ ran S C_ ~P A ) /\ A. x e. dom S ( A. y e. ( dom S \ { x } ) ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( dom S \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) )
131 111 121 130 3bitr4d 
 |-  ( ( A e. ( SubGrp ` G ) /\ S e. _V ) -> ( H dom DProd S <-> ( G dom DProd S /\ ran S C_ ~P A ) ) )
132 131 ex 
 |-  ( A e. ( SubGrp ` G ) -> ( S e. _V -> ( H dom DProd S <-> ( G dom DProd S /\ ran S C_ ~P A ) ) ) )
133 4 7 132 pm5.21ndd 
 |-  ( A e. ( SubGrp ` G ) -> ( H dom DProd S <-> ( G dom DProd S /\ ran S C_ ~P A ) ) )