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