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