This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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