Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-docaN Structured version   Visualization version   GIF version

Definition df-docaN 40295
Description: Define subspace orthocomplement for DVecA partial 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, 6-Dec-2013.)
Assertion
Ref Expression
df-docaN ocA = (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ (π‘₯ ∈ 𝒫 ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜((((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))(meetβ€˜π‘˜)𝑀)))))
Distinct variable group:   𝑀,π‘˜,π‘₯,𝑧

Detailed syntax breakdown of Definition df-docaN
StepHypRef Expression
1 cocaN 40294 . 2 class ocA
2 vk . . 3 setvar π‘˜
3 cvv 3473 . . 3 class V
4 vw . . . 4 setvar 𝑀
52cv 1539 . . . . 5 class π‘˜
6 clh 39159 . . . . 5 class LHyp
75, 6cfv 6544 . . . 4 class (LHypβ€˜π‘˜)
8 vx . . . . 5 setvar π‘₯
94cv 1539 . . . . . . 7 class 𝑀
10 cltrn 39276 . . . . . . . 8 class LTrn
115, 10cfv 6544 . . . . . . 7 class (LTrnβ€˜π‘˜)
129, 11cfv 6544 . . . . . 6 class ((LTrnβ€˜π‘˜)β€˜π‘€)
1312cpw 4603 . . . . 5 class 𝒫 ((LTrnβ€˜π‘˜)β€˜π‘€)
148cv 1539 . . . . . . . . . . . . 13 class π‘₯
15 vz . . . . . . . . . . . . . 14 setvar 𝑧
1615cv 1539 . . . . . . . . . . . . 13 class 𝑧
1714, 16wss 3949 . . . . . . . . . . . 12 wff π‘₯ βŠ† 𝑧
18 cdia 40203 . . . . . . . . . . . . . . 15 class DIsoA
195, 18cfv 6544 . . . . . . . . . . . . . 14 class (DIsoAβ€˜π‘˜)
209, 19cfv 6544 . . . . . . . . . . . . 13 class ((DIsoAβ€˜π‘˜)β€˜π‘€)
2120crn 5678 . . . . . . . . . . . 12 class ran ((DIsoAβ€˜π‘˜)β€˜π‘€)
2217, 15, 21crab 3431 . . . . . . . . . . 11 class {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}
2322cint 4951 . . . . . . . . . 10 class ∩ {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}
2420ccnv 5676 . . . . . . . . . 10 class β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)
2523, 24cfv 6544 . . . . . . . . 9 class (β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧})
26 coc 17210 . . . . . . . . . 10 class oc
275, 26cfv 6544 . . . . . . . . 9 class (ocβ€˜π‘˜)
2825, 27cfv 6544 . . . . . . . 8 class ((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))
299, 27cfv 6544 . . . . . . . 8 class ((ocβ€˜π‘˜)β€˜π‘€)
30 cjn 18269 . . . . . . . . 9 class join
315, 30cfv 6544 . . . . . . . 8 class (joinβ€˜π‘˜)
3228, 29, 31co 7412 . . . . . . 7 class (((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))
33 cmee 18270 . . . . . . . 8 class meet
345, 33cfv 6544 . . . . . . 7 class (meetβ€˜π‘˜)
3532, 9, 34co 7412 . . . . . 6 class ((((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))(meetβ€˜π‘˜)𝑀)
3635, 20cfv 6544 . . . . 5 class (((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜((((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))(meetβ€˜π‘˜)𝑀))
378, 13, 36cmpt 5232 . . . 4 class (π‘₯ ∈ 𝒫 ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜((((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))(meetβ€˜π‘˜)𝑀)))
384, 7, 37cmpt 5232 . . 3 class (𝑀 ∈ (LHypβ€˜π‘˜) ↦ (π‘₯ ∈ 𝒫 ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜((((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))(meetβ€˜π‘˜)𝑀))))
392, 3, 38cmpt 5232 . 2 class (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ (π‘₯ ∈ 𝒫 ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜((((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))(meetβ€˜π‘˜)𝑀)))))
401, 39wceq 1540 1 wff ocA = (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ (π‘₯ ∈ 𝒫 ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜((((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))(meetβ€˜π‘˜)𝑀)))))
Colors of variables: wff setvar class
This definition is referenced by:  docaffvalN  40296
  Copyright terms: Public domain W3C validator