Definition df-doch 42229

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 42228	. 2 class ocH
2		vk	. . 3 setvar 𝑘
3		cvv 3453	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1569	. . . . 5 class 𝑘
6		clh 40865	. . . . 5 class LHyp
7	5, 6	cfv 6537	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9	4	cv 1569	. . . . . . . 8 class 𝑤
10		cdvh 41959	. . . . . . . . 9 class DVecH
11	5, 10	cfv 6537	. . . . . . . 8 class (DVecH‘𝑘)
12	9, 11	cfv 6537	. . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13		cbs 17307	. . . . . . 7 class Base
14	12, 13	cfv 6537	. . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
15	14	cpw 4560	. . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
16	8	cv 1569	. . . . . . . . . 10 class 𝑥
17		vy	. . . . . . . . . . . 12 setvar 𝑦
18	17	cv 1569	. . . . . . . . . . 11 class 𝑦
19		cdih 42109	. . . . . . . . . . . . 13 class DIsoH
20	5, 19	cfv 6537	. . . . . . . . . . . 12 class (DIsoH‘𝑘)
21	9, 20	cfv 6537	. . . . . . . . . . 11 class ((DIsoH‘𝑘)‘𝑤)
22	18, 21	cfv 6537	. . . . . . . . . 10 class (((DIsoH‘𝑘)‘𝑤)‘𝑦)
23	16, 22	wss 3902	. . . . . . . . 9 wff 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)
24	5, 13	cfv 6537	. . . . . . . . 9 class (Base‘𝑘)
25	23, 17, 24	crab 3414	. . . . . . . 8 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}
26		cglb 18404	. . . . . . . . 9 class glb
27	5, 26	cfv 6537	. . . . . . . 8 class (glb‘𝑘)
28	25, 27	cfv 6537	. . . . . . 7 class ((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})
29		coc 17356	. . . . . . . 8 class oc
30	5, 29	cfv 6537	. . . . . . 7 class (oc‘𝑘)
31	28, 30	cfv 6537	. . . . . 6 class ((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))
32	31, 21	cfv 6537	. . . . 5 class (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))
33	8, 15, 32	cmpt 5190	. . . 4 class (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))
34	4, 7, 33	cmpt 5190	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))
35	2, 3, 34	cmpt 5190	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))
36	1, 35	wceq 1570	1 wff ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))))

This definition is used by:  dochffval  42230