Definition df-djh 41397

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 41396	. 2 class joinH
2		vk	. . 3 setvar 𝑘
3		cvv 3480	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1539	. . . . 5 class 𝑘
6		clh 39986	. . . . 5 class LHyp
7	5, 6	cfv 6561	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9		vy	. . . . 5 setvar 𝑦
10	4	cv 1539	. . . . . . . 8 class 𝑤
11		cdvh 41080	. . . . . . . . 9 class DVecH
12	5, 11	cfv 6561	. . . . . . . 8 class (DVecH‘𝑘)
13	10, 12	cfv 6561	. . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
14		cbs 17247	. . . . . . 7 class Base
15	13, 14	cfv 6561	. . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
16	15	cpw 4600	. . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
17	8	cv 1539	. . . . . . . 8 class 𝑥
18		coch 41349	. . . . . . . . . 10 class ocH
19	5, 18	cfv 6561	. . . . . . . . 9 class (ocH‘𝑘)
20	10, 19	cfv 6561	. . . . . . . 8 class ((ocH‘𝑘)‘𝑤)
21	17, 20	cfv 6561	. . . . . . 7 class (((ocH‘𝑘)‘𝑤)‘𝑥)
22	9	cv 1539	. . . . . . . 8 class 𝑦
23	22, 20	cfv 6561	. . . . . . 7 class (((ocH‘𝑘)‘𝑤)‘𝑦)
24	21, 23	cin 3950	. . . . . 6 class ((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))
25	24, 20	cfv 6561	. . . . 5 class (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦)))
26	8, 9, 16, 16, 25	cmpo 7433	. . . 4 class (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))))
27	4, 7, 26	cmpt 5225	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦)))))
28	2, 3, 27	cmpt 5225	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))))))
29	1, 28	wceq 1540	1 wff joinH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦))))))

This definition is referenced by:  djhffval  41398