Theorem pj1lmhm2

Description: The left projection function is a linear operator. (Contributed by Mario Carneiro, 15-Oct-2015) (Revised by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	pj1lmhm.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
	pj1lmhm.s	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	pj1lmhm.z	⊢ 0 = ( 0g ‘ 𝑊 )
	pj1lmhm.p	⊢ 𝑃 = ( proj1 ‘ 𝑊 )
	pj1lmhm.1	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	pj1lmhm.2	⊢ ( 𝜑 → 𝑇 ∈ 𝐿 )
	pj1lmhm.3	⊢ ( 𝜑 → 𝑈 ∈ 𝐿 )
	pj1lmhm.4	⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
Assertion	pj1lmhm2	⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) LMHom ( 𝑊 ↾s 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pj1lmhm.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
2		pj1lmhm.s	⊢ ⊕ = ( LSSum ‘ 𝑊 )
3		pj1lmhm.z	⊢ 0 = ( 0g ‘ 𝑊 )
4		pj1lmhm.p	⊢ 𝑃 = ( proj1 ‘ 𝑊 )
5		pj1lmhm.1	⊢ ( 𝜑 → 𝑊 ∈ LMod )
6		pj1lmhm.2	⊢ ( 𝜑 → 𝑇 ∈ 𝐿 )
7		pj1lmhm.3	⊢ ( 𝜑 → 𝑈 ∈ 𝐿 )
8		pj1lmhm.4	⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
9	1 2 3 4 5 6 7 8	pj1lmhm	⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) LMHom 𝑊 ) )
10		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
11		eqid	⊢ ( Cntz ‘ 𝑊 ) = ( Cntz ‘ 𝑊 )
12	1	lsssssubg	⊢ ( 𝑊 ∈ LMod → 𝐿 ⊆ ( SubGrp ‘ 𝑊 ) )
13	5 12	syl	⊢ ( 𝜑 → 𝐿 ⊆ ( SubGrp ‘ 𝑊 ) )
14	13 6	sseldd	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
15	13 7	sseldd	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
16		lmodabl	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
17	5 16	syl	⊢ ( 𝜑 → 𝑊 ∈ Abel )
18	11 17 14 15	ablcntzd	⊢ ( 𝜑 → 𝑇 ⊆ ( ( Cntz ‘ 𝑊 ) ‘ 𝑈 ) )
19	10 2 3 11 14 15 8 18 4	pj1f	⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑇 )
20	19	frnd	⊢ ( 𝜑 → ran ( 𝑇 𝑃 𝑈 ) ⊆ 𝑇 )
21		eqid	⊢ ( 𝑊 ↾s 𝑇 ) = ( 𝑊 ↾s 𝑇 )
22	21 1	reslmhm2b	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝐿 ∧ ran ( 𝑇 𝑃 𝑈 ) ⊆ 𝑇 ) → ( ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) LMHom 𝑊 ) ↔ ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) LMHom ( 𝑊 ↾s 𝑇 ) ) ) )
23	5 6 20 22	syl3anc	⊢ ( 𝜑 → ( ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) LMHom 𝑊 ) ↔ ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) LMHom ( 𝑊 ↾s 𝑇 ) ) ) )
24	9 23	mpbid	⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) LMHom ( 𝑊 ↾s 𝑇 ) ) )