Metamath Proof Explorer

Theorem dpjf

Description: The X -th index projection is a function from the direct product to the X -th factor. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dpjfval.1 
|- ( ph -> G dom DProd S )
dpjfval.2 
|- ( ph -> dom S = I )
dpjfval.p 
|- P = ( G dProj S )
dpjf.3 
|- ( ph -> X e. I )
Assertion dpjf 
|- ( ph -> ( P ` X ) : ( G DProd S ) --> ( S ` X ) )

Proof

Step Hyp Ref Expression
1 dpjfval.1 
 |-  ( ph -> G dom DProd S )
2 dpjfval.2 
 |-  ( ph -> dom S = I )
3 dpjfval.p 
 |-  P = ( G dProj S )
4 dpjf.3 
 |-  ( ph -> X e. I )
5 eqid 
 |-  ( +g ` G ) = ( +g ` G )
6 eqid 
 |-  ( LSSum ` G ) = ( LSSum ` G )
7 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
8 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
9 1 2 dprdf2 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
10 9 4 ffvelrnd 
 |-  ( ph -> ( S ` X ) e. ( SubGrp ` G ) )
11 difssd 
 |-  ( ph -> ( I \ { X } ) C_ I )
12 1 2 11 dprdres 
 |-  ( ph -> ( G dom DProd ( S |` ( I \ { X } ) ) /\ ( G DProd ( S |` ( I \ { X } ) ) ) C_ ( G DProd S ) ) )
13 12 simpld 
 |-  ( ph -> G dom DProd ( S |` ( I \ { X } ) ) )
14 dprdsubg 
 |-  ( G dom DProd ( S |` ( I \ { X } ) ) -> ( G DProd ( S |` ( I \ { X } ) ) ) e. ( SubGrp ` G ) )
15 13 14 syl 
 |-  ( ph -> ( G DProd ( S |` ( I \ { X } ) ) ) e. ( SubGrp ` G ) )
16 1 2 4 7 dpjdisj 
 |-  ( ph -> ( ( S ` X ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) = { ( 0g ` G ) } )
17 1 2 4 8 dpjcntz 
 |-  ( ph -> ( S ` X ) C_ ( ( Cntz ` G ) ` ( G DProd ( S |` ( I \ { X } ) ) ) ) )
18 eqid 
 |-  ( proj1 ` G ) = ( proj1 ` G )
19 5 6 7 8 10 15 16 17 18 pj1f 
 |-  ( ph -> ( ( S ` X ) ( proj1 ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) : ( ( S ` X ) ( LSSum ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) --> ( S ` X ) )
20 1 2 3 18 4 dpjval 
 |-  ( ph -> ( P ` X ) = ( ( S ` X ) ( proj1 ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) )
21 1 2 4 6 dpjlsm 
 |-  ( ph -> ( G DProd S ) = ( ( S ` X ) ( LSSum ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) )
22 20 21 feq12d 
 |-  ( ph -> ( ( P ` X ) : ( G DProd S ) --> ( S ` X ) <-> ( ( S ` X ) ( proj1 ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) : ( ( S ` X ) ( LSSum ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) --> ( S ` X ) ) )
23 19 22 mpbird 
 |-  ( ph -> ( P ` X ) : ( G DProd S ) --> ( S ` X ) )