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 37141
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 37140 . 2 class ocA
2 vk . . 3 setvar 𝑘
3 cvv 3385 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1652 . . . . 5 class 𝑘
6 clh 36005 . . . . 5 class LHyp
75, 6cfv 6101 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1652 . . . . . . 7 class 𝑤
10 cltrn 36122 . . . . . . . 8 class LTrn
115, 10cfv 6101 . . . . . . 7 class (LTrn‘𝑘)
129, 11cfv 6101 . . . . . 6 class ((LTrn‘𝑘)‘𝑤)
1312cpw 4349 . . . . 5 class 𝒫 ((LTrn‘𝑘)‘𝑤)
148cv 1652 . . . . . . . . . . . . 13 class 𝑥
15 vz . . . . . . . . . . . . . 14 setvar 𝑧
1615cv 1652 . . . . . . . . . . . . 13 class 𝑧
1714, 16wss 3769 . . . . . . . . . . . 12 wff 𝑥𝑧
18 cdia 37049 . . . . . . . . . . . . . . 15 class DIsoA
195, 18cfv 6101 . . . . . . . . . . . . . 14 class (DIsoA‘𝑘)
209, 19cfv 6101 . . . . . . . . . . . . 13 class ((DIsoA‘𝑘)‘𝑤)
2120crn 5313 . . . . . . . . . . . 12 class ran ((DIsoA‘𝑘)‘𝑤)
2217, 15, 21crab 3093 . . . . . . . . . . 11 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}
2322cint 4667 . . . . . . . . . 10 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}
2420ccnv 5311 . . . . . . . . . 10 class ((DIsoA‘𝑘)‘𝑤)
2523, 24cfv 6101 . . . . . . . . 9 class (((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧})
26 coc 16275 . . . . . . . . . 10 class oc
275, 26cfv 6101 . . . . . . . . 9 class (oc‘𝑘)
2825, 27cfv 6101 . . . . . . . 8 class ((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))
299, 27cfv 6101 . . . . . . . 8 class ((oc‘𝑘)‘𝑤)
30 cjn 17259 . . . . . . . . 9 class join
315, 30cfv 6101 . . . . . . . 8 class (join‘𝑘)
3228, 29, 31co 6878 . . . . . . 7 class (((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))
33 cmee 17260 . . . . . . . 8 class meet
345, 33cfv 6101 . . . . . . 7 class (meet‘𝑘)
3532, 9, 34co 6878 . . . . . 6 class ((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)
3635, 20cfv 6101 . . . . 5 class (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))
378, 13, 36cmpt 4922 . . . 4 class (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))
384, 7, 37cmpt 4922 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))))
392, 3, 38cmpt 4922 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))
401, 39wceq 1653 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  37142
  Copyright terms: Public domain W3C validator