Metamath Proof Explorer


Theorem pj1lmhm

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 pj1lmhm φ T P U W 𝑠 T ˙ U LMHom W

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 eqid + W = + W
10 eqid Cntz W = Cntz W
11 1 lsssssubg W LMod L SubGrp W
12 5 11 syl φ L SubGrp W
13 12 6 sseldd φ T SubGrp W
14 12 7 sseldd φ U SubGrp W
15 lmodabl W LMod W Abel
16 5 15 syl φ W Abel
17 10 16 13 14 ablcntzd φ T Cntz W U
18 9 2 3 10 13 14 8 17 4 pj1ghm φ T P U W 𝑠 T ˙ U GrpHom W
19 eqid Scalar W = Scalar W
20 19 a1i φ Scalar W = Scalar W
21 9 2 3 10 13 14 8 17 4 pj1id φ y T ˙ U y = T P U y + W U P T y
22 21 adantrl φ x Base Scalar W y T ˙ U y = T P U y + W U P T y
23 22 oveq2d φ x Base Scalar W y T ˙ U x W y = x W T P U y + W U P T y
24 5 adantr φ x Base Scalar W y T ˙ U W LMod
25 simprl φ x Base Scalar W y T ˙ U x Base Scalar W
26 6 adantr φ x Base Scalar W y T ˙ U T L
27 eqid Base W = Base W
28 27 1 lssss T L T Base W
29 26 28 syl φ x Base Scalar W y T ˙ U T Base W
30 13 adantr φ x Base Scalar W y T ˙ U T SubGrp W
31 14 adantr φ x Base Scalar W y T ˙ U U SubGrp W
32 8 adantr φ x Base Scalar W y T ˙ U T U = 0 ˙
33 17 adantr φ x Base Scalar W y T ˙ U T Cntz W U
34 9 2 3 10 30 31 32 33 4 pj1f φ x Base Scalar W y T ˙ U T P U : T ˙ U T
35 simprr φ x Base Scalar W y T ˙ U y T ˙ U
36 34 35 ffvelrnd φ x Base Scalar W y T ˙ U T P U y T
37 29 36 sseldd φ x Base Scalar W y T ˙ U T P U y Base W
38 7 adantr φ x Base Scalar W y T ˙ U U L
39 27 1 lssss U L U Base W
40 38 39 syl φ x Base Scalar W y T ˙ U U Base W
41 9 2 3 10 30 31 32 33 4 pj2f φ x Base Scalar W y T ˙ U U P T : T ˙ U U
42 41 35 ffvelrnd φ x Base Scalar W y T ˙ U U P T y U
43 40 42 sseldd φ x Base Scalar W y T ˙ U U P T y Base W
44 eqid W = W
45 eqid Base Scalar W = Base Scalar W
46 27 9 19 44 45 lmodvsdi W LMod x Base Scalar W T P U y Base W U P T y Base W x W T P U y + W U P T y = x W T P U y + W x W U P T y
47 24 25 37 43 46 syl13anc φ x Base Scalar W y T ˙ U x W T P U y + W U P T y = x W T P U y + W x W U P T y
48 23 47 eqtrd φ x Base Scalar W y T ˙ U x W y = x W T P U y + W x W U P T y
49 1 2 lsmcl W LMod T L U L T ˙ U L
50 5 6 7 49 syl3anc φ T ˙ U L
51 50 adantr φ x Base Scalar W y T ˙ U T ˙ U L
52 19 44 45 1 lssvscl W LMod T ˙ U L x Base Scalar W y T ˙ U x W y T ˙ U
53 24 51 25 35 52 syl22anc φ x Base Scalar W y T ˙ U x W y T ˙ U
54 19 44 45 1 lssvscl W LMod T L x Base Scalar W T P U y T x W T P U y T
55 24 26 25 36 54 syl22anc φ x Base Scalar W y T ˙ U x W T P U y T
56 19 44 45 1 lssvscl W LMod U L x Base Scalar W U P T y U x W U P T y U
57 24 38 25 42 56 syl22anc φ x Base Scalar W y T ˙ U x W U P T y U
58 9 2 3 10 30 31 32 33 4 53 55 57 pj1eq φ x Base Scalar W y T ˙ U x W y = x W T P U y + W x W U P T y T P U x W y = x W T P U y U P T x W y = x W U P T y
59 48 58 mpbid φ x Base Scalar W y T ˙ U T P U x W y = x W T P U y U P T x W y = x W U P T y
60 59 simpld φ x Base Scalar W y T ˙ U T P U x W y = x W T P U y
61 60 ralrimivva φ x Base Scalar W y T ˙ U T P U x W y = x W T P U y
62 12 50 sseldd φ T ˙ U SubGrp W
63 eqid W 𝑠 T ˙ U = W 𝑠 T ˙ U
64 63 subgbas T ˙ U SubGrp W T ˙ U = Base W 𝑠 T ˙ U
65 62 64 syl φ T ˙ U = Base W 𝑠 T ˙ U
66 65 raleqdv φ y T ˙ U T P U x W y = x W T P U y y Base W 𝑠 T ˙ U T P U x W y = x W T P U y
67 66 ralbidv φ x Base Scalar W y T ˙ U T P U x W y = x W T P U y x Base Scalar W y Base W 𝑠 T ˙ U T P U x W y = x W T P U y
68 61 67 mpbid φ x Base Scalar W y Base W 𝑠 T ˙ U T P U x W y = x W T P U y
69 63 1 lsslmod W LMod T ˙ U L W 𝑠 T ˙ U LMod
70 5 50 69 syl2anc φ W 𝑠 T ˙ U LMod
71 ovex T ˙ U V
72 63 19 resssca T ˙ U V Scalar W = Scalar W 𝑠 T ˙ U
73 71 72 ax-mp Scalar W = Scalar W 𝑠 T ˙ U
74 eqid Base W 𝑠 T ˙ U = Base W 𝑠 T ˙ U
75 63 44 ressvsca T ˙ U V W = W 𝑠 T ˙ U
76 71 75 ax-mp W = W 𝑠 T ˙ U
77 73 19 45 74 76 44 islmhm3 W 𝑠 T ˙ U LMod W LMod T P U W 𝑠 T ˙ U LMHom W T P U W 𝑠 T ˙ U GrpHom W Scalar W = Scalar W x Base Scalar W y Base W 𝑠 T ˙ U T P U x W y = x W T P U y
78 70 5 77 syl2anc φ T P U W 𝑠 T ˙ U LMHom W T P U W 𝑠 T ˙ U GrpHom W Scalar W = Scalar W x Base Scalar W y Base W 𝑠 T ˙ U T P U x W y = x W T P U y
79 18 20 68 78 mpbir3and φ T P U W 𝑠 T ˙ U LMHom W