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