dprdub

Description: Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016)

Step	Hyp	Ref	Expression
1		dprdub.1	$⊢ φ \to G dom DProd S$
2		dprdub.2	$⊢ φ \to dom S = I$
3		dprdub.3	$⊢ φ \to X \in I$
4		eqid	$⊢ 0_{G} = 0_{G}$
5		eqid	$⊢ \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\}$
6	1	adantr	$⊢ (φ \land x \in S (X)) \to G dom DProd S$
7	2	adantr	$⊢ (φ \land x \in S (X)) \to dom S = I$
8	3	adantr	$⊢ (φ \land x \in S (X)) \to X \in I$
9		simpr	$⊢ (φ \land x \in S (X)) \to x \in S (X)$
10		eqid	$⊢ (n \in I ⟼ if (n = X, x, 0_{G})) = (n \in I ⟼ if (n = X, x, 0_{G}))$
11	4 5 6 7 8 9 10	dprdfid	$⊢ (φ \land x \in S (X)) \to ((n \in I ⟼ if (n = X, x, 0_{G})) \in \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \land \underset{n \in I}{\sum_{G}} if (n = X, x, 0_{G}) = x)$
12	11	simprd	$⊢ (φ \land x \in S (X)) \to \underset{n \in I}{\sum_{G}} if (n = X, x, 0_{G}) = x$
13	11	simpld	$⊢ (φ \land x \in S (X)) \to (n \in I ⟼ if (n = X, x, 0_{G})) \in \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\}$
14	4 5 6 7 13	eldprdi	$⊢ (φ \land x \in S (X)) \to \underset{n \in I}{\sum_{G}} if (n = X, x, 0_{G}) \in (G DProd S)$
15	12 14	eqeltrrd	$⊢ (φ \land x \in S (X)) \to x \in (G DProd S)$
16	15	ex	$⊢ φ \to (x \in S (X) \to x \in (G DProd S))$
17	16	ssrdv	$⊢ φ \to S (X) \subseteq G DProd S$

Metamath Proof Explorer