Definition df-docaN 41229

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 41228	. 2 class ocA
2		vk	. . 3 setvar 𝑘
3		cvv 3436	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1540	. . . . 5 class 𝑘
6		clh 40093	. . . . 5 class LHyp
7	5, 6	cfv 6481	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9	4	cv 1540	. . . . . . 7 class 𝑤
10		cltrn 40210	. . . . . . . 8 class LTrn
11	5, 10	cfv 6481	. . . . . . 7 class (LTrn‘𝑘)
12	9, 11	cfv 6481	. . . . . 6 class ((LTrn‘𝑘)‘𝑤)
13	12	cpw 4547	. . . . 5 class 𝒫 ((LTrn‘𝑘)‘𝑤)
14	8	cv 1540	. . . . . . . . . . . . 13 class 𝑥
15		vz	. . . . . . . . . . . . . 14 setvar 𝑧
16	15	cv 1540	. . . . . . . . . . . . 13 class 𝑧
17	14, 16	wss 3897	. . . . . . . . . . . 12 wff 𝑥 ⊆ 𝑧
18		cdia 41137	. . . . . . . . . . . . . . 15 class DIsoA
19	5, 18	cfv 6481	. . . . . . . . . . . . . 14 class (DIsoA‘𝑘)
20	9, 19	cfv 6481	. . . . . . . . . . . . 13 class ((DIsoA‘𝑘)‘𝑤)
21	20	crn 5615	. . . . . . . . . . . 12 class ran ((DIsoA‘𝑘)‘𝑤)
22	17, 15, 21	crab 3395	. . . . . . . . . . 11 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}
23	22	cint 4895	. . . . . . . . . 10 class ∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}
24	20	ccnv 5613	. . . . . . . . . 10 class ◡((DIsoA‘𝑘)‘𝑤)
25	23, 24	cfv 6481	. . . . . . . . 9 class (◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧})
26		coc 17169	. . . . . . . . . 10 class oc
27	5, 26	cfv 6481	. . . . . . . . 9 class (oc‘𝑘)
28	25, 27	cfv 6481	. . . . . . . 8 class ((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))
29	9, 27	cfv 6481	. . . . . . . 8 class ((oc‘𝑘)‘𝑤)
30		cjn 18217	. . . . . . . . 9 class join
31	5, 30	cfv 6481	. . . . . . . 8 class (join‘𝑘)
32	28, 29, 31	co 7346	. . . . . . 7 class (((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))
33		cmee 18218	. . . . . . . 8 class meet
34	5, 33	cfv 6481	. . . . . . 7 class (meet‘𝑘)
35	32, 9, 34	co 7346	. . . . . 6 class ((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)
36	35, 20	cfv 6481	. . . . 5 class (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))
37	8, 13, 36	cmpt 5170	. . . 4 class (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))
38	4, 7, 37	cmpt 5170	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))))
39	2, 3, 38	cmpt 5170	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))
40	1, 39	wceq 1541	1 wff ocA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))

This definition is referenced by:  docaffvalN  41230