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𝐺 )
pj1eu.s = ( LSSum ‘ 𝐺 )
pj1eu.o 0 = ( 0g𝐺 )
pj1eu.z 𝑍 = ( Cntz ‘ 𝐺 )
pj1eu.2 ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
pj1eu.3 ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
pj1eu.4 ( 𝜑 → ( 𝑇𝑈 ) = { 0 } )
pj1eu.5 ( 𝜑𝑇 ⊆ ( 𝑍𝑈 ) )
pj1f.p 𝑃 = ( proj1𝐺 )
Assertion pj1lid ( ( 𝜑𝑋𝑇 ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 pj1eu.a + = ( +g𝐺 )
2 pj1eu.s = ( LSSum ‘ 𝐺 )
3 pj1eu.o 0 = ( 0g𝐺 )
4 pj1eu.z 𝑍 = ( Cntz ‘ 𝐺 )
5 pj1eu.2 ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
6 pj1eu.3 ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
7 pj1eu.4 ( 𝜑 → ( 𝑇𝑈 ) = { 0 } )
8 pj1eu.5 ( 𝜑𝑇 ⊆ ( 𝑍𝑈 ) )
9 pj1f.p 𝑃 = ( proj1𝐺 )
10 5 adantr ( ( 𝜑𝑋𝑇 ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
11 subgrcl ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
12 10 11 syl ( ( 𝜑𝑋𝑇 ) → 𝐺 ∈ Grp )
13 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
14 13 subgss ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
15 5 14 syl ( 𝜑𝑇 ⊆ ( Base ‘ 𝐺 ) )
16 15 sselda ( ( 𝜑𝑋𝑇 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
17 13 1 3 grprid ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑋 + 0 ) = 𝑋 )
18 12 16 17 syl2anc ( ( 𝜑𝑋𝑇 ) → ( 𝑋 + 0 ) = 𝑋 )
19 18 eqcomd ( ( 𝜑𝑋𝑇 ) → 𝑋 = ( 𝑋 + 0 ) )
20 6 adantr ( ( 𝜑𝑋𝑇 ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
21 7 adantr ( ( 𝜑𝑋𝑇 ) → ( 𝑇𝑈 ) = { 0 } )
22 8 adantr ( ( 𝜑𝑋𝑇 ) → 𝑇 ⊆ ( 𝑍𝑈 ) )
23 2 lsmub1 ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( 𝑇 𝑈 ) )
24 5 6 23 syl2anc ( 𝜑𝑇 ⊆ ( 𝑇 𝑈 ) )
25 24 sselda ( ( 𝜑𝑋𝑇 ) → 𝑋 ∈ ( 𝑇 𝑈 ) )
26 simpr ( ( 𝜑𝑋𝑇 ) → 𝑋𝑇 )
27 3 subg0cl ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 0𝑈 )
28 20 27 syl ( ( 𝜑𝑋𝑇 ) → 0𝑈 )
29 1 2 3 4 10 20 21 22 9 25 26 28 pj1eq ( ( 𝜑𝑋𝑇 ) → ( 𝑋 = ( 𝑋 + 0 ) ↔ ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 𝑋 ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = 0 ) ) )
30 19 29 mpbid ( ( 𝜑𝑋𝑇 ) → ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 𝑋 ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = 0 ) )
31 30 simpld ( ( 𝜑𝑋𝑇 ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 𝑋 )