Metamath Proof Explorer

Definition df-doch

Description: Define subspace orthocomplement for DVecH vector space. Temporarily, we are using the range of the isomorphism instead of the set of closed subspaces. Later, when inner product is introduced, we will show that these are the same. (Contributed by NM, 14-Mar-2014)

Ref Expression
Assertion df-doch ⊢ ocH = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ DIsoH ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 coch class ocH
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp ⁡ k
7 vx setvar x
8 cbs class Base
9 cdvh class DVecH
10 5 9 cfv class DVecH ⁡ k
11 3 cv setvar w
12 11 10 cfv class DVecH ⁡ k ⁡ w
13 12 8 cfv class Base DVecH ⁡ k ⁡ w
14 13 cpw class 𝒫 Base DVecH ⁡ k ⁡ w
15 cdih class DIsoH
16 5 15 cfv class DIsoH ⁡ k
17 11 16 cfv class DIsoH ⁡ k ⁡ w
18 coc class oc
19 5 18 cfv class oc ⁡ k
20 cglb class glb
21 5 20 cfv class glb ⁡ k
22 vy setvar y
23 5 8 cfv class Base k
24 7 cv setvar x
25 22 cv setvar y
26 25 17 cfv class DIsoH ⁡ k ⁡ w ⁡ y
27 24 26 wss wff x ⊆ DIsoH ⁡ k ⁡ w ⁡ y
28 27 22 23 crab class y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y
29 28 21 cfv class glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y
30 29 19 cfv class oc ⁡ k ⁡ glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y
31 30 17 cfv class DIsoH ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y
32 7 14 31 cmpt class x ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ DIsoH ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y
33 3 6 32 cmpt class w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ DIsoH ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y
34 1 2 33 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ DIsoH ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y
35 0 34 wceq wff ocH = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ DIsoH ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y