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 = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cocaN ocA
1 vk 𝑘
2 cvv V
3 vw 𝑤
4 clh LHyp
5 1 cv 𝑘
6 5 4 cfv ( LHyp ‘ 𝑘 )
7 vx 𝑥
8 cltrn LTrn
9 5 8 cfv ( LTrn ‘ 𝑘 )
10 3 cv 𝑤
11 10 9 cfv ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
12 11 cpw 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
13 cdia DIsoA
14 5 13 cfv ( DIsoA ‘ 𝑘 )
15 10 14 cfv ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 )
16 coc oc
17 5 16 cfv ( oc ‘ 𝑘 )
18 15 ccnv ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 )
19 vz 𝑧
20 15 crn ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 )
21 7 cv 𝑥
22 19 cv 𝑧
23 21 22 wss 𝑥𝑧
24 23 19 20 crab { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥𝑧 }
25 24 cint { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥𝑧 }
26 25 18 cfv ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } )
27 26 17 cfv ( ( oc ‘ 𝑘 ) ‘ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) )
28 cjn join
29 5 28 cfv ( join ‘ 𝑘 )
30 10 17 cfv ( ( oc ‘ 𝑘 ) ‘ 𝑤 )
31 27 30 29 co ( ( ( oc ‘ 𝑘 ) ‘ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) )
32 cmee meet
33 5 32 cfv ( meet ‘ 𝑘 )
34 31 10 33 co ( ( ( ( oc ‘ 𝑘 ) ‘ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 )
35 34 15 cfv ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) )
36 7 12 35 cmpt ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) )
37 3 6 36 cmpt ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) )
38 1 2 37 cmpt ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) )
39 0 38 wceq ocA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) )