Metamath Proof Explorer

Theorem dprdssv

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

Ref Expression
Hypothesis dprdssv.b 
|- B = ( Base ` G )
Assertion dprdssv 
|- ( G DProd S ) C_ B

Proof

Step Hyp Ref Expression
1 dprdssv.b 
 |-  B = ( Base ` G )
2 eqid 
 |-  dom S = dom S
3 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
4 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 ) }
5 3 4 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 ) ) ) )
6 2 5 ax-mp 
 |-  ( 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 ) ) )
7 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
8 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
9 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
10 8 9 syl 
 |-  ( G dom DProd S -> G e. Mnd )
11 10 adantr 
 |-  ( ( G dom DProd S /\ f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) -> G e. Mnd )
12 reldmdprd 
 |-  Rel dom DProd
13 12 brrelex2i 
 |-  ( G dom DProd S -> S e. _V )
14 13 dmexd 
 |-  ( G dom DProd S -> dom S e. _V )
15 14 adantr 
 |-  ( ( G dom DProd S /\ f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) -> dom S e. _V )
16 simpl 
 |-  ( ( G dom DProd S /\ f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) -> G dom DProd S )
17 eqidd 
 |-  ( ( G dom DProd S /\ f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) -> dom S = dom S )
18 simpr 
 |-  ( ( G dom DProd S /\ f 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 ) } )
19 4 16 17 18 1 dprdff 
 |-  ( ( G dom DProd S /\ f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) -> f : dom S --> B )
20 4 16 17 18 7 dprdfcntz 
 |-  ( ( G dom DProd S /\ f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) -> ran f C_ ( ( Cntz ` G ) ` ran f ) )
21 4 16 17 18 dprdffsupp 
 |-  ( ( G dom DProd S /\ f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) -> f finSupp ( 0g ` G ) )
22 1 3 7 11 15 19 20 21 gsumzcl 
 |-  ( ( G dom DProd S /\ f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) -> ( G gsum f ) e. B )
23 eleq1 
 |-  ( x = ( G gsum f ) -> ( x e. B <-> ( G gsum f ) e. B ) )
24 22 23 syl5ibrcom 
 |-  ( ( G dom DProd S /\ f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } ) -> ( x = ( G gsum f ) -> x e. B ) )
25 24 rexlimdva 
 |-  ( G dom DProd S -> ( E. f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } x = ( G gsum f ) -> x e. B ) )
26 25 imp 
 |-  ( ( G dom DProd S /\ E. f e. { h e. X_ i e. dom S ( S ` i ) | h finSupp ( 0g ` G ) } x = ( G gsum f ) ) -> x e. B )
27 6 26 sylbi 
 |-  ( x e. ( G DProd S ) -> x e. B )
28 27 ssriv 
 |-  ( G DProd S ) C_ B