This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eldprdi

Description: The domain of definition of the internal direct product, which states that S is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses eldprdi.0 
|- .0. = ( 0g ` G )
eldprdi.w 
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
eldprdi.1 
|- ( ph -> G dom DProd S )
eldprdi.2 
|- ( ph -> dom S = I )
eldprdi.3 
|- ( ph -> F e. W )
Assertion eldprdi 
|- ( ph -> ( G gsum F ) e. ( G DProd S ) )

Proof

Step Hyp Ref Expression
1 eldprdi.0 
 |-  .0. = ( 0g ` G )
2 eldprdi.w 
 |-  W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
3 eldprdi.1 
 |-  ( ph -> G dom DProd S )
4 eldprdi.2 
 |-  ( ph -> dom S = I )
5 eldprdi.3 
 |-  ( ph -> F e. W )
6 eqid 
 |-  ( G gsum F ) = ( G gsum F )
7 oveq2 
 |-  ( f = F -> ( G gsum f ) = ( G gsum F ) )
8 7 rspceeqv 
 |-  ( ( F e. W /\ ( G gsum F ) = ( G gsum F ) ) -> E. f e. W ( G gsum F ) = ( G gsum f ) )
9 5 6 8 sylancl 
 |-  ( ph -> E. f e. W ( G gsum F ) = ( G gsum f ) )
10 1 2 eldprd 
 |-  ( dom S = I -> ( ( G gsum F ) e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. W ( G gsum F ) = ( G gsum f ) ) ) )
11 4 10 syl 
 |-  ( ph -> ( ( G gsum F ) e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. W ( G gsum F ) = ( G gsum f ) ) ) )
12 3 9 11 mpbir2and 
 |-  ( ph -> ( G gsum F ) e. ( G DProd S ) )