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	$$⊢\underset{\dot{}}{0}=0_G$$
	eldprdi.w	$$⊢W=\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}$$
	eldprdi.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
	eldprdi.2	$$⊢\phi \to \mathrm{dom}S=I$$
	eldprdi.3	$$⊢\phi \to F\in W$$
Assertion	eldprdi	$$⊢\phi \to {\sum }_{G}F\in \left(G\mathrm{DProd}S\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldprdi.0	$$⊢\underset{\dot{}}{0}=0_G$$
2		eldprdi.w	$$⊢W=\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}$$
3		eldprdi.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
4		eldprdi.2	$$⊢\phi \to \mathrm{dom}S=I$$
5		eldprdi.3	$$⊢\phi \to F\in W$$
6		eqid	$$⊢{\sum }_{G}F={\sum }_{G}F$$
7		oveq2	$$⊢f=F\to {\sum }_{G}f={\sum }_{G}F$$
8	7	rspceeqv	$$⊢\left(F\in W\wedge {\sum }_{G}F={\sum }_{G}F\right)\to \exists f\in W{\sum }_{G}F={\sum }_{G}f$$
9	5 6 8	sylancl	$$⊢\phi \to \exists f\in W{\sum }_{G}F={\sum }_{G}f$$
10	1 2	eldprd	$$⊢\mathrm{dom}S=I\to \left({\sum }_{G}F\in \left(G\mathrm{DProd}S\right)\leftrightarrow \left(G\mathrm{dom}\mathrm{DProd}S\wedge \exists f\in W{\sum }_{G}F={\sum }_{G}f\right)\right)$$
11	4 10	syl	$$⊢\phi \to \left({\sum }_{G}F\in \left(G\mathrm{DProd}S\right)\leftrightarrow \left(G\mathrm{dom}\mathrm{DProd}S\wedge \exists f\in W{\sum }_{G}F={\sum }_{G}f\right)\right)$$
12	3 9 11	mpbir2and	$$⊢\phi \to {\sum }_{G}F\in \left(G\mathrm{DProd}S\right)$$