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∈𝒫BaseDVecH⁡k⁡w⟼DIsoH⁡k⁡w⁡oc⁡k⁡glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y

Detailed syntax breakdown

Step Hyp Ref Expression
0 coch classocH
1 vk setvark
2 cvv classV
3 vw setvarw
4 clh classLHyp
5 1 cv setvark
6 5 4 cfv classLHyp⁡k
7 vx setvarx
8 cbs classBase
9 cdvh classDVecH
10 5 9 cfv classDVecH⁡k
11 3 cv setvarw
12 11 10 cfv classDVecH⁡k⁡w
13 12 8 cfv classBaseDVecH⁡k⁡w
14 13 cpw class𝒫BaseDVecH⁡k⁡w
15 cdih classDIsoH
16 5 15 cfv classDIsoH⁡k
17 11 16 cfv classDIsoH⁡k⁡w
18 coc classoc
19 5 18 cfv classoc⁡k
20 cglb classglb
21 5 20 cfv classglb⁡k
22 vy setvary
23 5 8 cfv classBasek
24 7 cv setvarx
25 22 cv setvary
26 25 17 cfv classDIsoH⁡k⁡w⁡y
27 24 26 wss wffx⊆DIsoH⁡k⁡w⁡y
28 27 22 23 crab classy∈Basek|x⊆DIsoH⁡k⁡w⁡y
29 28 21 cfv classglb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y
30 29 19 cfv classoc⁡k⁡glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y
31 30 17 cfv classDIsoH⁡k⁡w⁡oc⁡k⁡glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y
32 7 14 31 cmpt classx∈𝒫BaseDVecH⁡k⁡w⟼DIsoH⁡k⁡w⁡oc⁡k⁡glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y
33 3 6 32 cmpt classw∈LHyp⁡k⟼x∈𝒫BaseDVecH⁡k⁡w⟼DIsoH⁡k⁡w⁡oc⁡k⁡glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y
34 1 2 33 cmpt classk∈V⟼w∈LHyp⁡k⟼x∈𝒫BaseDVecH⁡k⁡w⟼DIsoH⁡k⁡w⁡oc⁡k⁡glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y
35 0 34 wceq wffocH=k∈V⟼w∈LHyp⁡k⟼x∈𝒫BaseDVecH⁡k⁡w⟼DIsoH⁡k⁡w⁡oc⁡k⁡glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y