Metamath Proof Explorer


Theorem docaffvalN

Description: Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses docaval.j ˙ = join K
docaval.m ˙ = meet K
docaval.o ˙ = oc K
docaval.h H = LHyp K
Assertion docaffvalN K V ocA K = w H x 𝒫 LTrn K w DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w

Proof

Step Hyp Ref Expression
1 docaval.j ˙ = join K
2 docaval.m ˙ = meet K
3 docaval.o ˙ = oc K
4 docaval.h H = LHyp K
5 elex K V K V
6 fveq2 k = K LHyp k = LHyp K
7 6 4 eqtr4di k = K LHyp k = H
8 fveq2 k = K LTrn k = LTrn K
9 8 fveq1d k = K LTrn k w = LTrn K w
10 9 pweqd k = K 𝒫 LTrn k w = 𝒫 LTrn K w
11 fveq2 k = K DIsoA k = DIsoA K
12 11 fveq1d k = K DIsoA k w = DIsoA K w
13 fveq2 k = K meet k = meet K
14 13 2 eqtr4di k = K meet k = ˙
15 fveq2 k = K join k = join K
16 15 1 eqtr4di k = K join k = ˙
17 fveq2 k = K oc k = oc K
18 17 3 eqtr4di k = K oc k = ˙
19 12 cnveqd k = K DIsoA k w -1 = DIsoA K w -1
20 12 rneqd k = K ran DIsoA k w = ran DIsoA K w
21 20 rabeqdv k = K z ran DIsoA k w | x z = z ran DIsoA K w | x z
22 21 inteqd k = K z ran DIsoA k w | x z = z ran DIsoA K w | x z
23 19 22 fveq12d k = K DIsoA k w -1 z ran DIsoA k w | x z = DIsoA K w -1 z ran DIsoA K w | x z
24 18 23 fveq12d k = K oc k DIsoA k w -1 z ran DIsoA k w | x z = ˙ DIsoA K w -1 z ran DIsoA K w | x z
25 18 fveq1d k = K oc k w = ˙ w
26 16 24 25 oveq123d k = K oc k DIsoA k w -1 z ran DIsoA k w | x z join k oc k w = ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w
27 eqidd k = K w = w
28 14 26 27 oveq123d k = K oc k DIsoA k w -1 z ran DIsoA k w | x z join k oc k w meet k w = ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w
29 12 28 fveq12d k = K DIsoA k w oc k DIsoA k w -1 z ran DIsoA k w | x z join k oc k w meet k w = DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w
30 10 29 mpteq12dv k = 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 = x 𝒫 LTrn K w DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w
31 7 30 mpteq12dv k = K 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 = w H x 𝒫 LTrn K w DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w
32 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
33 31 32 4 mptfvmpt K V ocA K = w H x 𝒫 LTrn K w DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w
34 5 33 syl K V ocA K = w H x 𝒫 LTrn K w DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w