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	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑇 ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 𝑋 )