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

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 = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑦 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdjh ⊢ joinH
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 vy ⊢ 𝑦
16 coch ⊢ ocH
17 5 16 cfv ⊢ ( ocH ‘ 𝑘 )
18 11 17 cfv ⊢ ( ( ocH ‘ 𝑘 ) ‘ 𝑤 )
19 7 cv ⊢ 𝑥
20 19 18 cfv ⊢ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 )
21 15 cv ⊢ 𝑦
22 21 18 cfv ⊢ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 )
23 20 22 cin ⊢ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) )
24 23 18 cfv ⊢ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) )
25 7 15 14 14 24 cmpo ⊢ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑦 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) )
26 3 6 25 cmpt ⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑦 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) )
27 1 2 26 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑦 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) )
28 0 27 wceq ⊢ joinH = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑦 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) )