Metamath Proof Explorer

Theorem dprdff

Description: A finitely supported function in S is a function into the base. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

		Ref	Expression
	Hypotheses	dprdff.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
		dprdff.1	$⊢ φ \to G dom DProd S$
		dprdff.2	$⊢ φ \to dom S = I$
		dprdff.3	$⊢ φ \to F \in W$
		dprdff.b	$⊢ B = {Base}_{G}$
	Assertion	dprdff	$⊢ φ \to F : I ⟶ B$

Proof

Step	Hyp	Ref	Expression
1		dprdff.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
2		dprdff.1	$⊢ φ \to G dom DProd S$
3		dprdff.2	$⊢ φ \to dom S = I$
4		dprdff.3	$⊢ φ \to F \in W$
5		dprdff.b	$⊢ B = {Base}_{G}$
6	1 2 3	dprdw	$⊢ φ \to (F \in W \leftrightarrow (F Fn I \land \forall x \in I F (x) \in S (x) \land {finSupp}_{\underset{˙}{0}} (F)))$
7	4 6	mpbid	$⊢ φ \to (F Fn I \land \forall x \in I F (x) \in S (x) \land {finSupp}_{\underset{˙}{0}} (F))$
8	7	simp1d	$⊢ φ \to F Fn I$
9	7	simp2d	$⊢ φ \to \forall x \in I F (x) \in S (x)$
10	2 3	dprdf2	$⊢ φ \to S : I ⟶ SubGrp (G)$
11	10	ffvelcdmda	$⊢ (φ \land x \in I) \to S (x) \in SubGrp (G)$
12	5	subgss	$⊢ S (x) \in SubGrp (G) \to S (x) \subseteq B$
13	11 12	syl	$⊢ (φ \land x \in I) \to S (x) \subseteq B$
14	13	sseld	$⊢ (φ \land x \in I) \to (F (x) \in S (x) \to F (x) \in B)$
15	14	ralimdva	$⊢ φ \to (\forall x \in I F (x) \in S (x) \to \forall x \in I F (x) \in B)$
16	9 15	mpd	$⊢ φ \to \forall x \in I F (x) \in B$
17		ffnfv	$⊢ F : I ⟶ B \leftrightarrow (F Fn I \land \forall x \in I F (x) \in B)$
18	8 16 17	sylanbrc	$⊢ φ \to F : I ⟶ B$