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 ⊆ z join ⁡ k oc ⁡ k ⁡ w meet ⁡ k w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cocaN class ocA
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp ⁡ k
7 vx setvar x
8 cltrn class LTrn
9 5 8 cfv class LTrn ⁡ k
10 3 cv setvar w
11 10 9 cfv class LTrn ⁡ k ⁡ w
12 11 cpw class 𝒫 LTrn ⁡ k ⁡ w
13 cdia class DIsoA
14 5 13 cfv class DIsoA ⁡ k
15 10 14 cfv class DIsoA ⁡ k ⁡ w
16 coc class oc
17 5 16 cfv class oc ⁡ k
18 15 ccnv class DIsoA ⁡ k ⁡ w -1
19 vz setvar z
20 15 crn class ran ⁡ DIsoA ⁡ k ⁡ w
21 7 cv setvar x
22 19 cv setvar z
23 21 22 wss wff x ⊆ z
24 23 19 20 crab class z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z
25 24 cint class ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z
26 25 18 cfv class DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z
27 26 17 cfv class oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z
28 cjn class join
29 5 28 cfv class join ⁡ k
30 10 17 cfv class oc ⁡ k ⁡ w
31 27 30 29 co class oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z join ⁡ k oc ⁡ k ⁡ w
32 cmee class meet
33 5 32 cfv class meet ⁡ k
34 31 10 33 co class oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z join ⁡ k oc ⁡ k ⁡ w meet ⁡ k w
35 34 15 cfv class DIsoA ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z join ⁡ k oc ⁡ k ⁡ w meet ⁡ k w
36 7 12 35 cmpt class x ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z join ⁡ k oc ⁡ k ⁡ w meet ⁡ k w
37 3 6 36 cmpt class w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z join ⁡ k oc ⁡ k ⁡ w meet ⁡ k w
38 1 2 37 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z join ⁡ k oc ⁡ k ⁡ w meet ⁡ k w
39 0 38 wceq wff 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 ⊆ z join ⁡ k oc ⁡ k ⁡ w meet ⁡ k w