Definition df-doch 35655

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 35654	. 2 class ocH
2		vk	. . 3 setvar 𝑘
3		cvv 3173	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1474	. . . . 5 class 𝑘
6		clh 34288	. . . . 5 class LHyp
7	5, 6	cfv 5804	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9	4	cv 1474	. . . . . . . 8 class 𝑤
10		cdvh 35385	. . . . . . . . 9 class DVecH
11	5, 10	cfv 5804	. . . . . . . 8 class (DVecH‘𝑘)
12	9, 11	cfv 5804	. . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13		cbs 15695	. . . . . . 7 class Base
14	12, 13	cfv 5804	. . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
15	14	cpw 4108	. . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
16	8	cv 1474	. . . . . . . . . 10 class 𝑥
17		vy	. . . . . . . . . . . 12 setvar 𝑦
18	17	cv 1474	. . . . . . . . . . 11 class 𝑦
19		cdih 35535	. . . . . . . . . . . . 13 class DIsoH
20	5, 19	cfv 5804	. . . . . . . . . . . 12 class (DIsoH‘𝑘)
21	9, 20	cfv 5804	. . . . . . . . . . 11 class ((DIsoH‘𝑘)‘𝑤)
22	18, 21	cfv 5804	. . . . . . . . . 10 class (((DIsoH‘𝑘)‘𝑤)‘𝑦)
23	16, 22	wss 3540	. . . . . . . . 9 wff 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)
24	5, 13	cfv 5804	. . . . . . . . 9 class (Base‘𝑘)
25	23, 17, 24	crab 2900	. . . . . . . 8 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}
26		cglb 16766	. . . . . . . . 9 class glb
27	5, 26	cfv 5804	. . . . . . . 8 class (glb‘𝑘)
28	25, 27	cfv 5804	. . . . . . 7 class ((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})
29		coc 15776	. . . . . . . 8 class oc
30	5, 29	cfv 5804	. . . . . . 7 class (oc‘𝑘)
31	28, 30	cfv 5804	. . . . . 6 class ((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))
32	31, 21	cfv 5804	. . . . 5 class (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))
33	8, 15, 32	cmpt 4643	. . . 4 class (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))
34	4, 7, 33	cmpt 4643	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))
35	2, 3, 34	cmpt 4643	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
36	1, 35	wceq 1475	1 wff ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))

This definition is referenced by:  dochffval  35656