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 ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) )