Metamath Proof Explorer

Theorem pjf2

Description: A projection is a function from the base set to the subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses pjf.k ⊢ 𝐾 = ( proj ‘ 𝑊 )
pjf.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
Assertion pjf2 ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( 𝐾 ‘ 𝑇 ) : 𝑉 ⟶ 𝑇 )

Proof

Step Hyp Ref Expression
1 pjf.k ⊢ 𝐾 = ( proj ‘ 𝑊 )
2 pjf.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
4 eqid ⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
5 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
6 eqid ⊢ ( Cntz ‘ 𝑊 ) = ( Cntz ‘ 𝑊 )
7 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
8 7 adantr ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑊 ∈ LMod )
9 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
10 9 lsssssubg ⊢ ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
11 8 10 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
12 eqid ⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
13 2 9 12 4 1 pjdm2 ⊢ ( 𝑊 ∈ PreHil → ( 𝑇 ∈ dom 𝐾 ↔ ( 𝑇 ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) = 𝑉 ) ) )
14 13 simprbda ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 ∈ ( LSubSp ‘ 𝑊 ) )
15 11 14 sseldd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
16 2 9 lssss ⊢ ( 𝑇 ∈ ( LSubSp ‘ 𝑊 ) → 𝑇 ⊆ 𝑉 )
17 14 16 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 ⊆ 𝑉 )
18 2 12 9 ocvlss ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ⊆ 𝑉 ) → ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ∈ ( LSubSp ‘ 𝑊 ) )
19 17 18 syldan ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ∈ ( LSubSp ‘ 𝑊 ) )
20 11 19 sseldd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ∈ ( SubGrp ‘ 𝑊 ) )
21 12 9 5 ocvin ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑇 ∩ ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) = { ( 0g ‘ 𝑊 ) } )
22 14 21 syldan ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( 𝑇 ∩ ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) = { ( 0g ‘ 𝑊 ) } )
23 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
24 8 23 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑊 ∈ Abel )
25 6 24 15 20 ablcntzd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 ⊆ ( ( Cntz ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) )
26 eqid ⊢ ( proj1 ‘ 𝑊 ) = ( proj1 ‘ 𝑊 )
27 3 4 5 6 15 20 22 25 26 pj1f ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) : ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) ⟶ 𝑇 )
28 12 26 1 pjval ⊢ ( 𝑇 ∈ dom 𝐾 → ( 𝐾 ‘ 𝑇 ) = ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) )
29 28 adantl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( 𝐾 ‘ 𝑇 ) = ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) )
30 29 eqcomd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) = ( 𝐾 ‘ 𝑇 ) )
31 13 simplbda ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) = 𝑉 )
32 30 31 feq12d ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) : ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) ⟶ 𝑇 ↔ ( 𝐾 ‘ 𝑇 ) : 𝑉 ⟶ 𝑇 ) )
33 27 32 mpbid ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( 𝐾 ‘ 𝑇 ) : 𝑉 ⟶ 𝑇 )