Definition df-docaN 39991

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 39990	. 2 class ocA
2		vk	. . 3 setvar 𝑘
3		cvv 3475	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1541	. . . . 5 class 𝑘
6		clh 38855	. . . . 5 class LHyp
7	5, 6	cfv 6544	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9	4	cv 1541	. . . . . . 7 class 𝑤
10		cltrn 38972	. . . . . . . 8 class LTrn
11	5, 10	cfv 6544	. . . . . . 7 class (LTrn‘𝑘)
12	9, 11	cfv 6544	. . . . . 6 class ((LTrn‘𝑘)‘𝑤)
13	12	cpw 4603	. . . . 5 class 𝒫 ((LTrn‘𝑘)‘𝑤)
14	8	cv 1541	. . . . . . . . . . . . 13 class 𝑥
15		vz	. . . . . . . . . . . . . 14 setvar 𝑧
16	15	cv 1541	. . . . . . . . . . . . 13 class 𝑧
17	14, 16	wss 3949	. . . . . . . . . . . 12 wff 𝑥 ⊆ 𝑧
18		cdia 39899	. . . . . . . . . . . . . . 15 class DIsoA
19	5, 18	cfv 6544	. . . . . . . . . . . . . 14 class (DIsoA‘𝑘)
20	9, 19	cfv 6544	. . . . . . . . . . . . 13 class ((DIsoA‘𝑘)‘𝑤)
21	20	crn 5678	. . . . . . . . . . . 12 class ran ((DIsoA‘𝑘)‘𝑤)
22	17, 15, 21	crab 3433	. . . . . . . . . . 11 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}
23	22	cint 4951	. . . . . . . . . 10 class ∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}
24	20	ccnv 5676	. . . . . . . . . 10 class ◡((DIsoA‘𝑘)‘𝑤)
25	23, 24	cfv 6544	. . . . . . . . 9 class (◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧})
26		coc 17205	. . . . . . . . . 10 class oc
27	5, 26	cfv 6544	. . . . . . . . 9 class (oc‘𝑘)
28	25, 27	cfv 6544	. . . . . . . 8 class ((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))
29	9, 27	cfv 6544	. . . . . . . 8 class ((oc‘𝑘)‘𝑤)
30		cjn 18264	. . . . . . . . 9 class join
31	5, 30	cfv 6544	. . . . . . . 8 class (join‘𝑘)
32	28, 29, 31	co 7409	. . . . . . 7 class (((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))
33		cmee 18265	. . . . . . . 8 class meet
34	5, 33	cfv 6544	. . . . . . 7 class (meet‘𝑘)
35	32, 9, 34	co 7409	. . . . . 6 class ((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)
36	35, 20	cfv 6544	. . . . 5 class (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))
37	8, 13, 36	cmpt 5232	. . . 4 class (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))
38	4, 7, 37	cmpt 5232	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))))
39	2, 3, 38	cmpt 5232	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))
40	1, 39	wceq 1542	1 wff ocA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))))

This definition is referenced by:  docaffvalN  39992