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 1oex 
 |-  1o e. _V
38 37 prid2 
 |-  1o e. { (/) , 1o }
39 38 14 eleqtrri 
 |-  1o e. 2o
40 fnressn 
 |-  ( ( { <. (/) , S >. , <. 1o , T >. } Fn 2o /\ 1o e. 2o ) -> ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) = { <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. } )
41 21 39 40 sylancl 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) = { <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. } )
42 fvpr1o 
 |-  ( T e. ( SubGrp ` G ) -> ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) = T )
43 4 42 syl 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) = T )
44 43 opeq2d 
 |-  ( ph -> <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. = <. 1o , T >. )
45 44 sneqd 
 |-  ( ph -> { <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. } = { <. 1o , T >. } )
46 41 45 eqtrd 
 |-  ( ph -> ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) = { <. 1o , T >. } )
47 46 oveq2d 
 |-  ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) = ( G DProd { <. 1o , T >. } ) )
48 1on 
 |-  1o e. On
49 dprdsn 
 |-  ( ( 1o e. On /\ T e. ( SubGrp ` G ) ) -> ( G dom DProd { <. 1o , T >. } /\ ( G DProd { <. 1o , T >. } ) = T ) )
50 48 4 49 sylancr 
 |-  ( ph -> ( G dom DProd { <. 1o , T >. } /\ ( G DProd { <. 1o , T >. } ) = T ) )
51 50 simprd 
 |-  ( ph -> ( G DProd { <. 1o , T >. } ) = T )
52 47 51 eqtrd 
 |-  ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) = T )
53 36 52 oveq12d 
 |-  ( ph -> ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { (/) } ) ) .(+) ( G DProd ( { <. (/) , S >. , <. 1o , T >. } |` { 1o } ) ) ) = ( S .(+) T ) )
54 20 53 eqtrd 
 |-  ( ph -> ( G DProd { <. (/) , S >. , <. 1o , T >. } ) = ( S .(+) T ) )