Description: The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hlhilslem.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
hlhilslem.e | ⊢ 𝐸 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) | ||
hlhilslem.u | ⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 ) | ||
hlhilslem.r | ⊢ 𝑅 = ( Scalar ‘ 𝑈 ) | ||
hlhilslem.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | ||
hlhilsbase.c | ⊢ 𝐶 = ( Base ‘ 𝐸 ) | ||
Assertion | hlhilsbase | ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝑅 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlhilslem.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
2 | hlhilslem.e | ⊢ 𝐸 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) | |
3 | hlhilslem.u | ⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 ) | |
4 | hlhilslem.r | ⊢ 𝑅 = ( Scalar ‘ 𝑈 ) | |
5 | hlhilslem.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | |
6 | hlhilsbase.c | ⊢ 𝐶 = ( Base ‘ 𝐸 ) | |
7 | df-base | ⊢ Base = Slot 1 | |
8 | 1nn | ⊢ 1 ∈ ℕ | |
9 | 1lt4 | ⊢ 1 < 4 | |
10 | 1 2 3 4 5 7 8 9 6 | hlhilslem | ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝑅 ) ) |