Metamath Proof Explorer

Theorem dprdsubg

Description: The internal direct product of a family of subgroups is a subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Assertion dprdsubg 
|- ( G dom DProd S -> ( G DProd S ) e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( Base ` G )
2 1 dprdssv 
 |-  ( G DProd S ) C_ ( Base ` G )
3 2 a1i 
 |-  ( G dom DProd S -> ( G DProd S ) C_ ( Base ` G ) )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 eqid 
 |-  { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } = { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) }
6 id 
 |-  ( G dom DProd S -> G dom DProd S )
7 eqidd 
 |-  ( G dom DProd S -> dom S = dom S )
8 fvex 
 |-  ( 0g ` G ) e. _V
9 fnconstg 
 |-  ( ( 0g ` G ) e. _V -> ( dom S X. { ( 0g ` G ) } ) Fn dom S )
10 8 9 mp1i 
 |-  ( G dom DProd S -> ( dom S X. { ( 0g ` G ) } ) Fn dom S )
11 8 fvconst2 
 |-  ( k e. dom S -> ( ( dom S X. { ( 0g ` G ) } ) ` k ) = ( 0g ` G ) )
12 11 adantl 
 |-  ( ( G dom DProd S /\ k e. dom S ) -> ( ( dom S X. { ( 0g ` G ) } ) ` k ) = ( 0g ` G ) )
13 dprdf 
 |-  ( G dom DProd S -> S : dom S --> ( SubGrp ` G ) )
14 13 ffvelrnda 
 |-  ( ( G dom DProd S /\ k e. dom S ) -> ( S ` k ) e. ( SubGrp ` G ) )
15 4 subg0cl 
 |-  ( ( S ` k ) e. ( SubGrp ` G ) -> ( 0g ` G ) e. ( S ` k ) )
16 14 15 syl 
 |-  ( ( G dom DProd S /\ k e. dom S ) -> ( 0g ` G ) e. ( S ` k ) )
17 12 16 eqeltrd 
 |-  ( ( G dom DProd S /\ k e. dom S ) -> ( ( dom S X. { ( 0g ` G ) } ) ` k ) e. ( S ` k ) )
18 17 ralrimiva 
 |-  ( G dom DProd S -> A. k e. dom S ( ( dom S X. { ( 0g ` G ) } ) ` k ) e. ( S ` k ) )
19 df-nel 
 |-  ( dom S e/ _V <-> -. dom S e. _V )
20 dprddomprc 
 |-  ( dom S e/ _V -> -. G dom DProd S )
21 19 20 sylbir 
 |-  ( -. dom S e. _V -> -. G dom DProd S )
22 21 con4i 
 |-  ( G dom DProd S -> dom S e. _V )
23 8 a1i 
 |-  ( G dom DProd S -> ( 0g ` G ) e. _V )
24 22 23 fczfsuppd 
 |-  ( G dom DProd S -> ( dom S X. { ( 0g ` G ) } ) finSupp ( 0g ` G ) )
25 5 6 7 dprdw 
 |-  ( G dom DProd S -> ( ( dom S X. { ( 0g ` G ) } ) e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } <-> ( ( dom S X. { ( 0g ` G ) } ) Fn dom S /\ A. k e. dom S ( ( dom S X. { ( 0g ` G ) } ) ` k ) e. ( S ` k ) /\ ( dom S X. { ( 0g ` G ) } ) finSupp ( 0g ` G ) ) ) )
26 10 18 24 25 mpbir3and 
 |-  ( G dom DProd S -> ( dom S X. { ( 0g ` G ) } ) e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } )
27 4 5 6 7 26 eldprdi 
 |-  ( G dom DProd S -> ( G gsum ( dom S X. { ( 0g ` G ) } ) ) e. ( G DProd S ) )
28 27 ne0d 
 |-  ( G dom DProd S -> ( G DProd S ) =/= (/) )
29 eqid 
 |-  dom S = dom S
30 4 5 eldprd 
 |-  ( dom S = dom S -> ( x e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } x = ( G gsum f ) ) ) )
31 30 baibd 
 |-  ( ( dom S = dom S /\ G dom DProd S ) -> ( x e. ( G DProd S ) <-> E. f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } x = ( G gsum f ) ) )
32 4 5 eldprd 
 |-  ( dom S = dom S -> ( y e. ( G DProd S ) <-> ( G dom DProd S /\ E. g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } y = ( G gsum g ) ) ) )
33 32 baibd 
 |-  ( ( dom S = dom S /\ G dom DProd S ) -> ( y e. ( G DProd S ) <-> E. g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } y = ( G gsum g ) ) )
34 31 33 anbi12d 
 |-  ( ( dom S = dom S /\ G dom DProd S ) -> ( ( x e. ( G DProd S ) /\ y e. ( G DProd S ) ) <-> ( E. f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } x = ( G gsum f ) /\ E. g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } y = ( G gsum g ) ) ) )
35 29 34 mpan 
 |-  ( G dom DProd S -> ( ( x e. ( G DProd S ) /\ y e. ( G DProd S ) ) <-> ( E. f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } x = ( G gsum f ) /\ E. g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } y = ( G gsum g ) ) ) )
36 reeanv 
 |-  ( E. f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } E. g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ( x = ( G gsum f ) /\ y = ( G gsum g ) ) <-> ( E. f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } x = ( G gsum f ) /\ E. g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } y = ( G gsum g ) ) )
37 simpl 
 |-  ( ( G dom DProd S /\ ( f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } /\ g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) ) -> G dom DProd S )
38 eqidd 
 |-  ( ( G dom DProd S /\ ( f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } /\ g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) ) -> dom S = dom S )
39 simprl 
 |-  ( ( G dom DProd S /\ ( f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } /\ g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) ) -> f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } )
40 simprr 
 |-  ( ( G dom DProd S /\ ( f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } /\ g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) ) -> g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } )
41 eqid 
 |-  ( -g ` G ) = ( -g ` G )
42 4 5 37 38 39 40 41 dprdfsub 
 |-  ( ( G dom DProd S /\ ( f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } /\ g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) ) -> ( ( f oF ( -g ` G ) g ) e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } /\ ( G gsum ( f oF ( -g ` G ) g ) ) = ( ( G gsum f ) ( -g ` G ) ( G gsum g ) ) ) )
43 42 simprd 
 |-  ( ( G dom DProd S /\ ( f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } /\ g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) ) -> ( G gsum ( f oF ( -g ` G ) g ) ) = ( ( G gsum f ) ( -g ` G ) ( G gsum g ) ) )
44 42 simpld 
 |-  ( ( G dom DProd S /\ ( f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } /\ g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) ) -> ( f oF ( -g ` G ) g ) e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } )
45 4 5 37 38 44 eldprdi 
 |-  ( ( G dom DProd S /\ ( f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } /\ g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) ) -> ( G gsum ( f oF ( -g ` G ) g ) ) e. ( G DProd S ) )
46 43 45 eqeltrrd 
 |-  ( ( G dom DProd S /\ ( f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } /\ g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) ) -> ( ( G gsum f ) ( -g ` G ) ( G gsum g ) ) e. ( G DProd S ) )
47 oveq12 
 |-  ( ( x = ( G gsum f ) /\ y = ( G gsum g ) ) -> ( x ( -g ` G ) y ) = ( ( G gsum f ) ( -g ` G ) ( G gsum g ) ) )
48 47 eleq1d 
 |-  ( ( x = ( G gsum f ) /\ y = ( G gsum g ) ) -> ( ( x ( -g ` G ) y ) e. ( G DProd S ) <-> ( ( G gsum f ) ( -g ` G ) ( G gsum g ) ) e. ( G DProd S ) ) )
49 46 48 syl5ibrcom 
 |-  ( ( G dom DProd S /\ ( f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } /\ g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) ) -> ( ( x = ( G gsum f ) /\ y = ( G gsum g ) ) -> ( x ( -g ` G ) y ) e. ( G DProd S ) ) )
50 49 rexlimdvva 
 |-  ( G dom DProd S -> ( E. f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } E. g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ( x = ( G gsum f ) /\ y = ( G gsum g ) ) -> ( x ( -g ` G ) y ) e. ( G DProd S ) ) )
51 36 50 syl5bir 
 |-  ( G dom DProd S -> ( ( E. f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } x = ( G gsum f ) /\ E. g e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } y = ( G gsum g ) ) -> ( x ( -g ` G ) y ) e. ( G DProd S ) ) )
52 35 51 sylbid 
 |-  ( G dom DProd S -> ( ( x e. ( G DProd S ) /\ y e. ( G DProd S ) ) -> ( x ( -g ` G ) y ) e. ( G DProd S ) ) )
53 52 ralrimivv 
 |-  ( G dom DProd S -> A. x e. ( G DProd S ) A. y e. ( G DProd S ) ( x ( -g ` G ) y ) e. ( G DProd S ) )
54 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
55 1 41 issubg4 
 |-  ( G e. Grp -> ( ( G DProd S ) e. ( SubGrp ` G ) <-> ( ( G DProd S ) C_ ( Base ` G ) /\ ( G DProd S ) =/= (/) /\ A. x e. ( G DProd S ) A. y e. ( G DProd S ) ( x ( -g ` G ) y ) e. ( G DProd S ) ) ) )
56 54 55 syl 
 |-  ( G dom DProd S -> ( ( G DProd S ) e. ( SubGrp ` G ) <-> ( ( G DProd S ) C_ ( Base ` G ) /\ ( G DProd S ) =/= (/) /\ A. x e. ( G DProd S ) A. y e. ( G DProd S ) ( x ( -g ` G ) y ) e. ( G DProd S ) ) ) )
57 3 28 53 56 mpbir3and 
 |-  ( G dom DProd S -> ( G DProd S ) e. ( SubGrp ` G ) )