This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑇 ) ) )