Metamath Proof Explorer

Definition df-docaN

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)

Ref Expression
Assertion df-docaN ⊢ocA=k∈V⟼w∈LHyp⁡k⟼x∈𝒫LTrn⁡k⁡w⟼DIsoA⁡k⁡w⁡oc⁡k⁡DIsoA⁡k⁡w-1⁡⋂z∈ran⁡DIsoA⁡k⁡w|x⊆zjoin⁡koc⁡k⁡wmeet⁡kw

Detailed syntax breakdown

Step Hyp Ref Expression
0 cocaN classocA
1 vk setvark
2 cvv classV
3 vw setvarw
4 clh classLHyp
5 1 cv setvark
6 5 4 cfv classLHyp⁡k
7 vx setvarx
8 cltrn classLTrn
9 5 8 cfv classLTrn⁡k
10 3 cv setvarw
11 10 9 cfv classLTrn⁡k⁡w
12 11 cpw class𝒫LTrn⁡k⁡w
13 cdia classDIsoA
14 5 13 cfv classDIsoA⁡k
15 10 14 cfv classDIsoA⁡k⁡w
16 coc classoc
17 5 16 cfv classoc⁡k
18 15 ccnv classDIsoA⁡k⁡w-1
19 vz setvarz
20 15 crn classran⁡DIsoA⁡k⁡w
21 7 cv setvarx
22 19 cv setvarz
23 21 22 wss wffx⊆z
24 23 19 20 crab classz∈ran⁡DIsoA⁡k⁡w|x⊆z
25 24 cint class⋂z∈ran⁡DIsoA⁡k⁡w|x⊆z
26 25 18 cfv classDIsoA⁡k⁡w-1⁡⋂z∈ran⁡DIsoA⁡k⁡w|x⊆z
27 26 17 cfv classoc⁡k⁡DIsoA⁡k⁡w-1⁡⋂z∈ran⁡DIsoA⁡k⁡w|x⊆z
28 cjn classjoin
29 5 28 cfv classjoin⁡k
30 10 17 cfv classoc⁡k⁡w
31 27 30 29 co classoc⁡k⁡DIsoA⁡k⁡w-1⁡⋂z∈ran⁡DIsoA⁡k⁡w|x⊆zjoin⁡koc⁡k⁡w
32 cmee classmeet
33 5 32 cfv classmeet⁡k
34 31 10 33 co classoc⁡k⁡DIsoA⁡k⁡w-1⁡⋂z∈ran⁡DIsoA⁡k⁡w|x⊆zjoin⁡koc⁡k⁡wmeet⁡kw
35 34 15 cfv classDIsoA⁡k⁡w⁡oc⁡k⁡DIsoA⁡k⁡w-1⁡⋂z∈ran⁡DIsoA⁡k⁡w|x⊆zjoin⁡koc⁡k⁡wmeet⁡kw
36 7 12 35 cmpt classx∈𝒫LTrn⁡k⁡w⟼DIsoA⁡k⁡w⁡oc⁡k⁡DIsoA⁡k⁡w-1⁡⋂z∈ran⁡DIsoA⁡k⁡w|x⊆zjoin⁡koc⁡k⁡wmeet⁡kw
37 3 6 36 cmpt classw∈LHyp⁡k⟼x∈𝒫LTrn⁡k⁡w⟼DIsoA⁡k⁡w⁡oc⁡k⁡DIsoA⁡k⁡w-1⁡⋂z∈ran⁡DIsoA⁡k⁡w|x⊆zjoin⁡koc⁡k⁡wmeet⁡kw
38 1 2 37 cmpt classk∈V⟼w∈LHyp⁡k⟼x∈𝒫LTrn⁡k⁡w⟼DIsoA⁡k⁡w⁡oc⁡k⁡DIsoA⁡k⁡w-1⁡⋂z∈ran⁡DIsoA⁡k⁡w|x⊆zjoin⁡koc⁡k⁡wmeet⁡kw
39 0 38 wceq wffocA=k∈V⟼w∈LHyp⁡k⟼x∈𝒫LTrn⁡k⁡w⟼DIsoA⁡k⁡w⁡oc⁡k⁡DIsoA⁡k⁡w-1⁡⋂z∈ran⁡DIsoA⁡k⁡w|x⊆zjoin⁡koc⁡k⁡wmeet⁡kw