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

Metamath Proof Explorer

Definition df-djaN

Description: Define (closed) subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013)

Ref Expression
Assertion df-djaN vA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑦 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdjaN ⊢ vA
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 vy ⊢ 𝑦
14 cocaN ⊢ ocA
15 5 14 cfv ⊢ ( ocA ‘ 𝑘 )
16 10 15 cfv ⊢ ( ( ocA ‘ 𝑘 ) ‘ 𝑤 )
17 7 cv ⊢ 𝑥
18 17 16 cfv ⊢ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 )
19 13 cv ⊢ 𝑦
20 19 16 cfv ⊢ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 )
21 18 20 cin ⊢ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) )
22 21 16 cfv ⊢ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) )
23 7 13 12 12 22 cmpo ⊢ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑦 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) )
24 3 6 23 cmpt ⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑦 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) )
25 1 2 24 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑦 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) )
26 0 25 wceq ⊢ vA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑦 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) )