Metamath Proof Explorer


Theorem hlhilocv

Description: The orthocomplement for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015) (Revised by Mario Carneiro, 29-Jun-2015)

Ref Expression
Hypotheses hlhil0.h H = LHyp K
hlhil0.l L = DVecH K W
hlhil0.u U = HLHil K W
hlhil0.k φ K HL W H
hlhilocv.v V = Base L
hlhilocv.n N = ocH K W
hlhilocv.o O = ocv U
hlhilocv.x φ X V
Assertion hlhilocv φ O X = N X

Proof

Step Hyp Ref Expression
1 hlhil0.h H = LHyp K
2 hlhil0.l L = DVecH K W
3 hlhil0.u U = HLHil K W
4 hlhil0.k φ K HL W H
5 hlhilocv.v V = Base L
6 hlhilocv.n N = ocH K W
7 hlhilocv.o O = ocv U
8 hlhilocv.x φ X V
9 1 3 4 2 5 hlhilbase φ V = Base U
10 rabeq V = Base U y V | z X y 𝑖 U z = 0 Scalar U = y Base U | z X y 𝑖 U z = 0 Scalar U
11 9 10 syl φ y V | z X y 𝑖 U z = 0 Scalar U = y Base U | z X y 𝑖 U z = 0 Scalar U
12 eqid HDMap K W = HDMap K W
13 4 ad2antrr φ y V z X K HL W H
14 eqid 𝑖 U = 𝑖 U
15 simplr φ y V z X y V
16 8 adantr φ y V X V
17 16 sselda φ y V z X z V
18 1 2 5 12 3 13 14 15 17 hlhilipval φ y V z X y 𝑖 U z = HDMap K W z y
19 eqid Scalar L = Scalar L
20 eqid Scalar U = Scalar U
21 eqid 0 Scalar L = 0 Scalar L
22 1 2 19 3 20 4 21 hlhils0 φ 0 Scalar L = 0 Scalar U
23 22 eqcomd φ 0 Scalar U = 0 Scalar L
24 23 ad2antrr φ y V z X 0 Scalar U = 0 Scalar L
25 18 24 eqeq12d φ y V z X y 𝑖 U z = 0 Scalar U HDMap K W z y = 0 Scalar L
26 25 ralbidva φ y V z X y 𝑖 U z = 0 Scalar U z X HDMap K W z y = 0 Scalar L
27 26 rabbidva φ y V | z X y 𝑖 U z = 0 Scalar U = y V | z X HDMap K W z y = 0 Scalar L
28 11 27 eqtr3d φ y Base U | z X y 𝑖 U z = 0 Scalar U = y V | z X HDMap K W z y = 0 Scalar L
29 8 9 sseqtrd φ X Base U
30 eqid Base U = Base U
31 eqid 0 Scalar U = 0 Scalar U
32 30 14 20 31 7 ocvval X Base U O X = y Base U | z X y 𝑖 U z = 0 Scalar U
33 29 32 syl φ O X = y Base U | z X y 𝑖 U z = 0 Scalar U
34 1 2 5 19 21 6 12 4 8 hdmapoc φ N X = y V | z X HDMap K W z y = 0 Scalar L
35 28 33 34 3eqtr4d φ O X = N X