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 38123
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 38122 . 2 class ocA
2 vk . . 3 setvar 𝑘
3 cvv 3500 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1529 . . . . 5 class 𝑘
6 clh 36987 . . . . 5 class LHyp
75, 6cfv 6352 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1529 . . . . . . 7 class 𝑤
10 cltrn 37104 . . . . . . . 8 class LTrn
115, 10cfv 6352 . . . . . . 7 class (LTrn‘𝑘)
129, 11cfv 6352 . . . . . 6 class ((LTrn‘𝑘)‘𝑤)
1312cpw 4542 . . . . 5 class 𝒫 ((LTrn‘𝑘)‘𝑤)
148cv 1529 . . . . . . . . . . . . 13 class 𝑥
15 vz . . . . . . . . . . . . . 14 setvar 𝑧
1615cv 1529 . . . . . . . . . . . . 13 class 𝑧
1714, 16wss 3940 . . . . . . . . . . . 12 wff 𝑥𝑧
18 cdia 38031 . . . . . . . . . . . . . . 15 class DIsoA
195, 18cfv 6352 . . . . . . . . . . . . . 14 class (DIsoA‘𝑘)
209, 19cfv 6352 . . . . . . . . . . . . 13 class ((DIsoA‘𝑘)‘𝑤)
2120crn 5555 . . . . . . . . . . . 12 class ran ((DIsoA‘𝑘)‘𝑤)
2217, 15, 21crab 3147 . . . . . . . . . . 11 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}
2322cint 4874 . . . . . . . . . 10 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}
2420ccnv 5553 . . . . . . . . . 10 class ((DIsoA‘𝑘)‘𝑤)
2523, 24cfv 6352 . . . . . . . . 9 class (((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧})
26 coc 16563 . . . . . . . . . 10 class oc
275, 26cfv 6352 . . . . . . . . 9 class (oc‘𝑘)
2825, 27cfv 6352 . . . . . . . 8 class ((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))
299, 27cfv 6352 . . . . . . . 8 class ((oc‘𝑘)‘𝑤)
30 cjn 17544 . . . . . . . . 9 class join
315, 30cfv 6352 . . . . . . . 8 class (join‘𝑘)
3228, 29, 31co 7148 . . . . . . 7 class (((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))
33 cmee 17545 . . . . . . . 8 class meet
345, 33cfv 6352 . . . . . . 7 class (meet‘𝑘)
3532, 9, 34co 7148 . . . . . 6 class ((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)
3635, 20cfv 6352 . . . . 5 class (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))
378, 13, 36cmpt 5143 . . . 4 class (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))
384, 7, 37cmpt 5143 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))))
392, 3, 38cmpt 5143 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))
401, 39wceq 1530 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  38124
  Copyright terms: Public domain W3C validator