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 40207
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 40206 . 2 class ocH
2 vk . . 3 setvar π‘˜
3 cvv 3474 . . 3 class V
4 vw . . . 4 setvar 𝑀
52cv 1540 . . . . 5 class π‘˜
6 clh 38843 . . . . 5 class LHyp
75, 6cfv 6540 . . . 4 class (LHypβ€˜π‘˜)
8 vx . . . . 5 setvar π‘₯
94cv 1540 . . . . . . . 8 class 𝑀
10 cdvh 39937 . . . . . . . . 9 class DVecH
115, 10cfv 6540 . . . . . . . 8 class (DVecHβ€˜π‘˜)
129, 11cfv 6540 . . . . . . 7 class ((DVecHβ€˜π‘˜)β€˜π‘€)
13 cbs 17140 . . . . . . 7 class Base
1412, 13cfv 6540 . . . . . 6 class (Baseβ€˜((DVecHβ€˜π‘˜)β€˜π‘€))
1514cpw 4601 . . . . 5 class 𝒫 (Baseβ€˜((DVecHβ€˜π‘˜)β€˜π‘€))
168cv 1540 . . . . . . . . . 10 class π‘₯
17 vy . . . . . . . . . . . 12 setvar 𝑦
1817cv 1540 . . . . . . . . . . 11 class 𝑦
19 cdih 40087 . . . . . . . . . . . . 13 class DIsoH
205, 19cfv 6540 . . . . . . . . . . . 12 class (DIsoHβ€˜π‘˜)
219, 20cfv 6540 . . . . . . . . . . 11 class ((DIsoHβ€˜π‘˜)β€˜π‘€)
2218, 21cfv 6540 . . . . . . . . . 10 class (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜π‘¦)
2316, 22wss 3947 . . . . . . . . 9 wff π‘₯ βŠ† (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜π‘¦)
245, 13cfv 6540 . . . . . . . . 9 class (Baseβ€˜π‘˜)
2523, 17, 24crab 3432 . . . . . . . 8 class {𝑦 ∈ (Baseβ€˜π‘˜) ∣ π‘₯ βŠ† (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜π‘¦)}
26 cglb 18259 . . . . . . . . 9 class glb
275, 26cfv 6540 . . . . . . . 8 class (glbβ€˜π‘˜)
2825, 27cfv 6540 . . . . . . 7 class ((glbβ€˜π‘˜)β€˜{𝑦 ∈ (Baseβ€˜π‘˜) ∣ π‘₯ βŠ† (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜π‘¦)})
29 coc 17201 . . . . . . . 8 class oc
305, 29cfv 6540 . . . . . . 7 class (ocβ€˜π‘˜)
3128, 30cfv 6540 . . . . . 6 class ((ocβ€˜π‘˜)β€˜((glbβ€˜π‘˜)β€˜{𝑦 ∈ (Baseβ€˜π‘˜) ∣ π‘₯ βŠ† (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜π‘¦)}))
3231, 21cfv 6540 . . . . 5 class (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜((ocβ€˜π‘˜)β€˜((glbβ€˜π‘˜)β€˜{𝑦 ∈ (Baseβ€˜π‘˜) ∣ π‘₯ βŠ† (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜π‘¦)})))
338, 15, 32cmpt 5230 . . . 4 class (π‘₯ ∈ 𝒫 (Baseβ€˜((DVecHβ€˜π‘˜)β€˜π‘€)) ↦ (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜((ocβ€˜π‘˜)β€˜((glbβ€˜π‘˜)β€˜{𝑦 ∈ (Baseβ€˜π‘˜) ∣ π‘₯ βŠ† (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜π‘¦)}))))
344, 7, 33cmpt 5230 . . 3 class (𝑀 ∈ (LHypβ€˜π‘˜) ↦ (π‘₯ ∈ 𝒫 (Baseβ€˜((DVecHβ€˜π‘˜)β€˜π‘€)) ↦ (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜((ocβ€˜π‘˜)β€˜((glbβ€˜π‘˜)β€˜{𝑦 ∈ (Baseβ€˜π‘˜) ∣ π‘₯ βŠ† (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜π‘¦)})))))
352, 3, 34cmpt 5230 . 2 class (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ (π‘₯ ∈ 𝒫 (Baseβ€˜((DVecHβ€˜π‘˜)β€˜π‘€)) ↦ (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜((ocβ€˜π‘˜)β€˜((glbβ€˜π‘˜)β€˜{𝑦 ∈ (Baseβ€˜π‘˜) ∣ π‘₯ βŠ† (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜π‘¦)}))))))
361, 35wceq 1541 1 wff ocH = (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ (π‘₯ ∈ 𝒫 (Baseβ€˜((DVecHβ€˜π‘˜)β€˜π‘€)) ↦ (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜((ocβ€˜π‘˜)β€˜((glbβ€˜π‘˜)β€˜{𝑦 ∈ (Baseβ€˜π‘˜) ∣ π‘₯ βŠ† (((DIsoHβ€˜π‘˜)β€˜π‘€)β€˜π‘¦)}))))))
Colors of variables: wff setvar class
This definition is referenced by:  dochffval  40208
  Copyright terms: Public domain W3C validator