Definition df-docaN 38289

Description: Define subspace orthocomplement for DVecA partial 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, 6-Dec-2013.)

Assertion

Ref	Expression
df-docaN	⊢ ocA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))

Distinct variable group:   𝑤,𝑘,𝑥,𝑧

Detailed syntax breakdown of Definition df-docaN

Step	Hyp	Ref	Expression
1		cocaN 38288	. 2 class ocA
2		vk	. . 3 setvar 𝑘
3		cvv 3491	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1535	. . . . 5 class 𝑘
6		clh 37153	. . . . 5 class LHyp
7	5, 6	cfv 6348	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9	4	cv 1535	. . . . . . 7 class 𝑤
10		cltrn 37270	. . . . . . . 8 class LTrn
11	5, 10	cfv 6348	. . . . . . 7 class (LTrn‘𝑘)
12	9, 11	cfv 6348	. . . . . 6 class ((LTrn‘𝑘)‘𝑤)
13	12	cpw 4532	. . . . 5 class 𝒫 ((LTrn‘𝑘)‘𝑤)
14	8	cv 1535	. . . . . . . . . . . . 13 class 𝑥
15		vz	. . . . . . . . . . . . . 14 setvar 𝑧
16	15	cv 1535	. . . . . . . . . . . . 13 class 𝑧
17	14, 16	wss 3929	. . . . . . . . . . . 12 wff 𝑥 ⊆ 𝑧
18		cdia 38197	. . . . . . . . . . . . . . 15 class DIsoA
19	5, 18	cfv 6348	. . . . . . . . . . . . . 14 class (DIsoA‘𝑘)
20	9, 19	cfv 6348	. . . . . . . . . . . . 13 class ((DIsoA‘𝑘)‘𝑤)
21	20	crn 5549	. . . . . . . . . . . 12 class ran ((DIsoA‘𝑘)‘𝑤)
22	17, 15, 21	crab 3141	. . . . . . . . . . 11 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}
23	22	cint 4869	. . . . . . . . . 10 class ∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}
24	20	ccnv 5547	. . . . . . . . . 10 class ◡((DIsoA‘𝑘)‘𝑤)
25	23, 24	cfv 6348	. . . . . . . . 9 class (◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧})
26		coc 16568	. . . . . . . . . 10 class oc
27	5, 26	cfv 6348	. . . . . . . . 9 class (oc‘𝑘)
28	25, 27	cfv 6348	. . . . . . . 8 class ((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))
29	9, 27	cfv 6348	. . . . . . . 8 class ((oc‘𝑘)‘𝑤)
30		cjn 17549	. . . . . . . . 9 class join
31	5, 30	cfv 6348	. . . . . . . 8 class (join‘𝑘)
32	28, 29, 31	co 7149	. . . . . . 7 class (((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))
33		cmee 17550	. . . . . . . 8 class meet
34	5, 33	cfv 6348	. . . . . . 7 class (meet‘𝑘)
35	32, 9, 34	co 7149	. . . . . 6 class ((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)
36	35, 20	cfv 6348	. . . . 5 class (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))
37	8, 13, 36	cmpt 5139	. . . 4 class (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))
38	4, 7, 37	cmpt 5139	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))))
39	2, 3, 38	cmpt 5139	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))
40	1, 39	wceq 1536	1 wff ocA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))

This definition is referenced by:  docaffvalN  38290