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 e. X_ i e. I ( S ` i ) | h finSupp .0. }
	dprdff.1	|- ( ph -> G dom DProd S )
	dprdff.2	|- ( ph -> dom S = I )
	dprdff.3	|- ( ph -> F e. W )
	dprdff.b	|- B = ( Base ` G )
Assertion	dprdff	|- ( ph -> F : I --> B )

Proof

Step	Hyp	Ref	Expression
1		dprdff.w	|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
2		dprdff.1	|- ( ph -> G dom DProd S )
3		dprdff.2	|- ( ph -> dom S = I )
4		dprdff.3	|- ( ph -> F e. W )
5		dprdff.b	|- B = ( Base ` G )
6	1 2 3	dprdw	|- ( ph -> ( F e. W <-> ( F Fn I /\ A. x e. I ( F ` x ) e. ( S ` x ) /\ F finSupp .0. ) ) )
7	4 6	mpbid	|- ( ph -> ( F Fn I /\ A. x e. I ( F ` x ) e. ( S ` x ) /\ F finSupp .0. ) )
8	7	simp1d	|- ( ph -> F Fn I )
9	7	simp2d	|- ( ph -> A. x e. I ( F ` x ) e. ( S ` x ) )
10	2 3	dprdf2	|- ( ph -> S : I --> ( SubGrp ` G ) )
11	10	ffvelrnda	|- ( ( ph /\ x e. I ) -> ( S ` x ) e. ( SubGrp ` G ) )
12	5	subgss	|- ( ( S ` x ) e. ( SubGrp ` G ) -> ( S ` x ) C_ B )
13	11 12	syl	|- ( ( ph /\ x e. I ) -> ( S ` x ) C_ B )
14	13	sseld	|- ( ( ph /\ x e. I ) -> ( ( F ` x ) e. ( S ` x ) -> ( F ` x ) e. B ) )
15	14	ralimdva	|- ( ph -> ( A. x e. I ( F ` x ) e. ( S ` x ) -> A. x e. I ( F ` x ) e. B ) )
16	9 15	mpd	|- ( ph -> A. x e. I ( F ` x ) e. B )
17		ffnfv	|- ( F : I --> B <-> ( F Fn I /\ A. x e. I ( F ` x ) e. B ) )
18	8 16 17	sylanbrc	|- ( ph -> F : I --> B )