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 36923
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 36922 . 2 class ocA
2 vk . . 3 setvar 𝑘
3 cvv 3349 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1629 . . . . 5 class 𝑘
6 clh 35785 . . . . 5 class LHyp
75, 6cfv 6031 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1629 . . . . . . 7 class 𝑤
10 cltrn 35902 . . . . . . . 8 class LTrn
115, 10cfv 6031 . . . . . . 7 class (LTrn‘𝑘)
129, 11cfv 6031 . . . . . 6 class ((LTrn‘𝑘)‘𝑤)
1312cpw 4295 . . . . 5 class 𝒫 ((LTrn‘𝑘)‘𝑤)
148cv 1629 . . . . . . . . . . . . 13 class 𝑥
15 vz . . . . . . . . . . . . . 14 setvar 𝑧
1615cv 1629 . . . . . . . . . . . . 13 class 𝑧
1714, 16wss 3721 . . . . . . . . . . . 12 wff 𝑥𝑧
18 cdia 36831 . . . . . . . . . . . . . . 15 class DIsoA
195, 18cfv 6031 . . . . . . . . . . . . . 14 class (DIsoA‘𝑘)
209, 19cfv 6031 . . . . . . . . . . . . 13 class ((DIsoA‘𝑘)‘𝑤)
2120crn 5250 . . . . . . . . . . . 12 class ran ((DIsoA‘𝑘)‘𝑤)
2217, 15, 21crab 3064 . . . . . . . . . . 11 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}
2322cint 4609 . . . . . . . . . 10 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}
2420ccnv 5248 . . . . . . . . . 10 class ((DIsoA‘𝑘)‘𝑤)
2523, 24cfv 6031 . . . . . . . . 9 class (((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧})
26 coc 16156 . . . . . . . . . 10 class oc
275, 26cfv 6031 . . . . . . . . 9 class (oc‘𝑘)
2825, 27cfv 6031 . . . . . . . 8 class ((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))
299, 27cfv 6031 . . . . . . . 8 class ((oc‘𝑘)‘𝑤)
30 cjn 17151 . . . . . . . . 9 class join
315, 30cfv 6031 . . . . . . . 8 class (join‘𝑘)
3228, 29, 31co 6792 . . . . . . 7 class (((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))
33 cmee 17152 . . . . . . . 8 class meet
345, 33cfv 6031 . . . . . . 7 class (meet‘𝑘)
3532, 9, 34co 6792 . . . . . 6 class ((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)
3635, 20cfv 6031 . . . . 5 class (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))
378, 13, 36cmpt 4861 . . . 4 class (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))
384, 7, 37cmpt 4861 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))))
392, 3, 38cmpt 4861 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))
401, 39wceq 1630 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  36924
  Copyright terms: Public domain W3C validator