Metamath Proof Explorer

Theorem dprdz

Description: A family consisting entirely of trivial groups is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypothesis dprd0.0 
|- .0. = ( 0g ` G )
Assertion dprdz 
|- ( ( G e. Grp /\ I e. V ) -> ( G dom DProd ( x e. I |-> { .0. } ) /\ ( G DProd ( x e. I |-> { .0. } ) ) = { .0. } ) )

Proof

Step Hyp Ref Expression
1 dprd0.0 
 |-  .0. = ( 0g ` G )
2 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
3 eqid 
 |-  ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
4 simpl 
 |-  ( ( G e. Grp /\ I e. V ) -> G e. Grp )
5 simpr 
 |-  ( ( G e. Grp /\ I e. V ) -> I e. V )
6 1 0subg 
 |-  ( G e. Grp -> { .0. } e. ( SubGrp ` G ) )
7 6 ad2antrr 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ x e. I ) -> { .0. } e. ( SubGrp ` G ) )
8 7 fmpttd 
 |-  ( ( G e. Grp /\ I e. V ) -> ( x e. I |-> { .0. } ) : I --> ( SubGrp ` G ) )
9 eqid 
 |-  ( Base ` G ) = ( Base ` G )
10 9 1 grpidcl 
 |-  ( G e. Grp -> .0. e. ( Base ` G ) )
11 10 adantr 
 |-  ( ( G e. Grp /\ I e. V ) -> .0. e. ( Base ` G ) )
12 11 snssd 
 |-  ( ( G e. Grp /\ I e. V ) -> { .0. } C_ ( Base ` G ) )
13 9 2 cntzsubg 
 |-  ( ( G e. Grp /\ { .0. } C_ ( Base ` G ) ) -> ( ( Cntz ` G ) ` { .0. } ) e. ( SubGrp ` G ) )
14 12 13 syldan 
 |-  ( ( G e. Grp /\ I e. V ) -> ( ( Cntz ` G ) ` { .0. } ) e. ( SubGrp ` G ) )
15 1 subg0cl 
 |-  ( ( ( Cntz ` G ) ` { .0. } ) e. ( SubGrp ` G ) -> .0. e. ( ( Cntz ` G ) ` { .0. } ) )
16 14 15 syl 
 |-  ( ( G e. Grp /\ I e. V ) -> .0. e. ( ( Cntz ` G ) ` { .0. } ) )
17 16 snssd 
 |-  ( ( G e. Grp /\ I e. V ) -> { .0. } C_ ( ( Cntz ` G ) ` { .0. } ) )
18 17 adantr 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ ( y e. I /\ z e. I /\ y =/= z ) ) -> { .0. } C_ ( ( Cntz ` G ) ` { .0. } ) )
19 simpr1 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ ( y e. I /\ z e. I /\ y =/= z ) ) -> y e. I )
20 eqidd 
 |-  ( x = y -> { .0. } = { .0. } )
21 eqid 
 |-  ( x e. I |-> { .0. } ) = ( x e. I |-> { .0. } )
22 snex 
 |-  { .0. } e. _V
23 20 21 22 fvmpt3i 
 |-  ( y e. I -> ( ( x e. I |-> { .0. } ) ` y ) = { .0. } )
24 19 23 syl 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ ( y e. I /\ z e. I /\ y =/= z ) ) -> ( ( x e. I |-> { .0. } ) ` y ) = { .0. } )
25 simpr2 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ ( y e. I /\ z e. I /\ y =/= z ) ) -> z e. I )
26 eqidd 
 |-  ( x = z -> { .0. } = { .0. } )
27 26 21 22 fvmpt3i 
 |-  ( z e. I -> ( ( x e. I |-> { .0. } ) ` z ) = { .0. } )
28 25 27 syl 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ ( y e. I /\ z e. I /\ y =/= z ) ) -> ( ( x e. I |-> { .0. } ) ` z ) = { .0. } )
29 28 fveq2d 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ ( y e. I /\ z e. I /\ y =/= z ) ) -> ( ( Cntz ` G ) ` ( ( x e. I |-> { .0. } ) ` z ) ) = ( ( Cntz ` G ) ` { .0. } ) )
30 18 24 29 3sstr4d 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ ( y e. I /\ z e. I /\ y =/= z ) ) -> ( ( x e. I |-> { .0. } ) ` y ) C_ ( ( Cntz ` G ) ` ( ( x e. I |-> { .0. } ) ` z ) ) )
31 23 adantl 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ( ( x e. I |-> { .0. } ) ` y ) = { .0. } )
32 31 ineq1d 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ( ( ( x e. I |-> { .0. } ) ` y ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) ) = ( { .0. } i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) ) )
33 9 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
34 33 ad2antrr 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
35 34 acsmred 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
36 imassrn 
 |-  ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) C_ ran ( x e. I |-> { .0. } )
37 8 adantr 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ( x e. I |-> { .0. } ) : I --> ( SubGrp ` G ) )
38 37 frnd 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ran ( x e. I |-> { .0. } ) C_ ( SubGrp ` G ) )
39 mresspw 
 |-  ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
40 35 39 syl 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
41 38 40 sstrd 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ran ( x e. I |-> { .0. } ) C_ ~P ( Base ` G ) )
42 36 41 sstrid 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) C_ ~P ( Base ` G ) )
43 sspwuni 
 |-  ( ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) C_ ~P ( Base ` G ) <-> U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) C_ ( Base ` G ) )
44 42 43 sylib 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) C_ ( Base ` G ) )
45 3 mrccl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) C_ ( Base ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) e. ( SubGrp ` G ) )
46 35 44 45 syl2anc 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) e. ( SubGrp ` G ) )
47 1 subg0cl 
 |-  ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) e. ( SubGrp ` G ) -> .0. e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) )
48 46 47 syl 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> .0. e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) )
49 48 snssd 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> { .0. } C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) )
50 dfss2 
 |-  ( { .0. } C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) <-> ( { .0. } i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) ) = { .0. } )
51 49 50 sylib 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ( { .0. } i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) ) = { .0. } )
52 32 51 eqtrd 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ( ( ( x e. I |-> { .0. } ) ` y ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) ) = { .0. } )
53 eqimss 
 |-  ( ( ( ( x e. I |-> { .0. } ) ` y ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) ) = { .0. } -> ( ( ( x e. I |-> { .0. } ) ` y ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) ) C_ { .0. } )
54 52 53 syl 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ( ( ( x e. I |-> { .0. } ) ` y ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( x e. I |-> { .0. } ) " ( I \ { y } ) ) ) ) C_ { .0. } )
55 2 1 3 4 5 8 30 54 dmdprdd 
 |-  ( ( G e. Grp /\ I e. V ) -> G dom DProd ( x e. I |-> { .0. } ) )
56 21 7 dmmptd 
 |-  ( ( G e. Grp /\ I e. V ) -> dom ( x e. I |-> { .0. } ) = I )
57 6 adantr 
 |-  ( ( G e. Grp /\ I e. V ) -> { .0. } e. ( SubGrp ` G ) )
58 eqimss 
 |-  ( ( ( x e. I |-> { .0. } ) ` y ) = { .0. } -> ( ( x e. I |-> { .0. } ) ` y ) C_ { .0. } )
59 31 58 syl 
 |-  ( ( ( G e. Grp /\ I e. V ) /\ y e. I ) -> ( ( x e. I |-> { .0. } ) ` y ) C_ { .0. } )
60 55 56 57 59 dprdlub 
 |-  ( ( G e. Grp /\ I e. V ) -> ( G DProd ( x e. I |-> { .0. } ) ) C_ { .0. } )
61 dprdsubg 
 |-  ( G dom DProd ( x e. I |-> { .0. } ) -> ( G DProd ( x e. I |-> { .0. } ) ) e. ( SubGrp ` G ) )
62 1 subg0cl 
 |-  ( ( G DProd ( x e. I |-> { .0. } ) ) e. ( SubGrp ` G ) -> .0. e. ( G DProd ( x e. I |-> { .0. } ) ) )
63 55 61 62 3syl 
 |-  ( ( G e. Grp /\ I e. V ) -> .0. e. ( G DProd ( x e. I |-> { .0. } ) ) )
64 63 snssd 
 |-  ( ( G e. Grp /\ I e. V ) -> { .0. } C_ ( G DProd ( x e. I |-> { .0. } ) ) )
65 60 64 eqssd 
 |-  ( ( G e. Grp /\ I e. V ) -> ( G DProd ( x e. I |-> { .0. } ) ) = { .0. } )
66 55 65 jca 
 |-  ( ( G e. Grp /\ I e. V ) -> ( G dom DProd ( x e. I |-> { .0. } ) /\ ( G DProd ( x e. I |-> { .0. } ) ) = { .0. } ) )