Metamath Proof Explorer

Theorem dprdpr

Description: A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 26-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 ) )
dprdpr.s 
|- .(+) = ( LSSum ` G )
dprdpr.1 
|- ( ph -> S C_ ( Z ` T ) )
dprdpr.2 
|- ( ph -> ( S i^i T ) = { .0. } )
Assertion dprdpr 
|- ( ph -> ( G DProd { <. (/) , S >. , <. 1o , T >. } ) = ( S .(+) T ) )

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 dprdpr.s 
 |-  .(+) = ( LSSum ` G )
6 dprdpr.1 
 |-  ( ph -> S C_ ( Z ` T ) )
7 dprdpr.2 
 |-  ( ph -> ( S i^i T ) = { .0. } )
8 xpscf 
 |-  ( { <. (/) , S >. , <. 1o , T >. } : 2o --> ( SubGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) )
9 3 4 8 sylanbrc 
 |-  ( ph -> { <. (/) , S >. , <. 1o , T >. } : 2o --> ( SubGrp ` G ) )
10 1n0 
 |-  1o =/= (/)
11 10 necomi 
 |-  (/) =/= 1o
12 disjsn2 
 |-  ( (/) =/= 1o -> ( { (/) } i^i { 1o } ) = (/) )
13 11 12 mp1i 
 |-  ( ph -> ( { (/) } i^i { 1o } ) = (/) )
14 df2o3 
 |-  2o = { (/) , 1o }
15 df-pr 
 |-  { (/) , 1o } = ( { (/) } u. { 1o } )
16 14 15 eqtri 
 |-  2o = ( { (/) } u. { 1o } )
17 16 a1i 
 |-  ( ph -> 2o = ( { (/) } u. { 1o } ) )
18 1 2 3 4 dmdprdpr 
 |-  ( ph -> ( G dom DProd { <. (/) , S >. , <. 1o , T >. } <-> ( S C_ ( Z ` T ) /\ ( S i^i T ) = { .0. } ) ) )
19 6 7 18 mpbir2and 
 |-  ( ph -> G dom DProd { <. (/) , S >. , <. 1o , T >. } )
20 9 13 17 5 19 dprdsplit 
 |-  ( ph -> ( G DProd { <. (/) , S >. , <. 1o , T >. } ) = ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) .(+) ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) )
21 9 ffnd 
 |-  ( ph -> { <. (/) , S >. , <. 1o , T >. } Fn 2o )
22 0ex 
 |-  (/) e. _V
23 22 prid1 
 |-  (/) e. { (/) , 1o }
24 23 14 eleqtrri 
 |-  (/) e. 2o
25 fnressn 
 |-  ( ( { <. (/) , S >. , <. 1o , T >. } Fn 2o /\ (/) e. 2o ) -> ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) = { <. (/) , ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) >. } )
26 21 24 25 sylancl 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) = { <. (/) , ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) >. } )
27 fvpr0o 
 |-  ( S e. ( SubGrp ` G ) -> ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) = S )
28 3 27 syl 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) = S )
29 28 opeq2d 
 |-  ( ph -> <. (/) , ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) >. = <. (/) , S >. )
30 29 sneqd 
 |-  ( ph -> { <. (/) , ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) >. } = { <. (/) , S >. } )
31 26 30 eqtrd 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) = { <. (/) , S >. } )
32 31 oveq2d 
 |-  ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) = ( G DProd { <. (/) , S >. } ) )
33 dprdsn 
 |-  ( ( (/) e. _V /\ S e. ( SubGrp ` G ) ) -> ( G dom DProd { <. (/) , S >. } /\ ( G DProd { <. (/) , S >. } ) = S ) )
34 22 3 33 sylancr 
 |-  ( ph -> ( G dom DProd { <. (/) , S >. } /\ ( G DProd { <. (/) , S >. } ) = S ) )
35 34 simprd 
 |-  ( ph -> ( G DProd { <. (/) , S >. } ) = S )
36 32 35 eqtrd 
 |-  ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) = S )
37 1oelpr 
 |-  1o e. { (/) , 1o }
38 37 14 eleqtrri 
 |-  1o e. 2o
39 fnressn 
 |-  ( ( { <. (/) , S >. , <. 1o , T >. } Fn 2o /\ 1o e. 2o ) -> ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) = { <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. } )
40 21 38 39 sylancl 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) = { <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. } )
41 fvpr1o 
 |-  ( T e. ( SubGrp ` G ) -> ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) = T )
42 4 41 syl 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) = T )
43 42 opeq2d 
 |-  ( ph -> <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. = <. 1o , T >. )
44 43 sneqd 
 |-  ( ph -> { <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. } = { <. 1o , T >. } )
45 40 44 eqtrd 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) = { <. 1o , T >. } )
46 45 oveq2d 
 |-  ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) = ( G DProd { <. 1o , T >. } ) )
47 1on 
 |-  1o e. On
48 dprdsn 
 |-  ( ( 1o e. On /\ T e. ( SubGrp ` G ) ) -> ( G dom DProd { <. 1o , T >. } /\ ( G DProd { <. 1o , T >. } ) = T ) )
49 47 4 48 sylancr 
 |-  ( ph -> ( G dom DProd { <. 1o , T >. } /\ ( G DProd { <. 1o , T >. } ) = T ) )
50 49 simprd 
 |-  ( ph -> ( G DProd { <. 1o , T >. } ) = T )
51 46 50 eqtrd 
 |-  ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) = T )
52 36 51 oveq12d 
 |-  ( ph -> ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) .(+) ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = ( S .(+) T ) )
53 20 52 eqtrd 
 |-  ( ph -> ( G DProd { <. (/) , S >. , <. 1o , T >. } ) = ( S .(+) T ) )