Definition df-djh 40255

Description: Define (closed) subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.)

Assertion

Ref	Expression
df-djh	⊢ joinH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))))))

Distinct variable group:   𝑤,𝑘,𝑥,𝑦

Detailed syntax breakdown of Definition df-djh

Step	Hyp	Ref	Expression
1		cdjh 40254	. 2 class joinH
2		vk	. . 3 setvar 𝑘
3		cvv 3475	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1541	. . . . 5 class 𝑘
6		clh 38844	. . . . 5 class LHyp
7	5, 6	cfv 6541	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9		vy	. . . . 5 setvar 𝑦
10	4	cv 1541	. . . . . . . 8 class 𝑤
11		cdvh 39938	. . . . . . . . 9 class DVecH
12	5, 11	cfv 6541	. . . . . . . 8 class (DVecH‘𝑘)
13	10, 12	cfv 6541	. . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
14		cbs 17141	. . . . . . 7 class Base
15	13, 14	cfv 6541	. . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
16	15	cpw 4602	. . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
17	8	cv 1541	. . . . . . . 8 class 𝑥
18		coch 40207	. . . . . . . . . 10 class ocH
19	5, 18	cfv 6541	. . . . . . . . 9 class (ocH‘𝑘)
20	10, 19	cfv 6541	. . . . . . . 8 class ((ocH‘𝑘)‘𝑤)
21	17, 20	cfv 6541	. . . . . . 7 class (((ocH‘𝑘)‘𝑤)‘𝑥)
22	9	cv 1541	. . . . . . . 8 class 𝑦
23	22, 20	cfv 6541	. . . . . . 7 class (((ocH‘𝑘)‘𝑤)‘𝑦)
24	21, 23	cin 3947	. . . . . 6 class ((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))
25	24, 20	cfv 6541	. . . . 5 class (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦)))
26	8, 9, 16, 16, 25	cmpo 7408	. . . 4 class (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))))
27	4, 7, 26	cmpt 5231	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦)))))
28	2, 3, 27	cmpt 5231	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))))))
29	1, 28	wceq 1542	1 wff joinH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))))))

This definition is referenced by:  djhffval  40256