Metamath Proof Explorer


Theorem dochfN

Description: Domain and codomain of the subspace orthocomplement for the DVecH vector space. (Contributed by NM, 27-Dec-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dochf.h 𝐻 = ( LHyp ‘ 𝐾 )
dochf.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dochf.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochf.v 𝑉 = ( Base ‘ 𝑈 )
dochf.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochf.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
Assertion dochfN ( 𝜑 : 𝒫 𝑉 ⟶ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dochf.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dochf.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 dochf.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochf.v 𝑉 = ( Base ‘ 𝑈 )
5 dochf.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
6 dochf.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
7 fvexd ( ( 𝜑𝑥 ∈ 𝒫 𝑉 ) → ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ⊆ ( 𝐼𝑦 ) } ) ) ) ∈ V )
8 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 eqid ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
10 eqid ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
11 8 9 10 1 2 3 4 5 dochfval ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → = ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ⊆ ( 𝐼𝑦 ) } ) ) ) ) )
12 6 11 syl ( 𝜑 = ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ⊆ ( 𝐼𝑦 ) } ) ) ) ) )
13 elpwi ( 𝑦 ∈ 𝒫 𝑉𝑦𝑉 )
14 1 2 3 4 5 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑦𝑉 ) → ( 𝑦 ) ∈ ran 𝐼 )
15 6 13 14 syl2an ( ( 𝜑𝑦 ∈ 𝒫 𝑉 ) → ( 𝑦 ) ∈ ran 𝐼 )
16 7 12 15 fmpt2d ( 𝜑 : 𝒫 𝑉 ⟶ ran 𝐼 )