Metamath Proof Explorer

Theorem hlhilbase

Description: The base set of the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

Ref Expression
Hypotheses hlhilbase.h ⊢ H = LHyp ⁡ K
hlhilbase.u ⊢ U = HLHil ⁡ K ⁡ W
hlhilbase.k ⊢ φ → K ∈ HL ∧ W ∈ H
hlhilbase.l ⊢ L = DVecH ⁡ K ⁡ W
hlhilbase.m ⊢ M = Base L
Assertion hlhilbase ⊢ φ → M = Base U

Proof

Step Hyp Ref Expression
1 hlhilbase.h ⊢ H = LHyp ⁡ K
2 hlhilbase.u ⊢ U = HLHil ⁡ K ⁡ W
3 hlhilbase.k ⊢ φ → K ∈ HL ∧ W ∈ H
4 hlhilbase.l ⊢ L = DVecH ⁡ K ⁡ W
5 hlhilbase.m ⊢ M = Base L
6 5 fvexi ⊢ M ∈ V
7 eqid ⊢ Base ndx M + ndx + L Scalar ⁡ ndx EDRing ⁡ K ⁡ W sSet * ndx HGMap ⁡ K ⁡ W ∪ ⋅ ndx ⋅ L ⋅ 𝑖 ⁡ ndx x ∈ M , y ∈ M ⟼ HDMap ⁡ K ⁡ W ⁡ y ⁡ x = Base ndx M + ndx + L Scalar ⁡ ndx EDRing ⁡ K ⁡ W sSet * ndx HGMap ⁡ K ⁡ W ∪ ⋅ ndx ⋅ L ⋅ 𝑖 ⁡ ndx x ∈ M , y ∈ M ⟼ HDMap ⁡ K ⁡ W ⁡ y ⁡ x
8 7 phlbase ⊢ M ∈ V → M = Base Base ndx M + ndx + L Scalar ⁡ ndx EDRing ⁡ K ⁡ W sSet * ndx HGMap ⁡ K ⁡ W ∪ ⋅ ndx ⋅ L ⋅ 𝑖 ⁡ ndx x ∈ M , y ∈ M ⟼ HDMap ⁡ K ⁡ W ⁡ y ⁡ x
9 6 8 ax-mp ⊢ M = Base Base ndx M + ndx + L Scalar ⁡ ndx EDRing ⁡ K ⁡ W sSet * ndx HGMap ⁡ K ⁡ W ∪ ⋅ ndx ⋅ L ⋅ 𝑖 ⁡ ndx x ∈ M , y ∈ M ⟼ HDMap ⁡ K ⁡ W ⁡ y ⁡ x
10 eqid ⊢ + L = + L
11 eqid ⊢ EDRing ⁡ K ⁡ W = EDRing ⁡ K ⁡ W
12 eqid ⊢ HGMap ⁡ K ⁡ W = HGMap ⁡ K ⁡ W
13 eqid ⊢ EDRing ⁡ K ⁡ W sSet * ndx HGMap ⁡ K ⁡ W = EDRing ⁡ K ⁡ W sSet * ndx HGMap ⁡ K ⁡ W
14 eqid ⊢ ⋅ L = ⋅ L
15 eqid ⊢ HDMap ⁡ K ⁡ W = HDMap ⁡ K ⁡ W
16 eqid ⊢ x ∈ M , y ∈ M ⟼ HDMap ⁡ K ⁡ W ⁡ y ⁡ x = x ∈ M , y ∈ M ⟼ HDMap ⁡ K ⁡ W ⁡ y ⁡ x
17 1 2 4 5 10 11 12 13 14 15 16 3 hlhilset ⊢ φ → U = Base ndx M + ndx + L Scalar ⁡ ndx EDRing ⁡ K ⁡ W sSet * ndx HGMap ⁡ K ⁡ W ∪ ⋅ ndx ⋅ L ⋅ 𝑖 ⁡ ndx x ∈ M , y ∈ M ⟼ HDMap ⁡ K ⁡ W ⁡ y ⁡ x
18 17 fveq2d ⊢ φ → Base U = Base Base ndx M + ndx + L Scalar ⁡ ndx EDRing ⁡ K ⁡ W sSet * ndx HGMap ⁡ K ⁡ W ∪ ⋅ ndx ⋅ L ⋅ 𝑖 ⁡ ndx x ∈ M , y ∈ M ⟼ HDMap ⁡ K ⁡ W ⁡ y ⁡ x
19 9 18 eqtr4id ⊢ φ → M = Base U