Definition df-doch 42163

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 42162	. 2 class ocH
2		vk	. . 3 setvar 𝑘
3		cvv 3458	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1569	. . . . 5 class 𝑘
6		clh 40799	. . . . 5 class LHyp
7	5, 6	cfv 6543	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9	4	cv 1569	. . . . . . . 8 class 𝑤
10		cdvh 41893	. . . . . . . . 9 class DVecH
11	5, 10	cfv 6543	. . . . . . . 8 class (DVecH‘𝑘)
12	9, 11	cfv 6543	. . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13		cbs 17294	. . . . . . 7 class Base
14	12, 13	cfv 6543	. . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
15	14	cpw 4567	. . . . 5 class 𝒫 (Base‘((DVecH‘𝑘)‘𝑤))
16	8	cv 1569	. . . . . . . . . 10 class 𝑥
17		vy	. . . . . . . . . . . 12 setvar 𝑦
18	17	cv 1569	. . . . . . . . . . 11 class 𝑦
19		cdih 42043	. . . . . . . . . . . . 13 class DIsoH
20	5, 19	cfv 6543	. . . . . . . . . . . 12 class (DIsoH‘𝑘)
21	9, 20	cfv 6543	. . . . . . . . . . 11 class ((DIsoH‘𝑘)‘𝑤)
22	18, 21	cfv 6543	. . . . . . . . . 10 class (((DIsoH‘𝑘)‘𝑤)‘𝑦)
23	16, 22	wss 3908	. . . . . . . . 9 wff 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)
24	5, 13	cfv 6543	. . . . . . . . 9 class (Base‘𝑘)
25	23, 17, 24	crab 3419	. . . . . . . 8 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}
26		cglb 18391	. . . . . . . . 9 class glb
27	5, 26	cfv 6543	. . . . . . . 8 class (glb‘𝑘)
28	25, 27	cfv 6543	. . . . . . 7 class ((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})
29		coc 17343	. . . . . . . 8 class oc
30	5, 29	cfv 6543	. . . . . . 7 class (oc‘𝑘)
31	28, 30	cfv 6543	. . . . . 6 class ((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))
32	31, 21	cfv 6543	. . . . 5 class (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))
33	8, 15, 32	cmpt 5197	. . . 4 class (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))
34	4, 7, 33	cmpt 5197	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))
35	2, 3, 34	cmpt 5197	. 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  42164