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 ) )