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 𝐿 )