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