Definition df-djaN 36421

Description: Define (closed) subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.)

Assertion

Ref	Expression
df-djaN	|- vA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) , y e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) ) ) )

Distinct variable group:   w, k, x, y

Detailed syntax breakdown of Definition df-djaN

Step	Hyp	Ref	Expression
1		cdjaN 36420	. 2 class vA
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	. . . . . . 7 class w
11		cltrn 35387	. . . . . . . 8 class LTrn
12	5, 11	cfv 5888	. . . . . . 7 class ( LTrn ` k )
13	10, 12	cfv 5888	. . . . . 6 class ( ( LTrn ` k ) ` w )
14	13	cpw 4158	. . . . 5 class ~P ( ( LTrn ` k ) ` w )
15	8	cv 1482	. . . . . . . 8 class x
16		cocaN 36408	. . . . . . . . . 10 class ocA
17	5, 16	cfv 5888	. . . . . . . . 9 class ( ocA ` k )
18	10, 17	cfv 5888	. . . . . . . 8 class ( ( ocA ` k ) ` w )
19	15, 18	cfv 5888	. . . . . . 7 class ( ( ( ocA ` k ) ` w ) ` x )
20	9	cv 1482	. . . . . . . 8 class y
21	20, 18	cfv 5888	. . . . . . 7 class ( ( ( ocA ` k ) ` w ) ` y )
22	19, 21	cin 3573	. . . . . 6 class ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) )
23	22, 18	cfv 5888	. . . . 5 class ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) )
24	8, 9, 14, 14, 23	cmpt2 6652	. . . 4 class ( x e. ~P ( ( LTrn ` k ) ` w ) , y e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) )
25	4, 7, 24	cmpt 4729	. . 3 class ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) , y e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) ) )
26	2, 3, 25	cmpt 4729	. 2 class ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) , y e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) ) ) )
27	1, 26	wceq 1483	1 wff vA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) , y e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) ) ) )

This definition is referenced by:  djaffvalN  36422