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 37139
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 37138 . 2 class ocH
2 vk . . 3 setvar 𝑘
3 cvv 3340 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1631 . . . . 5 class 𝑘
6 clh 35773 . . . . 5 class LHyp
75, 6cfv 6049 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1631 . . . . . . . 8 class 𝑤
10 cdvh 36869 . . . . . . . . 9 class DVecH
115, 10cfv 6049 . . . . . . . 8 class (DVecH‘𝑘)
129, 11cfv 6049 . . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13 cbs 16059 . . . . . . 7 class Base
1412, 13cfv 6049 . . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
1514cpw 4302 . . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
168cv 1631 . . . . . . . . . 10 class 𝑥
17 vy . . . . . . . . . . . 12 setvar 𝑦
1817cv 1631 . . . . . . . . . . 11 class 𝑦
19 cdih 37019 . . . . . . . . . . . . 13 class DIsoH
205, 19cfv 6049 . . . . . . . . . . . 12 class (DIsoH‘𝑘)
219, 20cfv 6049 . . . . . . . . . . 11 class ((DIsoH‘𝑘)‘𝑤)
2218, 21cfv 6049 . . . . . . . . . 10 class (((DIsoH‘𝑘)‘𝑤)‘𝑦)
2316, 22wss 3715 . . . . . . . . 9 wff 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)
245, 13cfv 6049 . . . . . . . . 9 class (Base‘𝑘)
2523, 17, 24crab 3054 . . . . . . . 8 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}
26 cglb 17144 . . . . . . . . 9 class glb
275, 26cfv 6049 . . . . . . . 8 class (glb‘𝑘)
2825, 27cfv 6049 . . . . . . 7 class ((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})
29 coc 16151 . . . . . . . 8 class oc
305, 29cfv 6049 . . . . . . 7 class (oc‘𝑘)
3128, 30cfv 6049 . . . . . 6 class ((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))
3231, 21cfv 6049 . . . . 5 class (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))
338, 15, 32cmpt 4881 . . . 4 class (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))
344, 7, 33cmpt 4881 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))
352, 3, 34cmpt 4881 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
361, 35wceq 1632 1 wff ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
Colors of variables: wff setvar class
This definition is referenced by:  dochffval  37140
  Copyright terms: Public domain W3C validator