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