This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) ) ) ) )