Metamath Proof Explorer

Definition df-djh

Description: Define (closed) subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014)

Ref Expression
Assertion df-djh ⊢joinH=k∈V⟼w∈LHyp⁡k⟼x∈𝒫BaseDVecH⁡k⁡w,y∈𝒫BaseDVecH⁡k⁡w⟼ocH⁡k⁡w⁡ocH⁡k⁡w⁡x∩ocH⁡k⁡w⁡y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdjh classjoinH
1 vk setvark
2 cvv classV
3 vw setvarw
4 clh classLHyp
5 1 cv setvark
6 5 4 cfv classLHyp⁡k
7 vx setvarx
8 cbs classBase
9 cdvh classDVecH
10 5 9 cfv classDVecH⁡k
11 3 cv setvarw
12 11 10 cfv classDVecH⁡k⁡w
13 12 8 cfv classBaseDVecH⁡k⁡w
14 13 cpw class𝒫BaseDVecH⁡k⁡w
15 vy setvary
16 coch classocH
17 5 16 cfv classocH⁡k
18 11 17 cfv classocH⁡k⁡w
19 7 cv setvarx
20 19 18 cfv classocH⁡k⁡w⁡x
21 15 cv setvary
22 21 18 cfv classocH⁡k⁡w⁡y
23 20 22 cin classocH⁡k⁡w⁡x∩ocH⁡k⁡w⁡y
24 23 18 cfv classocH⁡k⁡w⁡ocH⁡k⁡w⁡x∩ocH⁡k⁡w⁡y
25 7 15 14 14 24 cmpo classx∈𝒫BaseDVecH⁡k⁡w,y∈𝒫BaseDVecH⁡k⁡w⟼ocH⁡k⁡w⁡ocH⁡k⁡w⁡x∩ocH⁡k⁡w⁡y
26 3 6 25 cmpt classw∈LHyp⁡k⟼x∈𝒫BaseDVecH⁡k⁡w,y∈𝒫BaseDVecH⁡k⁡w⟼ocH⁡k⁡w⁡ocH⁡k⁡w⁡x∩ocH⁡k⁡w⁡y
27 1 2 26 cmpt classk∈V⟼w∈LHyp⁡k⟼x∈𝒫BaseDVecH⁡k⁡w,y∈𝒫BaseDVecH⁡k⁡w⟼ocH⁡k⁡w⁡ocH⁡k⁡w⁡x∩ocH⁡k⁡w⁡y
28 0 27 wceq wffjoinH=k∈V⟼w∈LHyp⁡k⟼x∈𝒫BaseDVecH⁡k⁡w,y∈𝒫BaseDVecH⁡k⁡w⟼ocH⁡k⁡w⁡ocH⁡k⁡w⁡x∩ocH⁡k⁡w⁡y