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 38660
 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 38659 . 2 class ocH
2 vk . . 3 setvar 𝑘
3 cvv 3441 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1537 . . . . 5 class 𝑘
6 clh 37296 . . . . 5 class LHyp
75, 6cfv 6324 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1537 . . . . . . . 8 class 𝑤
10 cdvh 38390 . . . . . . . . 9 class DVecH
115, 10cfv 6324 . . . . . . . 8 class (DVecH‘𝑘)
129, 11cfv 6324 . . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13 cbs 16477 . . . . . . 7 class Base
1412, 13cfv 6324 . . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
1514cpw 4497 . . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
168cv 1537 . . . . . . . . . 10 class 𝑥
17 vy . . . . . . . . . . . 12 setvar 𝑦
1817cv 1537 . . . . . . . . . . 11 class 𝑦
19 cdih 38540 . . . . . . . . . . . . 13 class DIsoH
205, 19cfv 6324 . . . . . . . . . . . 12 class (DIsoH‘𝑘)
219, 20cfv 6324 . . . . . . . . . . 11 class ((DIsoH‘𝑘)‘𝑤)
2218, 21cfv 6324 . . . . . . . . . 10 class (((DIsoH‘𝑘)‘𝑤)‘𝑦)
2316, 22wss 3881 . . . . . . . . 9 wff 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)
245, 13cfv 6324 . . . . . . . . 9 class (Base‘𝑘)
2523, 17, 24crab 3110 . . . . . . . 8 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}
26 cglb 17547 . . . . . . . . 9 class glb
275, 26cfv 6324 . . . . . . . 8 class (glb‘𝑘)
2825, 27cfv 6324 . . . . . . 7 class ((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})
29 coc 16567 . . . . . . . 8 class oc
305, 29cfv 6324 . . . . . . 7 class (oc‘𝑘)
3128, 30cfv 6324 . . . . . 6 class ((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))
3231, 21cfv 6324 . . . . 5 class (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))
338, 15, 32cmpt 5110 . . . 4 class (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))
344, 7, 33cmpt 5110 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))
352, 3, 34cmpt 5110 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
361, 35wceq 1538 1 wff ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
 Colors of variables: wff setvar class This definition is referenced by:  dochffval  38661
 Copyright terms: Public domain W3C validator