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 ⊢ H = LHyp ⁡ K
dochf.i ⊢ I = DIsoH ⁡ K ⁡ W
dochf.u ⊢ U = DVecH ⁡ K ⁡ W
dochf.v ⊢ V = Base U
dochf.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochf.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion dochfN ⊢ φ → ⊥ ˙ : 𝒫 V ⟶ ran ⁡ I

Proof

Step Hyp Ref Expression
1 dochf.h ⊢ H = LHyp ⁡ K
2 dochf.i ⊢ I = DIsoH ⁡ K ⁡ W
3 dochf.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochf.v ⊢ V = Base U
5 dochf.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
6 dochf.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 fvexd ⊢ φ ∧ x ∈ 𝒫 V → I ⁡ oc ⁡ K ⁡ glb ⁡ K ⁡ y ∈ Base K | x ⊆ I ⁡ y ∈ V
8 eqid ⊢ Base K = Base K
9 eqid ⊢ glb ⁡ K = glb ⁡ K
10 eqid ⊢ oc ⁡ K = oc ⁡ K
11 8 9 10 1 2 3 4 5 dochfval ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ = x ∈ 𝒫 V ⟼ I ⁡ oc ⁡ K ⁡ glb ⁡ K ⁡ y ∈ Base K | x ⊆ I ⁡ y
12 6 11 syl ⊢ φ → ⊥ ˙ = x ∈ 𝒫 V ⟼ I ⁡ oc ⁡ K ⁡ glb ⁡ K ⁡ y ∈ Base K | x ⊆ I ⁡ y
13 elpwi ⊢ y ∈ 𝒫 V → y ⊆ V
14 1 2 3 4 5 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ y ⊆ V → ⊥ ˙ ⁡ y ∈ ran ⁡ I
15 6 13 14 syl2an ⊢ φ ∧ y ∈ 𝒫 V → ⊥ ˙ ⁡ y ∈ ran ⁡ I
16 7 12 15 fmpt2d ⊢ φ → ⊥ ˙ : 𝒫 V ⟶ ran ⁡ I