Metamath Proof Explorer

Definition df-doch

Description: Define subspace orthocomplement for DVecH 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, 14-Mar-2014)

Ref Expression
Assertion df-doch ocH = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( oc ‘ 𝑘 ) ‘ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 coch ⊢ ocH
1 vk ⊢ 𝑘
2 cvv ⊢ V
3 vw ⊢ 𝑤
4 clh ⊢ LHyp
5 1 cv ⊢ 𝑘
6 5 4 cfv ⊢ ( LHyp ‘ 𝑘 )
7 vx ⊢ 𝑥
8 cbs ⊢ Base
9 cdvh ⊢ DVecH
10 5 9 cfv ⊢ ( DVecH ‘ 𝑘 )
11 3 cv ⊢ 𝑤
12 11 10 cfv ⊢ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 )
13 12 8 cfv ⊢ ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
14 13 cpw ⊢ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
15 cdih ⊢ DIsoH
16 5 15 cfv ⊢ ( DIsoH ‘ 𝑘 )
17 11 16 cfv ⊢ ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 )
18 coc ⊢ oc
19 5 18 cfv ⊢ ( oc ‘ 𝑘 )
20 cglb ⊢ glb
21 5 20 cfv ⊢ ( glb ‘ 𝑘 )
22 vy ⊢ 𝑦
23 5 8 cfv ⊢ ( Base ‘ 𝑘 )
24 7 cv ⊢ 𝑥
25 22 cv ⊢ 𝑦
26 25 17 cfv ⊢ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 )
27 24 26 wss ⊢ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 )
28 27 22 23 crab ⊢ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) }
29 28 21 cfv ⊢ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } )
30 29 19 cfv ⊢ ( ( oc ‘ 𝑘 ) ‘ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) )
31 30 17 cfv ⊢ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( oc ‘ 𝑘 ) ‘ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) )
32 7 14 31 cmpt ⊢ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( oc ‘ 𝑘 ) ‘ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) )
33 3 6 32 cmpt ⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( oc ‘ 𝑘 ) ‘ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) )
34 1 2 33 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( oc ‘ 𝑘 ) ‘ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) )
35 0 34 wceq ⊢ ocH = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( oc ‘ 𝑘 ) ‘ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) )