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=BaseL
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=BaseL
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=BaseU
10 rabeq ⊢V=BaseU→y∈V|∀z∈Xy⋅𝑖⁡Uz=0Scalar⁡U=y∈BaseU|∀z∈Xy⋅𝑖⁡Uz=0Scalar⁡U
11 9 10 syl ⊢φ→y∈V|∀z∈Xy⋅𝑖⁡Uz=0Scalar⁡U=y∈BaseU|∀z∈Xy⋅𝑖⁡Uz=0Scalar⁡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⋅𝑖⁡Uz=HDMap⁡K⁡W⁡z⁡y
19 eqid ⊢Scalar⁡L=Scalar⁡L
20 eqid ⊢Scalar⁡U=Scalar⁡U
21 eqid ⊢0Scalar⁡L=0Scalar⁡L
22 1 2 19 3 20 4 21 hlhils0 ⊢φ→0Scalar⁡L=0Scalar⁡U
23 22 eqcomd ⊢φ→0Scalar⁡U=0Scalar⁡L
24 23 ad2antrr ⊢φ∧y∈V∧z∈X→0Scalar⁡U=0Scalar⁡L
25 18 24 eqeq12d ⊢φ∧y∈V∧z∈X→y⋅𝑖⁡Uz=0Scalar⁡U↔HDMap⁡K⁡W⁡z⁡y=0Scalar⁡L
26 25 ralbidva ⊢φ∧y∈V→∀z∈Xy⋅𝑖⁡Uz=0Scalar⁡U↔∀z∈XHDMap⁡K⁡W⁡z⁡y=0Scalar⁡L
27 26 rabbidva ⊢φ→y∈V|∀z∈Xy⋅𝑖⁡Uz=0Scalar⁡U=y∈V|∀z∈XHDMap⁡K⁡W⁡z⁡y=0Scalar⁡L
28 11 27 eqtr3d ⊢φ→y∈BaseU|∀z∈Xy⋅𝑖⁡Uz=0Scalar⁡U=y∈V|∀z∈XHDMap⁡K⁡W⁡z⁡y=0Scalar⁡L
29 8 9 sseqtrd ⊢φ→X⊆BaseU
30 eqid ⊢BaseU=BaseU
31 eqid ⊢0Scalar⁡U=0Scalar⁡U
32 30 14 20 31 7 ocvval ⊢X⊆BaseU→O⁡X=y∈BaseU|∀z∈Xy⋅𝑖⁡Uz=0Scalar⁡U
33 29 32 syl ⊢φ→O⁡X=y∈BaseU|∀z∈Xy⋅𝑖⁡Uz=0Scalar⁡U
34 1 2 5 19 21 6 12 4 8 hdmapoc ⊢φ→N⁡X=y∈V|∀z∈XHDMap⁡K⁡W⁡z⁡y=0Scalar⁡L
35 28 33 34 3eqtr4d ⊢φ→O⁡X=N⁡X