Metamath Proof Explorer

Theorem dmdprdd

Description: Show that a given family is a direct product decomposition. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

Ref Expression
Hypotheses dmdprd.z 
|- Z = ( Cntz ` G )
dmdprd.0 
|- .0. = ( 0g ` G )
dmdprd.k 
|- K = ( mrCls ` ( SubGrp ` G ) )
dmdprdd.1 
|- ( ph -> G e. Grp )
dmdprdd.2 
|- ( ph -> I e. V )
dmdprdd.3 
|- ( ph -> S : I --> ( SubGrp ` G ) )
dmdprdd.4 
|- ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> ( S ` x ) C_ ( Z ` ( S ` y ) ) )
dmdprdd.5 
|- ( ( ph /\ x e. I ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) C_ { .0. } )
Assertion dmdprdd 
|- ( ph -> G dom DProd S )

Proof

Step Hyp Ref Expression
1 dmdprd.z 
 |-  Z = ( Cntz ` G )
2 dmdprd.0 
 |-  .0. = ( 0g ` G )
3 dmdprd.k 
 |-  K = ( mrCls ` ( SubGrp ` G ) )
4 dmdprdd.1 
 |-  ( ph -> G e. Grp )
5 dmdprdd.2 
 |-  ( ph -> I e. V )
6 dmdprdd.3 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
7 dmdprdd.4 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> ( S ` x ) C_ ( Z ` ( S ` y ) ) )
8 dmdprdd.5 
 |-  ( ( ph /\ x e. I ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) C_ { .0. } )
9 eldifsn 
 |-  ( y e. ( I \ { x } ) <-> ( y e. I /\ y =/= x ) )
10 necom 
 |-  ( y =/= x <-> x =/= y )
11 10 anbi2i 
 |-  ( ( y e. I /\ y =/= x ) <-> ( y e. I /\ x =/= y ) )
12 9 11 bitri 
 |-  ( y e. ( I \ { x } ) <-> ( y e. I /\ x =/= y ) )
13 7 3exp2 
 |-  ( ph -> ( x e. I -> ( y e. I -> ( x =/= y -> ( S ` x ) C_ ( Z ` ( S ` y ) ) ) ) ) )
14 13 imp4b 
 |-  ( ( ph /\ x e. I ) -> ( ( y e. I /\ x =/= y ) -> ( S ` x ) C_ ( Z ` ( S ` y ) ) ) )
15 12 14 syl5bi 
 |-  ( ( ph /\ x e. I ) -> ( y e. ( I \ { x } ) -> ( S ` x ) C_ ( Z ` ( S ` y ) ) ) )
16 15 ralrimiv 
 |-  ( ( ph /\ x e. I ) -> A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) )
17 6 ffvelrnda 
 |-  ( ( ph /\ x e. I ) -> ( S ` x ) e. ( SubGrp ` G ) )
18 2 subg0cl 
 |-  ( ( S ` x ) e. ( SubGrp ` G ) -> .0. e. ( S ` x ) )
19 17 18 syl 
 |-  ( ( ph /\ x e. I ) -> .0. e. ( S ` x ) )
20 4 adantr 
 |-  ( ( ph /\ x e. I ) -> G e. Grp )
21 eqid 
 |-  ( Base ` G ) = ( Base ` G )
22 21 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
23 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
24 20 22 23 3syl 
 |-  ( ( ph /\ x e. I ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
25 imassrn 
 |-  ( S " ( I \ { x } ) ) C_ ran S
26 6 frnd 
 |-  ( ph -> ran S C_ ( SubGrp ` G ) )
27 26 adantr 
 |-  ( ( ph /\ x e. I ) -> ran S C_ ( SubGrp ` G ) )
28 25 27 sstrid 
 |-  ( ( ph /\ x e. I ) -> ( S " ( I \ { x } ) ) C_ ( SubGrp ` G ) )
29 mresspw 
 |-  ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
30 24 29 syl 
 |-  ( ( ph /\ x e. I ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
31 28 30 sstrd 
 |-  ( ( ph /\ x e. I ) -> ( S " ( I \ { x } ) ) C_ ~P ( Base ` G ) )
32 sspwuni 
 |-  ( ( S " ( I \ { x } ) ) C_ ~P ( Base ` G ) <-> U. ( S " ( I \ { x } ) ) C_ ( Base ` G ) )
33 31 32 sylib 
 |-  ( ( ph /\ x e. I ) -> U. ( S " ( I \ { x } ) ) C_ ( Base ` G ) )
34 3 mrccl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ( S " ( I \ { x } ) ) C_ ( Base ` G ) ) -> ( K ` U. ( S " ( I \ { x } ) ) ) e. ( SubGrp ` G ) )
35 24 33 34 syl2anc 
 |-  ( ( ph /\ x e. I ) -> ( K ` U. ( S " ( I \ { x } ) ) ) e. ( SubGrp ` G ) )
36 2 subg0cl 
 |-  ( ( K ` U. ( S " ( I \ { x } ) ) ) e. ( SubGrp ` G ) -> .0. e. ( K ` U. ( S " ( I \ { x } ) ) ) )
37 35 36 syl 
 |-  ( ( ph /\ x e. I ) -> .0. e. ( K ` U. ( S " ( I \ { x } ) ) ) )
38 19 37 elind 
 |-  ( ( ph /\ x e. I ) -> .0. e. ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) )
39 38 snssd 
 |-  ( ( ph /\ x e. I ) -> { .0. } C_ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) )
40 8 39 eqssd 
 |-  ( ( ph /\ x e. I ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } )
41 16 40 jca 
 |-  ( ( ph /\ x e. I ) -> ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) )
42 41 ralrimiva 
 |-  ( ph -> A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) )
43 6 fdmd 
 |-  ( ph -> dom S = I )
44 1 2 3 dmdprd 
 |-  ( ( I e. V /\ dom S = I ) -> ( G dom DProd S <-> ( G e. Grp /\ S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )
45 5 43 44 syl2anc 
 |-  ( ph -> ( G dom DProd S <-> ( G e. Grp /\ S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )
46 4 6 42 45 mpbir3and 
 |-  ( ph -> G dom DProd S )