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 𝒫 Base DVecH k w , y 𝒫 Base DVecH k w ocH k w ocH k w x ocH k w y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdjh class joinH
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp k
7 vx setvar x
8 cbs class Base
9 cdvh class DVecH
10 5 9 cfv class DVecH k
11 3 cv setvar w
12 11 10 cfv class DVecH k w
13 12 8 cfv class Base DVecH k w
14 13 cpw class 𝒫 Base DVecH k w
15 vy setvar y
16 coch class ocH
17 5 16 cfv class ocH k
18 11 17 cfv class ocH k w
19 7 cv setvar x
20 19 18 cfv class ocH k w x
21 15 cv setvar y
22 21 18 cfv class ocH k w y
23 20 22 cin class ocH k w x ocH k w y
24 23 18 cfv class ocH k w ocH k w x ocH k w y
25 7 15 14 14 24 cmpo class x 𝒫 Base DVecH k w , y 𝒫 Base DVecH k w ocH k w ocH k w x ocH k w y
26 3 6 25 cmpt class w LHyp k x 𝒫 Base DVecH k w , y 𝒫 Base DVecH k w ocH k w ocH k w x ocH k w y
27 1 2 26 cmpt class k V w LHyp k x 𝒫 Base DVecH k w , y 𝒫 Base DVecH k w ocH k w ocH k w x ocH k w y
28 0 27 wceq wff joinH = k V w LHyp k x 𝒫 Base DVecH k w , y 𝒫 Base DVecH k w ocH k w ocH k w x ocH k w y