Metamath Proof Explorer

Theorem dpjlid

Description: The X -th index projection acts as the identity on elements of 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 )
dpjlid.3 
|- ( ph -> X e. I )
dpjlid.4 
|- ( ph -> A e. ( S ` X ) )
Assertion dpjlid 
|- ( ph -> ( ( P ` X ) ` A ) = A )

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 dpjlid.3 
 |-  ( ph -> X e. I )
5 dpjlid.4 
 |-  ( ph -> A e. ( S ` X ) )
6 eqid 
 |-  ( proj1 ` G ) = ( proj1 ` G )
7 1 2 3 6 4 dpjval 
 |-  ( ph -> ( P ` X ) = ( ( S ` X ) ( proj1 ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) )
8 7 fveq1d 
 |-  ( ph -> ( ( P ` X ) ` A ) = ( ( ( S ` X ) ( proj1 ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) ` A ) )
9 eqid 
 |-  ( +g ` G ) = ( +g ` G )
10 eqid 
 |-  ( LSSum ` G ) = ( LSSum ` G )
11 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
12 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
13 1 2 dprdf2 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
14 13 4 ffvelrnd 
 |-  ( ph -> ( S ` X ) e. ( SubGrp ` G ) )
15 difssd 
 |-  ( ph -> ( I \ { X } ) C_ I )
16 1 2 15 dprdres 
 |-  ( ph -> ( G dom DProd ( S |` ( I \ { X } ) ) /\ ( G DProd ( S |` ( I \ { X } ) ) ) C_ ( G DProd S ) ) )
17 16 simpld 
 |-  ( ph -> G dom DProd ( S |` ( I \ { X } ) ) )
18 dprdsubg 
 |-  ( G dom DProd ( S |` ( I \ { X } ) ) -> ( G DProd ( S |` ( I \ { X } ) ) ) e. ( SubGrp ` G ) )
19 17 18 syl 
 |-  ( ph -> ( G DProd ( S |` ( I \ { X } ) ) ) e. ( SubGrp ` G ) )
20 1 2 4 11 dpjdisj 
 |-  ( ph -> ( ( S ` X ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) = { ( 0g ` G ) } )
21 1 2 4 12 dpjcntz 
 |-  ( ph -> ( S ` X ) C_ ( ( Cntz ` G ) ` ( G DProd ( S |` ( I \ { X } ) ) ) ) )
22 9 10 11 12 14 19 20 21 6 pj1lid 
 |-  ( ( ph /\ A e. ( S ` X ) ) -> ( ( ( S ` X ) ( proj1 ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) ` A ) = A )
23 5 22 mpdan 
 |-  ( ph -> ( ( ( S ` X ) ( proj1 ` G ) ( G DProd ( S |` ( I \ { X } ) ) ) ) ` A ) = A )
24 8 23 eqtrd 
 |-  ( ph -> ( ( P ` X ) ` A ) = A )