Definition df-docaN 42178

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 42177	. 2 class ocA
2		vk	. . 3 setvar 𝑘
3		cvv 3450	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1568	. . . . 5 class 𝑘
6		clh 41042	. . . . 5 class LHyp
7	5, 6	cfv 6538	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9	4	cv 1568	. . . . . . 7 class 𝑤
10		cltrn 41159	. . . . . . . 8 class LTrn
11	5, 10	cfv 6538	. . . . . . 7 class (LTrn‘𝑘)
12	9, 11	cfv 6538	. . . . . 6 class ((LTrn‘𝑘)‘𝑤)
13	12	cpw 4556	. . . . 5 class 𝒫 ((LTrn‘𝑘)‘𝑤)
14	8	cv 1568	. . . . . . . . . . . . 13 class 𝑥
15		vz	. . . . . . . . . . . . . 14 setvar 𝑧
16	15	cv 1568	. . . . . . . . . . . . 13 class 𝑧
17	14, 16	wss 3895	. . . . . . . . . . . 12 wff 𝑥 ⊆ 𝑧
18		cdia 42086	. . . . . . . . . . . . . . 15 class DIsoA
19	5, 18	cfv 6538	. . . . . . . . . . . . . 14 class (DIsoA‘𝑘)
20	9, 19	cfv 6538	. . . . . . . . . . . . 13 class ((DIsoA‘𝑘)‘𝑤)
21	20	crn 5651	. . . . . . . . . . . 12 class ran ((DIsoA‘𝑘)‘𝑤)
22	17, 15, 21	crab 3412	. . . . . . . . . . 11 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}
23	22	cint 4906	. . . . . . . . . 10 class ∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}
24	20	ccnv 5649	. . . . . . . . . 10 class ◡((DIsoA‘𝑘)‘𝑤)
25	23, 24	cfv 6538	. . . . . . . . 9 class (◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧})
26		coc 17436	. . . . . . . . . 10 class oc
27	5, 26	cfv 6538	. . . . . . . . 9 class (oc‘𝑘)
28	25, 27	cfv 6538	. . . . . . . 8 class ((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))
29	9, 27	cfv 6538	. . . . . . . 8 class ((oc‘𝑘)‘𝑤)
30		cjn 18485	. . . . . . . . 9 class join
31	5, 30	cfv 6538	. . . . . . . 8 class (join‘𝑘)
32	28, 29, 31	co 7420	. . . . . . 7 class (((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))
33		cmee 18486	. . . . . . . 8 class meet
34	5, 33	cfv 6538	. . . . . . 7 class (meet‘𝑘)
35	32, 9, 34	co 7420	. . . . . 6 class ((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)
36	35, 20	cfv 6538	. . . . 5 class (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))
37	8, 13, 36	cmpt 5185	. . . 4 class (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))
38	4, 7, 37	cmpt 5185	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))))
39	2, 3, 38	cmpt 5185	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))
40	1, 39	wceq 1569	1 wff ocA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))

This definition is used by:  docaffvalN  42179