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

Definition df-djh 35485
Description: Define (closed) subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.)
Assertion
Ref Expression
df-djh joinH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))))))
Distinct variable group:   𝑤,𝑘,𝑥,𝑦

Detailed syntax breakdown of Definition df-djh
StepHypRef Expression
1 cdjh 35484 . 2 class joinH
2 vk . . 3 setvar 𝑘
3 cvv 3172 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1473 . . . . 5 class 𝑘
6 clh 34071 . . . . 5 class LHyp
75, 6cfv 5789 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
9 vy . . . . 5 setvar 𝑦
104cv 1473 . . . . . . . 8 class 𝑤
11 cdvh 35168 . . . . . . . . 9 class DVecH
125, 11cfv 5789 . . . . . . . 8 class (DVecH‘𝑘)
1310, 12cfv 5789 . . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
14 cbs 15643 . . . . . . 7 class Base
1513, 14cfv 5789 . . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
1615cpw 4107 . . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
178cv 1473 . . . . . . . 8 class 𝑥
18 coch 35437 . . . . . . . . . 10 class ocH
195, 18cfv 5789 . . . . . . . . 9 class (ocH‘𝑘)
2010, 19cfv 5789 . . . . . . . 8 class ((ocH‘𝑘)‘𝑤)
2117, 20cfv 5789 . . . . . . 7 class (((ocH‘𝑘)‘𝑤)‘𝑥)
229cv 1473 . . . . . . . 8 class 𝑦
2322, 20cfv 5789 . . . . . . 7 class (((ocH‘𝑘)‘𝑤)‘𝑦)
2421, 23cin 3538 . . . . . 6 class ((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))
2524, 20cfv 5789 . . . . 5 class (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦)))
268, 9, 16, 16, 25cmpt2 6528 . . . 4 class (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))))
274, 7, 26cmpt 4637 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦)))))
282, 3, 27cmpt 4637 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))))))
291, 28wceq 1474 1 wff joinH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))))))
Colors of variables: wff setvar class
This definition is referenced by:  djhffval  35486
  Copyright terms: Public domain W3C validator