Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-djaN Structured version   Visualization version   GIF version

Definition df-djaN 37153
Description: Define (closed) subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.)
Assertion
Ref Expression
df-djaN vA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦))))))
Distinct variable group:   𝑤,𝑘,𝑥,𝑦

Detailed syntax breakdown of Definition df-djaN
StepHypRef Expression
1 cdjaN 37152 . 2 class vA
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 𝑥
9 vy . . . . 5 setvar 𝑦
104cv 1652 . . . . . . 7 class 𝑤
11 cltrn 36122 . . . . . . . 8 class LTrn
125, 11cfv 6101 . . . . . . 7 class (LTrn‘𝑘)
1310, 12cfv 6101 . . . . . 6 class ((LTrn‘𝑘)‘𝑤)
1413cpw 4349 . . . . 5 class 𝒫 ((LTrn‘𝑘)‘𝑤)
158cv 1652 . . . . . . . 8 class 𝑥
16 cocaN 37140 . . . . . . . . . 10 class ocA
175, 16cfv 6101 . . . . . . . . 9 class (ocA‘𝑘)
1810, 17cfv 6101 . . . . . . . 8 class ((ocA‘𝑘)‘𝑤)
1915, 18cfv 6101 . . . . . . 7 class (((ocA‘𝑘)‘𝑤)‘𝑥)
209cv 1652 . . . . . . . 8 class 𝑦
2120, 18cfv 6101 . . . . . . 7 class (((ocA‘𝑘)‘𝑤)‘𝑦)
2219, 21cin 3768 . . . . . 6 class ((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦))
2322, 18cfv 6101 . . . . 5 class (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦)))
248, 9, 14, 14, 23cmpt2 6880 . . . 4 class (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦))))
254, 7, 24cmpt 4922 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦)))))
262, 3, 25cmpt 4922 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦))))))
271, 26wceq 1653 1 wff vA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦))))))
Colors of variables: wff setvar class
This definition is referenced by:  djaffvalN  37154
  Copyright terms: Public domain W3C validator