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