Metamath Proof Explorer

Theorem pj1lid

Description: The left projection function is the identity on the left subspace. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses pj1eu.a 
|- .+ = ( +g ` G )
pj1eu.s 
|- .(+) = ( LSSum ` G )
pj1eu.o 
|- .0. = ( 0g ` G )
pj1eu.z 
|- Z = ( Cntz ` G )
pj1eu.2 
|- ( ph -> T e. ( SubGrp ` G ) )
pj1eu.3 
|- ( ph -> U e. ( SubGrp ` G ) )
pj1eu.4 
|- ( ph -> ( T i^i U ) = { .0. } )
pj1eu.5 
|- ( ph -> T C_ ( Z ` U ) )
pj1f.p 
|- P = ( proj1 ` G )
Assertion pj1lid 
|- ( ( ph /\ X e. T ) -> ( ( T P U ) ` X ) = X )

Proof

Step Hyp Ref Expression
1 pj1eu.a 
 |-  .+ = ( +g ` G )
2 pj1eu.s 
 |-  .(+) = ( LSSum ` G )
3 pj1eu.o 
 |-  .0. = ( 0g ` G )
4 pj1eu.z 
 |-  Z = ( Cntz ` G )
5 pj1eu.2 
 |-  ( ph -> T e. ( SubGrp ` G ) )
6 pj1eu.3 
 |-  ( ph -> U e. ( SubGrp ` G ) )
7 pj1eu.4 
 |-  ( ph -> ( T i^i U ) = { .0. } )
8 pj1eu.5 
 |-  ( ph -> T C_ ( Z ` U ) )
9 pj1f.p 
 |-  P = ( proj1 ` G )
10 5 adantr 
 |-  ( ( ph /\ X e. T ) -> T e. ( SubGrp ` G ) )
11 subgrcl 
 |-  ( T e. ( SubGrp ` G ) -> G e. Grp )
12 10 11 syl 
 |-  ( ( ph /\ X e. T ) -> G e. Grp )
13 eqid 
 |-  ( Base ` G ) = ( Base ` G )
14 13 subgss 
 |-  ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
15 5 14 syl 
 |-  ( ph -> T C_ ( Base ` G ) )
16 15 sselda 
 |-  ( ( ph /\ X e. T ) -> X e. ( Base ` G ) )
17 13 1 3 grprid 
 |-  ( ( G e. Grp /\ X e. ( Base ` G ) ) -> ( X .+ .0. ) = X )
18 12 16 17 syl2anc 
 |-  ( ( ph /\ X e. T ) -> ( X .+ .0. ) = X )
19 18 eqcomd 
 |-  ( ( ph /\ X e. T ) -> X = ( X .+ .0. ) )
20 6 adantr 
 |-  ( ( ph /\ X e. T ) -> U e. ( SubGrp ` G ) )
21 7 adantr 
 |-  ( ( ph /\ X e. T ) -> ( T i^i U ) = { .0. } )
22 8 adantr 
 |-  ( ( ph /\ X e. T ) -> T C_ ( Z ` U ) )
23 2 lsmub1 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T C_ ( T .(+) U ) )
24 5 6 23 syl2anc 
 |-  ( ph -> T C_ ( T .(+) U ) )
25 24 sselda 
 |-  ( ( ph /\ X e. T ) -> X e. ( T .(+) U ) )
26 simpr 
 |-  ( ( ph /\ X e. T ) -> X e. T )
27 3 subg0cl 
 |-  ( U e. ( SubGrp ` G ) -> .0. e. U )
28 20 27 syl 
 |-  ( ( ph /\ X e. T ) -> .0. e. U )
29 1 2 3 4 10 20 21 22 9 25 26 28 pj1eq 
 |-  ( ( ph /\ X e. T ) -> ( X = ( X .+ .0. ) <-> ( ( ( T P U ) ` X ) = X /\ ( ( U P T ) ` X ) = .0. ) ) )
30 19 29 mpbid 
 |-  ( ( ph /\ X e. T ) -> ( ( ( T P U ) ` X ) = X /\ ( ( U P T ) ` X ) = .0. ) )
31 30 simpld 
 |-  ( ( ph /\ X e. T ) -> ( ( T P U ) ` X ) = X )