Metamath Proof Explorer


Theorem docavalN

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 docavalN K HL W H X T N X = 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 5 6 7 docafvalN K HL W H N = x 𝒫 T I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W
9 8 adantr K HL W H X T N = x 𝒫 T I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W
10 9 fveq1d K HL W H X T N X = x 𝒫 T I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W X
11 5 fvexi T V
12 11 elpw2 X 𝒫 T X T
13 12 biimpri X T X 𝒫 T
14 13 adantl K HL W H X T X 𝒫 T
15 fvex I ˙ I -1 z ran I | X z ˙ ˙ W ˙ W V
16 sseq1 x = X x z X z
17 16 rabbidv x = X z ran I | x z = z ran I | X z
18 17 inteqd x = X z ran I | x z = z ran I | X z
19 18 fveq2d x = X I -1 z ran I | x z = I -1 z ran I | X z
20 19 fveq2d x = X ˙ I -1 z ran I | x z = ˙ I -1 z ran I | X z
21 20 oveq1d x = X ˙ I -1 z ran I | x z ˙ ˙ W = ˙ I -1 z ran I | X z ˙ ˙ W
22 21 fvoveq1d x = X I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W = I ˙ I -1 z ran I | X z ˙ ˙ W ˙ W
23 eqid x 𝒫 T I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W = x 𝒫 T I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W
24 22 23 fvmptg X 𝒫 T I ˙ I -1 z ran I | X z ˙ ˙ W ˙ W V x 𝒫 T I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W X = I ˙ I -1 z ran I | X z ˙ ˙ W ˙ W
25 14 15 24 sylancl K HL W H X T x 𝒫 T I ˙ I -1 z ran I | x z ˙ ˙ W ˙ W X = I ˙ I -1 z ran I | X z ˙ ˙ W ˙ W
26 10 25 eqtrd K HL W H X T N X = I ˙ I -1 z ran I | X z ˙ ˙ W ˙ W