Definition df-djaN 41093

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

Assertion

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

Distinct variable group:   𝑤,𝑘,𝑥,𝑦

Detailed syntax breakdown of Definition df-djaN

Step	Hyp	Ref	Expression
1		cdjaN 41092	. 2 class vA
2		vk	. . 3 setvar 𝑘
3		cvv 3463	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1538	. . . . 5 class 𝑘
6		clh 39945	. . . . 5 class LHyp
7	5, 6	cfv 6541	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9		vy	. . . . 5 setvar 𝑦
10	4	cv 1538	. . . . . . 7 class 𝑤
11		cltrn 40062	. . . . . . . 8 class LTrn
12	5, 11	cfv 6541	. . . . . . 7 class (LTrn‘𝑘)
13	10, 12	cfv 6541	. . . . . 6 class ((LTrn‘𝑘)‘𝑤)
14	13	cpw 4580	. . . . 5 class 𝒫 ((LTrn‘𝑘)‘𝑤)
15	8	cv 1538	. . . . . . . 8 class 𝑥
16		cocaN 41080	. . . . . . . . . 10 class ocA
17	5, 16	cfv 6541	. . . . . . . . 9 class (ocA‘𝑘)
18	10, 17	cfv 6541	. . . . . . . 8 class ((ocA‘𝑘)‘𝑤)
19	15, 18	cfv 6541	. . . . . . 7 class (((ocA‘𝑘)‘𝑤)‘𝑥)
20	9	cv 1538	. . . . . . . 8 class 𝑦
21	20, 18	cfv 6541	. . . . . . 7 class (((ocA‘𝑘)‘𝑤)‘𝑦)
22	19, 21	cin 3930	. . . . . 6 class ((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦))
23	22, 18	cfv 6541	. . . . 5 class (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦)))
24	8, 9, 14, 14, 23	cmpo 7415	. . . 4 class (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦))))
25	4, 7, 24	cmpt 5205	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦)))))
26	2, 3, 25	cmpt 5205	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦))))))
27	1, 26	wceq 1539	1 wff vA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦))))))

This definition is referenced by:  djaffvalN  41094