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 38364
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 38363 . 2 class ocH
2 vk . . 3 setvar 𝑘
3 cvv 3492 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1527 . . . . 5 class 𝑘
6 clh 37000 . . . . 5 class LHyp
75, 6cfv 6348 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1527 . . . . . . . 8 class 𝑤
10 cdvh 38094 . . . . . . . . 9 class DVecH
115, 10cfv 6348 . . . . . . . 8 class (DVecH‘𝑘)
129, 11cfv 6348 . . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13 cbs 16471 . . . . . . 7 class Base
1412, 13cfv 6348 . . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
1514cpw 4535 . . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
168cv 1527 . . . . . . . . . 10 class 𝑥
17 vy . . . . . . . . . . . 12 setvar 𝑦
1817cv 1527 . . . . . . . . . . 11 class 𝑦
19 cdih 38244 . . . . . . . . . . . . 13 class DIsoH
205, 19cfv 6348 . . . . . . . . . . . 12 class (DIsoH‘𝑘)
219, 20cfv 6348 . . . . . . . . . . 11 class ((DIsoH‘𝑘)‘𝑤)
2218, 21cfv 6348 . . . . . . . . . 10 class (((DIsoH‘𝑘)‘𝑤)‘𝑦)
2316, 22wss 3933 . . . . . . . . 9 wff 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)
245, 13cfv 6348 . . . . . . . . 9 class (Base‘𝑘)
2523, 17, 24crab 3139 . . . . . . . 8 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}
26 cglb 17541 . . . . . . . . 9 class glb
275, 26cfv 6348 . . . . . . . 8 class (glb‘𝑘)
2825, 27cfv 6348 . . . . . . 7 class ((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})
29 coc 16561 . . . . . . . 8 class oc
305, 29cfv 6348 . . . . . . 7 class (oc‘𝑘)
3128, 30cfv 6348 . . . . . 6 class ((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))
3231, 21cfv 6348 . . . . 5 class (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))
338, 15, 32cmpt 5137 . . . 4 class (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))
344, 7, 33cmpt 5137 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))
352, 3, 34cmpt 5137 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
361, 35wceq 1528 1 wff ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
Colors of variables: wff setvar class
This definition is referenced by:  dochffval  38365
  Copyright terms: Public domain W3C validator