Metamath Proof Explorer


Definition df-djaN

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

Ref Expression
Assertion 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 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdjaN
 |-  vA
1 vk
 |-  k
2 cvv
 |-  _V
3 vw
 |-  w
4 clh
 |-  LHyp
5 1 cv
 |-  k
6 5 4 cfv
 |-  ( LHyp ` k )
7 vx
 |-  x
8 cltrn
 |-  LTrn
9 5 8 cfv
 |-  ( LTrn ` k )
10 3 cv
 |-  w
11 10 9 cfv
 |-  ( ( LTrn ` k ) ` w )
12 11 cpw
 |-  ~P ( ( LTrn ` k ) ` w )
13 vy
 |-  y
14 cocaN
 |-  ocA
15 5 14 cfv
 |-  ( ocA ` k )
16 10 15 cfv
 |-  ( ( ocA ` k ) ` w )
17 7 cv
 |-  x
18 17 16 cfv
 |-  ( ( ( ocA ` k ) ` w ) ` x )
19 13 cv
 |-  y
20 19 16 cfv
 |-  ( ( ( ocA ` k ) ` w ) ` y )
21 18 20 cin
 |-  ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) )
22 21 16 cfv
 |-  ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) )
23 7 13 12 12 22 cmpo
 |-  ( 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 ) ) ) )
24 3 6 23 cmpt
 |-  ( 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 ) ) ) ) )
25 1 2 24 cmpt
 |-  ( 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 ) ) ) ) ) )
26 0 25 wceq
 |-  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 ) ) ) ) ) )