Definition df-djh 36684

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

Assertion

Ref	Expression
df-djh	|- joinH = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( ( ( ocH ` k ) ` w ) ` ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) ) ) ) ) )

Distinct variable group:   w, k, x, y

Detailed syntax breakdown of Definition df-djh

Step	Hyp	Ref	Expression
1		cdjh 36683	. 2 class joinH
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vw	. . . 4 setvar w
5	2	cv 1482	. . . . 5 class k
6		clh 35270	. . . . 5 class LHyp
7	5, 6	cfv 5888	. . . 4 class ( LHyp ` k )
8		vx	. . . . 5 setvar x
9		vy	. . . . 5 setvar y
10	4	cv 1482	. . . . . . . 8 class w
11		cdvh 36367	. . . . . . . . 9 class DVecH
12	5, 11	cfv 5888	. . . . . . . 8 class ( DVecH ` k )
13	10, 12	cfv 5888	. . . . . . 7 class ( ( DVecH ` k ) ` w )
14		cbs 15857	. . . . . . 7 class Base
15	13, 14	cfv 5888	. . . . . 6 class ( Base ` ( ( DVecH ` k ) ` w ) )
16	15	cpw 4158	. . . . 5 class ~P ( Base ` ( ( DVecH ` k ) ` w ) )
17	8	cv 1482	. . . . . . . 8 class x
18		coch 36636	. . . . . . . . . 10 class ocH
19	5, 18	cfv 5888	. . . . . . . . 9 class ( ocH ` k )
20	10, 19	cfv 5888	. . . . . . . 8 class ( ( ocH ` k ) ` w )
21	17, 20	cfv 5888	. . . . . . 7 class ( ( ( ocH ` k ) ` w ) ` x )
22	9	cv 1482	. . . . . . . 8 class y
23	22, 20	cfv 5888	. . . . . . 7 class ( ( ( ocH ` k ) ` w ) ` y )
24	21, 23	cin 3573	. . . . . 6 class ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) )
25	24, 20	cfv 5888	. . . . 5 class ( ( ( ocH ` k ) ` w ) ` ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) ) )
26	8, 9, 16, 16, 25	cmpt2 6652	. . . 4 class ( x e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( ( ( ocH ` k ) ` w ) ` ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) ) ) )
27	4, 7, 26	cmpt 4729	. . 3 class ( w e. ( LHyp ` k ) |-> ( x e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( ( ( ocH ` k ) ` w ) ` ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) ) ) ) )
28	2, 3, 27	cmpt 4729	. 2 class ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( ( ( ocH ` k ) ` w ) ` ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) ) ) ) ) )
29	1, 28	wceq 1483	1 wff joinH = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) , y e. ~P ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( ( ( ocH ` k ) ` w ) ` ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) ) ) ) ) )

This definition is referenced by:  djhffval  36685