Definition df-doch 42498

Description: Define subspace orthocomplement for DVecH vector space. Temporarily, we are using the range of the isomorphism instead of the set of closed subspaces. Later, when inner product is introduced, we will show that these are the same. (Contributed by NM, 14-Mar-2014.)

Assertion

Ref	Expression
df-doch	⊢ ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))

Distinct variable group:   𝑤,𝑘,𝑥,𝑦

Detailed syntax breakdown of Definition df-doch

Step	Hyp	Ref	Expression
1		coch 42497	. 2 class ocH
2		vk	. . 3 setvar 𝑘
3		cvv 3450	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1568	. . . . 5 class 𝑘
6		clh 41134	. . . . 5 class LHyp
7	5, 6	cfv 6538	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9	4	cv 1568	. . . . . . . 8 class 𝑤
10		cdvh 42228	. . . . . . . . 9 class DVecH
11	5, 10	cfv 6538	. . . . . . . 8 class (DVecH‘𝑘)
12	9, 11	cfv 6538	. . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13		cbs 17392	. . . . . . 7 class Base
14	12, 13	cfv 6538	. . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
15	14	cpw 4556	. . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
16	8	cv 1568	. . . . . . . . . 10 class 𝑥
17		vy	. . . . . . . . . . . 12 setvar 𝑦
18	17	cv 1568	. . . . . . . . . . 11 class 𝑦
19		cdih 42378	. . . . . . . . . . . . 13 class DIsoH
20	5, 19	cfv 6538	. . . . . . . . . . . 12 class (DIsoH‘𝑘)
21	9, 20	cfv 6538	. . . . . . . . . . 11 class ((DIsoH‘𝑘)‘𝑤)
22	18, 21	cfv 6538	. . . . . . . . . 10 class (((DIsoH‘𝑘)‘𝑤)‘𝑦)
23	16, 22	wss 3895	. . . . . . . . 9 wff 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)
24	5, 13	cfv 6538	. . . . . . . . 9 class (Base‘𝑘)
25	23, 17, 24	crab 3412	. . . . . . . 8 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}
26		cglb 18489	. . . . . . . . 9 class glb
27	5, 26	cfv 6538	. . . . . . . 8 class (glb‘𝑘)
28	25, 27	cfv 6538	. . . . . . 7 class ((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})
29		coc 17441	. . . . . . . 8 class oc
30	5, 29	cfv 6538	. . . . . . 7 class (oc‘𝑘)
31	28, 30	cfv 6538	. . . . . 6 class ((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))
32	31, 21	cfv 6538	. . . . 5 class (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))
33	8, 15, 32	cmpt 5185	. . . 4 class (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))
34	4, 7, 33	cmpt 5185	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))
35	2, 3, 34	cmpt 5185	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
36	1, 35	wceq 1569	1 wff ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))

This definition is used by:  dochffval  42499