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 ⊢ L = LSubSp ⁡ W
pj1lmhm.s ⊢ ⊕ ˙ = LSSum ⁡ W
pj1lmhm.z ⊢ 0 ˙ = 0 W
pj1lmhm.p ⊢ P = proj 1 ⁡ W
pj1lmhm.1 ⊢ φ → W ∈ LMod
pj1lmhm.2 ⊢ φ → T ∈ L
pj1lmhm.3 ⊢ φ → U ∈ L
pj1lmhm.4 ⊢ φ → T ∩ U = 0 ˙
Assertion pj1lmhm2 ⊢ φ → T P U ∈ W ↾ 𝑠 T ⊕ ˙ U LMHom W ↾ 𝑠 T

Proof

Step Hyp Ref Expression
1 pj1lmhm.l ⊢ L = LSubSp ⁡ W
2 pj1lmhm.s ⊢ ⊕ ˙ = LSSum ⁡ W
3 pj1lmhm.z ⊢ 0 ˙ = 0 W
4 pj1lmhm.p ⊢ P = proj 1 ⁡ W
5 pj1lmhm.1 ⊢ φ → W ∈ LMod
6 pj1lmhm.2 ⊢ φ → T ∈ L
7 pj1lmhm.3 ⊢ φ → U ∈ L
8 pj1lmhm.4 ⊢ φ → T ∩ U = 0 ˙
9 1 2 3 4 5 6 7 8 pj1lmhm ⊢ φ → T P U ∈ W ↾ 𝑠 T ⊕ ˙ U LMHom W
10 eqid ⊢ + W = + W
11 eqid ⊢ Cntz ⁡ W = Cntz ⁡ W
12 1 lsssssubg ⊢ W ∈ LMod → L ⊆ SubGrp ⁡ W
13 5 12 syl ⊢ φ → L ⊆ SubGrp ⁡ W
14 13 6 sseldd ⊢ φ → T ∈ SubGrp ⁡ W
15 13 7 sseldd ⊢ φ → U ∈ SubGrp ⁡ W
16 lmodabl ⊢ W ∈ LMod → W ∈ Abel
17 5 16 syl ⊢ φ → W ∈ Abel
18 11 17 14 15 ablcntzd ⊢ φ → T ⊆ Cntz ⁡ W ⁡ U
19 10 2 3 11 14 15 8 18 4 pj1f ⊢ φ → T P U : T ⊕ ˙ U ⟶ T
20 19 frnd ⊢ φ → ran ⁡ T P U ⊆ T
21 eqid ⊢ W ↾ 𝑠 T = W ↾ 𝑠 T
22 21 1 reslmhm2b ⊢ W ∈ LMod ∧ T ∈ L ∧ ran ⁡ T P U ⊆ T → T P U ∈ W ↾ 𝑠 T ⊕ ˙ U LMHom W ↔ T P U ∈ W ↾ 𝑠 T ⊕ ˙ U LMHom W ↾ 𝑠 T
23 5 6 20 22 syl3anc ⊢ φ → T P U ∈ W ↾ 𝑠 T ⊕ ˙ U LMHom W ↔ T P U ∈ W ↾ 𝑠 T ⊕ ˙ U LMHom W ↾ 𝑠 T
24 9 23 mpbid ⊢ φ → T P U ∈ W ↾ 𝑠 T ⊕ ˙ U LMHom W ↾ 𝑠 T