Metamath Proof Explorer


Theorem docafvalN

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
docaval.t T = LTrn K W
docaval.i I = DIsoA K W
docaval.n N = ocA K W
Assertion docafvalN K V W H N = x 𝒫 T I ˙ I -1 z ran I | 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 docaval.t T = LTrn K W
6 docaval.i I = DIsoA K W
7 docaval.n N = ocA K W
8 1 2 3 4 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
9 8 fveq1d K V ocA K W = w H x 𝒫 LTrn K w DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w W
10 7 9 syl5eq K V N = w H x 𝒫 LTrn K w DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w W
11 fveq2 w = W LTrn K w = LTrn K W
12 11 5 eqtr4di w = W LTrn K w = T
13 12 pweqd w = W 𝒫 LTrn K w = 𝒫 T
14 fveq2 w = W DIsoA K w = DIsoA K W
15 14 6 eqtr4di w = W DIsoA K w = I
16 15 cnveqd w = W DIsoA K w -1 = I -1
17 15 rneqd w = W ran DIsoA K w = ran I
18 17 rabeqdv w = W z ran DIsoA K w | x z = z ran I | x z
19 18 inteqd w = W z ran DIsoA K w | x z = z ran I | x z
20 16 19 fveq12d w = W DIsoA K w -1 z ran DIsoA K w | x z = I -1 z ran I | x z
21 20 fveq2d w = W ˙ DIsoA K w -1 z ran DIsoA K w | x z = ˙ I -1 z ran I | x z
22 fveq2 w = W ˙ w = ˙ W
23 21 22 oveq12d w = W ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w = ˙ I -1 z ran I | x z ˙ ˙ W
24 id w = W w = W
25 23 24 oveq12d w = W ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w = ˙ I -1 z ran I | x z ˙ ˙ W ˙ W
26 15 25 fveq12d w = W DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w = I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W
27 13 26 mpteq12dv w = W x 𝒫 LTrn K w DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w = x 𝒫 T I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W
28 eqid w H x 𝒫 LTrn K w DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w = w H x 𝒫 LTrn K w DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w
29 5 fvexi T V
30 29 pwex 𝒫 T V
31 30 mptex x 𝒫 T I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W V
32 27 28 31 fvmpt W H w H x 𝒫 LTrn K w DIsoA K w ˙ DIsoA K w -1 z ran DIsoA K w | x z ˙ ˙ w ˙ w W = x 𝒫 T I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W
33 10 32 sylan9eq K V W H N = x 𝒫 T I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W