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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdjh 
 |-  joinH
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 cbs 
 |-  Base
9 cdvh 
 |-  DVecH
10 5 9 cfv 
 |-  ( DVecH ` k )
11 3 cv 
 |-  w
12 11 10 cfv 
 |-  ( ( DVecH ` k ) ` w )
13 12 8 cfv 
 |-  ( Base ` ( ( DVecH ` k ) ` w ) )
14 13 cpw 
 |-  ~P ( Base ` ( ( DVecH ` k ) ` w ) )
15 vy 
 |-  y
16 coch 
 |-  ocH
17 5 16 cfv 
 |-  ( ocH ` k )
18 11 17 cfv 
 |-  ( ( ocH ` k ) ` w )
19 7 cv 
 |-  x
20 19 18 cfv 
 |-  ( ( ( ocH ` k ) ` w ) ` x )
21 15 cv 
 |-  y
22 21 18 cfv 
 |-  ( ( ( ocH ` k ) ` w ) ` y )
23 20 22 cin 
 |-  ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) )
24 23 18 cfv 
 |-  ( ( ( ocH ` k ) ` w ) ` ( ( ( ( ocH ` k ) ` w ) ` x ) i^i ( ( ( ocH ` k ) ` w ) ` y ) ) )
25 7 15 14 14 24 cmpo 
 |-  ( 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 ) ) ) )
26 3 6 25 cmpt 
 |-  ( 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 ) ) ) ) )
27 1 2 26 cmpt 
 |-  ( 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 ) ) ) ) ) )
28 0 27 wceq 
 |-  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 ) ) ) ) ) )