Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-doch Structured version   Visualization version   GIF version

Definition df-doch 36954
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.)
Assertion
Ref Expression
df-doch ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
Distinct variable group:   𝑤,𝑘,𝑥,𝑦

Detailed syntax breakdown of Definition df-doch
StepHypRef Expression
1 coch 36953 . 2 class ocH
2 vk . . 3 setvar 𝑘
3 cvv 3231 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1522 . . . . 5 class 𝑘
6 clh 35588 . . . . 5 class LHyp
75, 6cfv 5926 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1522 . . . . . . . 8 class 𝑤
10 cdvh 36684 . . . . . . . . 9 class DVecH
115, 10cfv 5926 . . . . . . . 8 class (DVecH‘𝑘)
129, 11cfv 5926 . . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13 cbs 15904 . . . . . . 7 class Base
1412, 13cfv 5926 . . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
1514cpw 4191 . . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
168cv 1522 . . . . . . . . . 10 class 𝑥
17 vy . . . . . . . . . . . 12 setvar 𝑦
1817cv 1522 . . . . . . . . . . 11 class 𝑦
19 cdih 36834 . . . . . . . . . . . . 13 class DIsoH
205, 19cfv 5926 . . . . . . . . . . . 12 class (DIsoH‘𝑘)
219, 20cfv 5926 . . . . . . . . . . 11 class ((DIsoH‘𝑘)‘𝑤)
2218, 21cfv 5926 . . . . . . . . . 10 class (((DIsoH‘𝑘)‘𝑤)‘𝑦)
2316, 22wss 3607 . . . . . . . . 9 wff 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)
245, 13cfv 5926 . . . . . . . . 9 class (Base‘𝑘)
2523, 17, 24crab 2945 . . . . . . . 8 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}
26 cglb 16990 . . . . . . . . 9 class glb
275, 26cfv 5926 . . . . . . . 8 class (glb‘𝑘)
2825, 27cfv 5926 . . . . . . 7 class ((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})
29 coc 15996 . . . . . . . 8 class oc
305, 29cfv 5926 . . . . . . 7 class (oc‘𝑘)
3128, 30cfv 5926 . . . . . 6 class ((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))
3231, 21cfv 5926 . . . . 5 class (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))
338, 15, 32cmpt 4762 . . . 4 class (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))
344, 7, 33cmpt 4762 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))
352, 3, 34cmpt 4762 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
361, 35wceq 1523 1 wff ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
Colors of variables: wff setvar class
This definition is referenced by:  dochffval  36955
  Copyright terms: Public domain W3C validator