This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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