Metamath Proof Explorer


Theorem hdmapoc

Description: Express our constructed orthocomplement (polarity) in terms of the Hilbert space definition of orthocomplement. Lines 24 and 25 in Holland95 p. 14. (Contributed by NM, 17-Jun-2015)

Ref Expression
Hypotheses hdmapoc.h H = LHyp K
hdmapoc.u U = DVecH K W
hdmapoc.v V = Base U
hdmapoc.r R = Scalar U
hdmapoc.z 0 ˙ = 0 R
hdmapoc.o O = ocH K W
hdmapoc.s S = HDMap K W
hdmapoc.k φ K HL W H
hdmapoc.x φ X V
Assertion hdmapoc φ O X = y V | z X S z y = 0 ˙

Proof

Step Hyp Ref Expression
1 hdmapoc.h H = LHyp K
2 hdmapoc.u U = DVecH K W
3 hdmapoc.v V = Base U
4 hdmapoc.r R = Scalar U
5 hdmapoc.z 0 ˙ = 0 R
6 hdmapoc.o O = ocH K W
7 hdmapoc.s S = HDMap K W
8 hdmapoc.k φ K HL W H
9 hdmapoc.x φ X V
10 1 2 3 6 dochssv K HL W H X V O X V
11 8 9 10 syl2anc φ O X V
12 11 sseld φ y O X y V
13 12 pm4.71rd φ y O X y V y O X
14 eqid LSubSp U = LSubSp U
15 eqid LSpan U = LSpan U
16 1 2 8 dvhlmod φ U LMod
17 16 adantr φ y V U LMod
18 1 2 3 14 6 dochlss K HL W H X V O X LSubSp U
19 8 9 18 syl2anc φ O X LSubSp U
20 19 adantr φ y V O X LSubSp U
21 simpr φ y V y V
22 3 14 15 17 20 21 lspsnel5 φ y V y O X LSpan U y O X
23 eqid DIsoH K W = DIsoH K W
24 8 adantr φ y V K HL W H
25 1 2 3 15 23 dihlsprn K HL W H y V LSpan U y ran DIsoH K W
26 24 21 25 syl2anc φ y V LSpan U y ran DIsoH K W
27 1 23 2 3 6 dochcl K HL W H X V O X ran DIsoH K W
28 8 9 27 syl2anc φ O X ran DIsoH K W
29 28 adantr φ y V O X ran DIsoH K W
30 1 23 6 24 26 29 dochord φ y V LSpan U y O X O O X O LSpan U y
31 21 snssd φ y V y V
32 1 2 6 3 15 24 31 dochocsp φ y V O LSpan U y = O y
33 32 sseq2d φ y V O O X O LSpan U y O O X O y
34 9 adantr φ y V X V
35 1 23 2 3 6 dochcl K HL W H y V O y ran DIsoH K W
36 24 31 35 syl2anc φ y V O y ran DIsoH K W
37 1 2 3 23 6 24 34 36 dochsscl φ y V X O y O O X O y
38 33 37 bitr4d φ y V O O X O LSpan U y X O y
39 22 30 38 3bitrd φ y V y O X X O y
40 dfss3 X O y z X z O y
41 39 40 bitrdi φ y V y O X z X z O y
42 8 ad2antrr φ y V z X K HL W H
43 34 sselda φ y V z X z V
44 simplr φ y V z X y V
45 1 6 2 3 4 5 7 42 43 44 hdmapellkr φ y V z X S z y = 0 ˙ y O z
46 1 6 2 3 42 44 43 dochsncom φ y V z X y O z z O y
47 45 46 bitrd φ y V z X S z y = 0 ˙ z O y
48 47 ralbidva φ y V z X S z y = 0 ˙ z X z O y
49 41 48 bitr4d φ y V y O X z X S z y = 0 ˙
50 49 pm5.32da φ y V y O X y V z X S z y = 0 ˙
51 13 50 bitrd φ y O X y V z X S z y = 0 ˙
52 51 abbi2dv φ O X = y | y V z X S z y = 0 ˙
53 df-rab y V | z X S z y = 0 ˙ = y | y V z X S z y = 0 ˙
54 52 53 eqtr4di φ O X = y V | z X S z y = 0 ˙