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