Metamath Proof Explorer

Theorem pjff

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

Ref Expression
Hypothesis pjf.k ⊢ 𝐾 = ( proj ‘ 𝑊 )
Assertion pjff ( 𝑊 ∈ PreHil → 𝐾 : dom 𝐾 ⟶ ( 𝑊 LMHom 𝑊 ) )

Proof

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