Metamath Proof Explorer

Theorem pjfo

Description: A projection is a surjection onto the subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 pjf.k ⊢ 𝐾 = ( proj ‘ 𝑊 )
2 pjf.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 1 2 pjf2 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( 𝐾 ‘ 𝑇 ) : 𝑉 ⟶ 𝑇 )
4 3 frnd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ran ( 𝐾 ‘ 𝑇 ) ⊆ 𝑇 )
5 eqid ⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
6 eqid ⊢ ( proj1 ‘ 𝑊 ) = ( proj1 ‘ 𝑊 )
7 5 6 1 pjval ⊢ ( 𝑇 ∈ dom 𝐾 → ( 𝐾 ‘ 𝑇 ) = ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) )
8 7 ad2antlr ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝐾 ‘ 𝑇 ) = ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) )
9 8 fveq1d ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) ∧ 𝑥 ∈ 𝑇 ) → ( ( 𝐾 ‘ 𝑇 ) ‘ 𝑥 ) = ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) ‘ 𝑥 ) )
10 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
11 eqid ⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
12 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
13 eqid ⊢ ( Cntz ‘ 𝑊 ) = ( Cntz ‘ 𝑊 )
14 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
15 14 adantr ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑊 ∈ LMod )
16 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
17 16 lsssssubg ⊢ ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
18 15 17 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
19 2 16 5 11 1 pjdm2 ⊢ ( 𝑊 ∈ PreHil → ( 𝑇 ∈ dom 𝐾 ↔ ( 𝑇 ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) = 𝑉 ) ) )
20 19 simprbda ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 ∈ ( LSubSp ‘ 𝑊 ) )
21 18 20 sseldd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
22 2 16 lssss ⊢ ( 𝑇 ∈ ( LSubSp ‘ 𝑊 ) → 𝑇 ⊆ 𝑉 )
23 20 22 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 ⊆ 𝑉 )
24 2 5 16 ocvlss ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ⊆ 𝑉 ) → ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ∈ ( LSubSp ‘ 𝑊 ) )
25 23 24 syldan ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ∈ ( LSubSp ‘ 𝑊 ) )
26 18 25 sseldd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ∈ ( SubGrp ‘ 𝑊 ) )
27 5 16 12 ocvin ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑇 ∩ ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) = { ( 0g ‘ 𝑊 ) } )
28 20 27 syldan ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( 𝑇 ∩ ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) = { ( 0g ‘ 𝑊 ) } )
29 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
30 15 29 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑊 ∈ Abel )
31 13 30 21 26 ablcntzd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 ⊆ ( ( Cntz ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) )
32 10 11 12 13 21 26 28 31 6 pj1lid ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) ∧ 𝑥 ∈ 𝑇 ) → ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) ‘ 𝑥 ) = 𝑥 )
33 9 32 eqtrd ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) ∧ 𝑥 ∈ 𝑇 ) → ( ( 𝐾 ‘ 𝑇 ) ‘ 𝑥 ) = 𝑥 )
34 3 ffnd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( 𝐾 ‘ 𝑇 ) Fn 𝑉 )
35 23 sselda ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ 𝑉 )
36 fnfvelrn ⊢ ( ( ( 𝐾 ‘ 𝑇 ) Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐾 ‘ 𝑇 ) ‘ 𝑥 ) ∈ ran ( 𝐾 ‘ 𝑇 ) )
37 34 35 36 syl2an2r ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) ∧ 𝑥 ∈ 𝑇 ) → ( ( 𝐾 ‘ 𝑇 ) ‘ 𝑥 ) ∈ ran ( 𝐾 ‘ 𝑇 ) )
38 33 37 eqeltrrd ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ran ( 𝐾 ‘ 𝑇 ) )
39 4 38 eqelssd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ran ( 𝐾 ‘ 𝑇 ) = 𝑇 )
40 dffo2 ⊢ ( ( 𝐾 ‘ 𝑇 ) : 𝑉 –onto→ 𝑇 ↔ ( ( 𝐾 ‘ 𝑇 ) : 𝑉 ⟶ 𝑇 ∧ ran ( 𝐾 ‘ 𝑇 ) = 𝑇 ) )
41 3 39 40 sylanbrc ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( 𝐾 ‘ 𝑇 ) : 𝑉 –onto→ 𝑇 )