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 39586
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 39585 . 2 class ocA
2 vk . . 3 setvar π‘˜
3 cvv 3446 . . 3 class V
4 vw . . . 4 setvar 𝑀
52cv 1541 . . . . 5 class π‘˜
6 clh 38450 . . . . 5 class LHyp
75, 6cfv 6497 . . . 4 class (LHypβ€˜π‘˜)
8 vx . . . . 5 setvar π‘₯
94cv 1541 . . . . . . 7 class 𝑀
10 cltrn 38567 . . . . . . . 8 class LTrn
115, 10cfv 6497 . . . . . . 7 class (LTrnβ€˜π‘˜)
129, 11cfv 6497 . . . . . 6 class ((LTrnβ€˜π‘˜)β€˜π‘€)
1312cpw 4561 . . . . 5 class 𝒫 ((LTrnβ€˜π‘˜)β€˜π‘€)
148cv 1541 . . . . . . . . . . . . 13 class π‘₯
15 vz . . . . . . . . . . . . . 14 setvar 𝑧
1615cv 1541 . . . . . . . . . . . . 13 class 𝑧
1714, 16wss 3911 . . . . . . . . . . . 12 wff π‘₯ βŠ† 𝑧
18 cdia 39494 . . . . . . . . . . . . . . 15 class DIsoA
195, 18cfv 6497 . . . . . . . . . . . . . 14 class (DIsoAβ€˜π‘˜)
209, 19cfv 6497 . . . . . . . . . . . . 13 class ((DIsoAβ€˜π‘˜)β€˜π‘€)
2120crn 5635 . . . . . . . . . . . 12 class ran ((DIsoAβ€˜π‘˜)β€˜π‘€)
2217, 15, 21crab 3408 . . . . . . . . . . 11 class {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}
2322cint 4908 . . . . . . . . . 10 class ∩ {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}
2420ccnv 5633 . . . . . . . . . 10 class β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)
2523, 24cfv 6497 . . . . . . . . 9 class (β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧})
26 coc 17142 . . . . . . . . . 10 class oc
275, 26cfv 6497 . . . . . . . . 9 class (ocβ€˜π‘˜)
2825, 27cfv 6497 . . . . . . . 8 class ((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))
299, 27cfv 6497 . . . . . . . 8 class ((ocβ€˜π‘˜)β€˜π‘€)
30 cjn 18201 . . . . . . . . 9 class join
315, 30cfv 6497 . . . . . . . 8 class (joinβ€˜π‘˜)
3228, 29, 31co 7358 . . . . . . 7 class (((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))
33 cmee 18202 . . . . . . . 8 class meet
345, 33cfv 6497 . . . . . . 7 class (meetβ€˜π‘˜)
3532, 9, 34co 7358 . . . . . 6 class ((((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))(meetβ€˜π‘˜)𝑀)
3635, 20cfv 6497 . . . . 5 class (((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜((((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))(meetβ€˜π‘˜)𝑀))
378, 13, 36cmpt 5189 . . . 4 class (π‘₯ ∈ 𝒫 ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜((((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))(meetβ€˜π‘˜)𝑀)))
384, 7, 37cmpt 5189 . . 3 class (𝑀 ∈ (LHypβ€˜π‘˜) ↦ (π‘₯ ∈ 𝒫 ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜((((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))(meetβ€˜π‘˜)𝑀))))
392, 3, 38cmpt 5189 . 2 class (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ (π‘₯ ∈ 𝒫 ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ (((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜((((ocβ€˜π‘˜)β€˜(β—‘((DIsoAβ€˜π‘˜)β€˜π‘€)β€˜βˆ© {𝑧 ∈ ran ((DIsoAβ€˜π‘˜)β€˜π‘€) ∣ π‘₯ βŠ† 𝑧}))(joinβ€˜π‘˜)((ocβ€˜π‘˜)β€˜π‘€))(meetβ€˜π‘˜)𝑀)))))
401, 39wceq 1542 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  39587
  Copyright terms: Public domain W3C validator