Metamath Proof Explorer

Theorem dmdprdpr

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

Ref Expression
Hypotheses dmdprdpr.z 
|- Z = ( Cntz ` G )
dmdprdpr.0 
|- .0. = ( 0g ` G )
dmdprdpr.s 
|- ( ph -> S e. ( SubGrp ` G ) )
dmdprdpr.t 
|- ( ph -> T e. ( SubGrp ` G ) )
Assertion dmdprdpr 
|- ( ph -> ( G dom DProd { <. (/) , S >. , <. 1o , T >. } <-> ( S C_ ( Z ` T ) /\ ( S i^i T ) = { .0. } ) ) )

Proof

Step Hyp Ref Expression
1 dmdprdpr.z 
 |-  Z = ( Cntz ` G )
2 dmdprdpr.0 
 |-  .0. = ( 0g ` G )
3 dmdprdpr.s 
 |-  ( ph -> S e. ( SubGrp ` G ) )
4 dmdprdpr.t 
 |-  ( ph -> T e. ( SubGrp ` G ) )
5 0ex 
 |-  (/) e. _V
6 dprdsn 
 |-  ( ( (/) e. _V /\ S e. ( SubGrp ` G ) ) -> ( G dom DProd { <. (/) , S >. } /\ ( G DProd { <. (/) , S >. } ) = S ) )
7 5 3 6 sylancr 
 |-  ( ph -> ( G dom DProd { <. (/) , S >. } /\ ( G DProd { <. (/) , S >. } ) = S ) )
8 7 simpld 
 |-  ( ph -> G dom DProd { <. (/) , S >. } )
9 xpscf 
 |-  ( { <. (/) , S >. , <. 1o , T >. } : 2o --> ( SubGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) )
10 3 4 9 sylanbrc 
 |-  ( ph -> { <. (/) , S >. , <. 1o , T >. } : 2o --> ( SubGrp ` G ) )
11 10 ffnd 
 |-  ( ph -> { <. (/) , S >. , <. 1o , T >. } Fn 2o )
12 5 prid1 
 |-  (/) e. { (/) , 1o }
13 df2o3 
 |-  2o = { (/) , 1o }
14 12 13 eleqtrri 
 |-  (/) e. 2o
15 fnressn 
 |-  ( ( { <. (/) , S >. , <. 1o , T >. } Fn 2o /\ (/) e. 2o ) -> ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) = { <. (/) , ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) >. } )
16 11 14 15 sylancl 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) = { <. (/) , ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) >. } )
17 fvpr0o 
 |-  ( S e. ( SubGrp ` G ) -> ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) = S )
18 3 17 syl 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) = S )
19 18 opeq2d 
 |-  ( ph -> <. (/) , ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) >. = <. (/) , S >. )
20 19 sneqd 
 |-  ( ph -> { <. (/) , ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) >. } = { <. (/) , S >. } )
21 16 20 eqtrd 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) = { <. (/) , S >. } )
22 8 21 breqtrrd 
 |-  ( ph -> G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) )
23 1on 
 |-  1o e. On
24 dprdsn 
 |-  ( ( 1o e. On /\ T e. ( SubGrp ` G ) ) -> ( G dom DProd { <. 1o , T >. } /\ ( G DProd { <. 1o , T >. } ) = T ) )
25 23 4 24 sylancr 
 |-  ( ph -> ( G dom DProd { <. 1o , T >. } /\ ( G DProd { <. 1o , T >. } ) = T ) )
26 25 simpld 
 |-  ( ph -> G dom DProd { <. 1o , T >. } )
27 1oex 
 |-  1o e. _V
28 27 prid2 
 |-  1o e. { (/) , 1o }
29 28 13 eleqtrri 
 |-  1o e. 2o
30 fnressn 
 |-  ( ( { <. (/) , S >. , <. 1o , T >. } Fn 2o /\ 1o e. 2o ) -> ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) = { <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. } )
31 11 29 30 sylancl 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) = { <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. } )
32 fvpr1o 
 |-  ( T e. ( SubGrp ` G ) -> ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) = T )
33 4 32 syl 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) = T )
34 33 opeq2d 
 |-  ( ph -> <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. = <. 1o , T >. )
35 34 sneqd 
 |-  ( ph -> { <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. } = { <. 1o , T >. } )
36 31 35 eqtrd 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) = { <. 1o , T >. } )
37 26 36 breqtrrd 
 |-  ( ph -> G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) )
38 1n0 
 |-  1o =/= (/)
39 38 necomi 
 |-  (/) =/= 1o
40 disjsn2 
 |-  ( (/) =/= 1o -> ( { (/) } i^i { 1o } ) = (/) )
41 39 40 mp1i 
 |-  ( ph -> ( { (/) } i^i { 1o } ) = (/) )
42 df-pr 
 |-  { (/) , 1o } = ( { (/) } u. { 1o } )
43 13 42 eqtri 
 |-  2o = ( { (/) } u. { 1o } )
44 43 a1i 
 |-  ( ph -> 2o = ( { (/) } u. { 1o } ) )
45 10 41 44 1 2 dmdprdsplit 
 |-  ( ph -> ( G dom DProd { <. (/) , S >. , <. 1o , T >. } <-> ( ( G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) /\ G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) /\ ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) C_ ( Z ` ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) /\ ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) i^i ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = { .0. } ) ) )
46 3anass 
 |-  ( ( ( G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) /\ G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) /\ ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) C_ ( Z ` ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) /\ ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) i^i ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = { .0. } ) <-> ( ( G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) /\ G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) /\ ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) C_ ( Z ` ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) /\ ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) i^i ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = { .0. } ) ) )
47 45 46 bitrdi 
 |-  ( ph -> ( G dom DProd { <. (/) , S >. , <. 1o , T >. } <-> ( ( G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) /\ G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) /\ ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) C_ ( Z ` ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) /\ ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) i^i ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = { .0. } ) ) ) )
48 47 baibd 
 |-  ( ( ph /\ ( G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) /\ G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) -> ( G dom DProd { <. (/) , S >. , <. 1o , T >. } <-> ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) C_ ( Z ` ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) /\ ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) i^i ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = { .0. } ) ) )
49 48 ex 
 |-  ( ph -> ( ( G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) /\ G dom DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) -> ( G dom DProd { <. (/) , S >. , <. 1o , T >. } <-> ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) C_ ( Z ` ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) /\ ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) i^i ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = { .0. } ) ) ) )
50 22 37 49 mp2and 
 |-  ( ph -> ( G dom DProd { <. (/) , S >. , <. 1o , T >. } <-> ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) C_ ( Z ` ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) /\ ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) i^i ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = { .0. } ) ) )
51 21 oveq2d 
 |-  ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) = ( G DProd { <. (/) , S >. } ) )
52 7 simprd 
 |-  ( ph -> ( G DProd { <. (/) , S >. } ) = S )
53 51 52 eqtrd 
 |-  ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) = S )
54 36 oveq2d 
 |-  ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) = ( G DProd { <. 1o , T >. } ) )
55 25 simprd 
 |-  ( ph -> ( G DProd { <. 1o , T >. } ) = T )
56 54 55 eqtrd 
 |-  ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) = T )
57 56 fveq2d 
 |-  ( ph -> ( Z ` ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = ( Z ` T ) )
58 53 57 sseq12d 
 |-  ( ph -> ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) C_ ( Z ` ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) <-> S C_ ( Z ` T ) ) )
59 53 56 ineq12d 
 |-  ( ph -> ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) i^i ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = ( S i^i T ) )
60 59 eqeq1d 
 |-  ( ph -> ( ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) i^i ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = { .0. } <-> ( S i^i T ) = { .0. } ) )
61 58 60 anbi12d 
 |-  ( ph -> ( ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) C_ ( Z ` ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) /\ ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) i^i ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = { .0. } ) <-> ( S C_ ( Z ` T ) /\ ( S i^i T ) = { .0. } ) ) )
62 50 61 bitrd 
 |-  ( ph -> ( G dom DProd { <. (/) , S >. , <. 1o , T >. } <-> ( S C_ ( Z ` T ) /\ ( S i^i T ) = { .0. } ) ) )