Definition df-docaN 40077

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 40076	. 2 class ocA
2		vk	. . 3 setvar 𝑘
3		cvv 3474	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1540	. . . . 5 class 𝑘
6		clh 38941	. . . . 5 class LHyp
7	5, 6	cfv 6543	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9	4	cv 1540	. . . . . . 7 class 𝑤
10		cltrn 39058	. . . . . . . 8 class LTrn
11	5, 10	cfv 6543	. . . . . . 7 class (LTrn‘𝑘)
12	9, 11	cfv 6543	. . . . . 6 class ((LTrn‘𝑘)‘𝑤)
13	12	cpw 4602	. . . . 5 class 𝒫 ((LTrn‘𝑘)‘𝑤)
14	8	cv 1540	. . . . . . . . . . . . 13 class 𝑥
15		vz	. . . . . . . . . . . . . 14 setvar 𝑧
16	15	cv 1540	. . . . . . . . . . . . 13 class 𝑧
17	14, 16	wss 3948	. . . . . . . . . . . 12 wff 𝑥 ⊆ 𝑧
18		cdia 39985	. . . . . . . . . . . . . . 15 class DIsoA
19	5, 18	cfv 6543	. . . . . . . . . . . . . 14 class (DIsoA‘𝑘)
20	9, 19	cfv 6543	. . . . . . . . . . . . 13 class ((DIsoA‘𝑘)‘𝑤)
21	20	crn 5677	. . . . . . . . . . . 12 class ran ((DIsoA‘𝑘)‘𝑤)
22	17, 15, 21	crab 3432	. . . . . . . . . . 11 class {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}
23	22	cint 4950	. . . . . . . . . 10 class ∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}
24	20	ccnv 5675	. . . . . . . . . 10 class ◡((DIsoA‘𝑘)‘𝑤)
25	23, 24	cfv 6543	. . . . . . . . 9 class (◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧})
26		coc 17207	. . . . . . . . . 10 class oc
27	5, 26	cfv 6543	. . . . . . . . 9 class (oc‘𝑘)
28	25, 27	cfv 6543	. . . . . . . 8 class ((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))
29	9, 27	cfv 6543	. . . . . . . 8 class ((oc‘𝑘)‘𝑤)
30		cjn 18266	. . . . . . . . 9 class join
31	5, 30	cfv 6543	. . . . . . . 8 class (join‘𝑘)
32	28, 29, 31	co 7411	. . . . . . 7 class (((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))
33		cmee 18267	. . . . . . . 8 class meet
34	5, 33	cfv 6543	. . . . . . 7 class (meet‘𝑘)
35	32, 9, 34	co 7411	. . . . . 6 class ((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)
36	35, 20	cfv 6543	. . . . 5 class (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))
37	8, 13, 36	cmpt 5231	. . . 4 class (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))
38	4, 7, 37	cmpt 5231	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))))
39	2, 3, 38	cmpt 5231	. 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  40078