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