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 41123
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 41122 . 2 class ocA
2 vk . . 3 setvar 𝑘
3 cvv 3479 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1538 . . . . 5 class 𝑘
6 clh 39987 . . . . 5 class LHyp
75, 6cfv 6560 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1538 . . . . . . 7 class 𝑤
10 cltrn 40104 . . . . . . . 8 class LTrn
115, 10cfv 6560 . . . . . . 7 class (LTrn‘𝑘)
129, 11cfv 6560 . . . . . 6 class ((LTrn‘𝑘)‘𝑤)
1312cpw 4599 . . . . 5 class 𝒫 ((LTrn‘𝑘)‘𝑤)
148cv 1538 . . . . . . . . . . . . 13 class 𝑥
15 vz . . . . . . . . . . . . . 14 setvar 𝑧
1615cv 1538 . . . . . . . . . . . . 13 class 𝑧
1714, 16wss 3950 . . . . . . . . . . . 12 wff 𝑥𝑧
18 cdia 41031 . . . . . . . . . . . . . . 15 class DIsoA
195, 18cfv 6560 . . . . . . . . . . . . . 14 class (DIsoA‘𝑘)
209, 19cfv 6560 . . . . . . . . . . . . 13 class ((DIsoA‘𝑘)‘𝑤)
2120crn 5685 . . . . . . . . . . . 12 class ran ((DIsoA‘𝑘)‘𝑤)
2217, 15, 21crab 3435 . . . . . . . . . . 11 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}
2322cint 4945 . . . . . . . . . 10 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}
2420ccnv 5683 . . . . . . . . . 10 class ((DIsoA‘𝑘)‘𝑤)
2523, 24cfv 6560 . . . . . . . . 9 class (((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧})
26 coc 17306 . . . . . . . . . 10 class oc
275, 26cfv 6560 . . . . . . . . 9 class (oc‘𝑘)
2825, 27cfv 6560 . . . . . . . 8 class ((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))
299, 27cfv 6560 . . . . . . . 8 class ((oc‘𝑘)‘𝑤)
30 cjn 18358 . . . . . . . . 9 class join
315, 30cfv 6560 . . . . . . . 8 class (join‘𝑘)
3228, 29, 31co 7432 . . . . . . 7 class (((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))
33 cmee 18359 . . . . . . . 8 class meet
345, 33cfv 6560 . . . . . . 7 class (meet‘𝑘)
3532, 9, 34co 7432 . . . . . 6 class ((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)
3635, 20cfv 6560 . . . . 5 class (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))
378, 13, 36cmpt 5224 . . . 4 class (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))
384, 7, 37cmpt 5224 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))))
392, 3, 38cmpt 5224 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(((DIsoA‘𝑘)‘𝑤)‘ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))
401, 39wceq 1539 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  41124
  Copyright terms: Public domain W3C validator