Metamath Proof Explorer

Definition df-docaN

Description: Define subspace orthocomplement for DVecA partial vector space. Temporarily, we are using the range of the isomorphism instead of the set of closed subspaces. Later, when inner product is introduced, we will show that these are the same. (Contributed by NM, 6-Dec-2013)

Ref Expression
Assertion df-docaN 
|- ocA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( DIsoA ` k ) ` w ) ` ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cocaN 
 |-  ocA
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 cdia 
 |-  DIsoA
14 5 13 cfv 
 |-  ( DIsoA ` k )
15 10 14 cfv 
 |-  ( ( DIsoA ` k ) ` w )
16 coc 
 |-  oc
17 5 16 cfv 
 |-  ( oc ` k )
18 15 ccnv 
 |-  `' ( ( DIsoA ` k ) ` w )
19 vz 
 |-  z
20 15 crn 
 |-  ran ( ( DIsoA ` k ) ` w )
21 7 cv 
 |-  x
22 19 cv 
 |-  z
23 21 22 wss 
 |-  x C_ z
24 23 19 20 crab 
 |-  { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z }
25 24 cint 
 |-  |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z }
26 25 18 cfv 
 |-  ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } )
27 26 17 cfv 
 |-  ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) )
28 cjn 
 |-  join
29 5 28 cfv 
 |-  ( join ` k )
30 10 17 cfv 
 |-  ( ( oc ` k ) ` w )
31 27 30 29 co 
 |-  ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) )
32 cmee 
 |-  meet
33 5 32 cfv 
 |-  ( meet ` k )
34 31 10 33 co 
 |-  ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w )
35 34 15 cfv 
 |-  ( ( ( DIsoA ` k ) ` w ) ` ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w ) )
36 7 12 35 cmpt 
 |-  ( x e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( DIsoA ` k ) ` w ) ` ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w ) ) )
37 3 6 36 cmpt 
 |-  ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( DIsoA ` k ) ` w ) ` ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w ) ) ) )
38 1 2 37 cmpt 
 |-  ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( DIsoA ` k ) ` w ) ` ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w ) ) ) ) )
39 0 38 wceq 
 |-  ocA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( DIsoA ` k ) ` w ) ` ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w ) ) ) ) )