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 35451
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 35450 . 2 class ocH
2 vk . . 3 setvar 𝑘
3 cvv 3172 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1473 . . . . 5 class 𝑘
6 clh 34084 . . . . 5 class LHyp
75, 6cfv 5790 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1473 . . . . . . . 8 class 𝑤
10 cdvh 35181 . . . . . . . . 9 class DVecH
115, 10cfv 5790 . . . . . . . 8 class (DVecH‘𝑘)
129, 11cfv 5790 . . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13 cbs 15641 . . . . . . 7 class Base
1412, 13cfv 5790 . . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
1514cpw 4107 . . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
168cv 1473 . . . . . . . . . 10 class 𝑥
17 vy . . . . . . . . . . . 12 setvar 𝑦
1817cv 1473 . . . . . . . . . . 11 class 𝑦
19 cdih 35331 . . . . . . . . . . . . 13 class DIsoH
205, 19cfv 5790 . . . . . . . . . . . 12 class (DIsoH‘𝑘)
219, 20cfv 5790 . . . . . . . . . . 11 class ((DIsoH‘𝑘)‘𝑤)
2218, 21cfv 5790 . . . . . . . . . 10 class (((DIsoH‘𝑘)‘𝑤)‘𝑦)
2316, 22wss 3539 . . . . . . . . 9 wff 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)
245, 13cfv 5790 . . . . . . . . 9 class (Base‘𝑘)
2523, 17, 24crab 2899 . . . . . . . 8 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}
26 cglb 16712 . . . . . . . . 9 class glb
275, 26cfv 5790 . . . . . . . 8 class (glb‘𝑘)
2825, 27cfv 5790 . . . . . . 7 class ((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})
29 coc 15722 . . . . . . . 8 class oc
305, 29cfv 5790 . . . . . . 7 class (oc‘𝑘)
3128, 30cfv 5790 . . . . . 6 class ((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))
3231, 21cfv 5790 . . . . 5 class (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))
338, 15, 32cmpt 4637 . . . 4 class (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))
344, 7, 33cmpt 4637 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))
352, 3, 34cmpt 4637 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
361, 35wceq 1474 1 wff ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
Colors of variables: wff setvar class
This definition is referenced by:  dochffval  35452
  Copyright terms: Public domain W3C validator