Metamath Proof Explorer

Theorem pjff

Description: A projection is a linear operator. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypothesis pjf.k ⊢ K = proj ⁡ W
Assertion pjff ⊢ W ∈ PreHil → K : dom ⁡ K ⟶ W LMHom W

Proof

Step Hyp Ref Expression
1 pjf.k ⊢ K = proj ⁡ W
2 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
3 eqid ⊢ LSSum ⁡ W = LSSum ⁡ W
4 eqid ⊢ 0 W = 0 W
5 eqid ⊢ proj 1 ⁡ W = proj 1 ⁡ W
6 phllmod ⊢ W ∈ PreHil → W ∈ LMod
7 6 adantr ⊢ W ∈ PreHil ∧ x ∈ dom ⁡ K → W ∈ LMod
8 eqid ⊢ Base W = Base W
9 eqid ⊢ ocv ⁡ W = ocv ⁡ W
10 8 2 9 3 1 pjdm2 ⊢ W ∈ PreHil → x ∈ dom ⁡ K ↔ x ∈ LSubSp ⁡ W ∧ x LSSum ⁡ W ocv ⁡ W ⁡ x = Base W
11 10 simprbda ⊢ W ∈ PreHil ∧ x ∈ dom ⁡ K → x ∈ LSubSp ⁡ W
12 8 2 lssss ⊢ x ∈ LSubSp ⁡ W → x ⊆ Base W
13 11 12 syl ⊢ W ∈ PreHil ∧ x ∈ dom ⁡ K → x ⊆ Base W
14 8 9 2 ocvlss ⊢ W ∈ PreHil ∧ x ⊆ Base W → ocv ⁡ W ⁡ x ∈ LSubSp ⁡ W
15 13 14 syldan ⊢ W ∈ PreHil ∧ x ∈ dom ⁡ K → ocv ⁡ W ⁡ x ∈ LSubSp ⁡ W
16 9 2 4 ocvin ⊢ W ∈ PreHil ∧ x ∈ LSubSp ⁡ W → x ∩ ocv ⁡ W ⁡ x = 0 W
17 11 16 syldan ⊢ W ∈ PreHil ∧ x ∈ dom ⁡ K → x ∩ ocv ⁡ W ⁡ x = 0 W
18 2 3 4 5 7 11 15 17 pj1lmhm ⊢ W ∈ PreHil ∧ x ∈ dom ⁡ K → x proj 1 ⁡ W ocv ⁡ W ⁡ x ∈ W ↾ 𝑠 x LSSum ⁡ W ocv ⁡ W ⁡ x LMHom W
19 10 simplbda ⊢ W ∈ PreHil ∧ x ∈ dom ⁡ K → x LSSum ⁡ W ocv ⁡ W ⁡ x = Base W
20 19 oveq2d ⊢ W ∈ PreHil ∧ x ∈ dom ⁡ K → W ↾ 𝑠 x LSSum ⁡ W ocv ⁡ W ⁡ x = W ↾ 𝑠 Base W
21 8 ressid ⊢ W ∈ PreHil → W ↾ 𝑠 Base W = W
22 21 adantr ⊢ W ∈ PreHil ∧ x ∈ dom ⁡ K → W ↾ 𝑠 Base W = W
23 20 22 eqtrd ⊢ W ∈ PreHil ∧ x ∈ dom ⁡ K → W ↾ 𝑠 x LSSum ⁡ W ocv ⁡ W ⁡ x = W
24 23 oveq1d ⊢ W ∈ PreHil ∧ x ∈ dom ⁡ K → W ↾ 𝑠 x LSSum ⁡ W ocv ⁡ W ⁡ x LMHom W = W LMHom W
25 18 24 eleqtrd ⊢ W ∈ PreHil ∧ x ∈ dom ⁡ K → x proj 1 ⁡ W ocv ⁡ W ⁡ x ∈ W LMHom W
26 9 5 1 pjfval2 ⊢ K = x ∈ dom ⁡ K ⟼ x proj 1 ⁡ W ocv ⁡ W ⁡ x
27 25 26 fmptd ⊢ W ∈ PreHil → K : dom ⁡ K ⟶ W LMHom W