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 )