Metamath Proof Explorer


Theorem pjpm

Description: The projection map is a partial function from subspaces of the pre-Hilbert space to total operators. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses pjpm.v 𝑉 = ( Base ‘ 𝑊 )
pjpm.l 𝐿 = ( LSubSp ‘ 𝑊 )
pjpm.k 𝐾 = ( proj ‘ 𝑊 )
Assertion pjpm 𝐾 ∈ ( ( 𝑉m 𝑉 ) ↑pm 𝐿 )

Proof

Step Hyp Ref Expression
1 pjpm.v 𝑉 = ( Base ‘ 𝑊 )
2 pjpm.l 𝐿 = ( LSubSp ‘ 𝑊 )
3 pjpm.k 𝐾 = ( proj ‘ 𝑊 )
4 eqid ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
5 eqid ( proj1𝑊 ) = ( proj1𝑊 )
6 1 2 4 5 3 pjfval 𝐾 = ( ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉m 𝑉 ) ) )
7 inss1 ( ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉m 𝑉 ) ) ) ⊆ ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) )
8 6 7 eqsstri 𝐾 ⊆ ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) )
9 funmpt Fun ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) )
10 funss ( 𝐾 ⊆ ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) → ( Fun ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) → Fun 𝐾 ) )
11 8 9 10 mp2 Fun 𝐾
12 eqid ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) = ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) )
13 ovexd ( 𝑥𝐿 → ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ∈ V )
14 12 13 fmpti ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) : 𝐿 ⟶ V
15 fssxp ( ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) : 𝐿 ⟶ V → ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) ⊆ ( 𝐿 × V ) )
16 ssrin ( ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) ⊆ ( 𝐿 × V ) → ( ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉m 𝑉 ) ) ) ⊆ ( ( 𝐿 × V ) ∩ ( V × ( 𝑉m 𝑉 ) ) ) )
17 14 15 16 mp2b ( ( 𝑥𝐿 ↦ ( 𝑥 ( proj1𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉m 𝑉 ) ) ) ⊆ ( ( 𝐿 × V ) ∩ ( V × ( 𝑉m 𝑉 ) ) )
18 6 17 eqsstri 𝐾 ⊆ ( ( 𝐿 × V ) ∩ ( V × ( 𝑉m 𝑉 ) ) )
19 inxp ( ( 𝐿 × V ) ∩ ( V × ( 𝑉m 𝑉 ) ) ) = ( ( 𝐿 ∩ V ) × ( V ∩ ( 𝑉m 𝑉 ) ) )
20 inv1 ( 𝐿 ∩ V ) = 𝐿
21 incom ( V ∩ ( 𝑉m 𝑉 ) ) = ( ( 𝑉m 𝑉 ) ∩ V )
22 inv1 ( ( 𝑉m 𝑉 ) ∩ V ) = ( 𝑉m 𝑉 )
23 21 22 eqtri ( V ∩ ( 𝑉m 𝑉 ) ) = ( 𝑉m 𝑉 )
24 20 23 xpeq12i ( ( 𝐿 ∩ V ) × ( V ∩ ( 𝑉m 𝑉 ) ) ) = ( 𝐿 × ( 𝑉m 𝑉 ) )
25 19 24 eqtri ( ( 𝐿 × V ) ∩ ( V × ( 𝑉m 𝑉 ) ) ) = ( 𝐿 × ( 𝑉m 𝑉 ) )
26 18 25 sseqtri 𝐾 ⊆ ( 𝐿 × ( 𝑉m 𝑉 ) )
27 ovex ( 𝑉m 𝑉 ) ∈ V
28 2 fvexi 𝐿 ∈ V
29 27 28 elpm ( 𝐾 ∈ ( ( 𝑉m 𝑉 ) ↑pm 𝐿 ) ↔ ( Fun 𝐾𝐾 ⊆ ( 𝐿 × ( 𝑉m 𝑉 ) ) ) )
30 11 26 29 mpbir2an 𝐾 ∈ ( ( 𝑉m 𝑉 ) ↑pm 𝐿 )