Definition df-doch 41979

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 41978	. 2 class ocH
2		vk	. . 3 setvar 𝑘
3		cvv 3457	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1562	. . . . 5 class 𝑘
6		clh 40615	. . . . 5 class LHyp
7	5, 6	cfv 6525	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9	4	cv 1562	. . . . . . . 8 class 𝑤
10		cdvh 41709	. . . . . . . . 9 class DVecH
11	5, 10	cfv 6525	. . . . . . . 8 class (DVecH‘𝑘)
12	9, 11	cfv 6525	. . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13		cbs 17257	. . . . . . 7 class Base
14	12, 13	cfv 6525	. . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
15	14	cpw 4558	. . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
16	8	cv 1562	. . . . . . . . . 10 class 𝑥
17		vy	. . . . . . . . . . . 12 setvar 𝑦
18	17	cv 1562	. . . . . . . . . . 11 class 𝑦
19		cdih 41859	. . . . . . . . . . . . 13 class DIsoH
20	5, 19	cfv 6525	. . . . . . . . . . . 12 class (DIsoH‘𝑘)
21	9, 20	cfv 6525	. . . . . . . . . . 11 class ((DIsoH‘𝑘)‘𝑤)
22	18, 21	cfv 6525	. . . . . . . . . 10 class (((DIsoH‘𝑘)‘𝑤)‘𝑦)
23	16, 22	wss 3907	. . . . . . . . 9 wff 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)
24	5, 13	cfv 6525	. . . . . . . . 9 class (Base‘𝑘)
25	23, 17, 24	crab 3417	. . . . . . . 8 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}
26		cglb 18354	. . . . . . . . 9 class glb
27	5, 26	cfv 6525	. . . . . . . 8 class (glb‘𝑘)
28	25, 27	cfv 6525	. . . . . . 7 class ((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})
29		coc 17306	. . . . . . . 8 class oc
30	5, 29	cfv 6525	. . . . . . 7 class (oc‘𝑘)
31	28, 30	cfv 6525	. . . . . 6 class ((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))
32	31, 21	cfv 6525	. . . . 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 1563	1 wff ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))

This definition is referenced by:  dochffval  41980