Description: The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015) (Revised by AV, 6-Nov-2024)
| 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 | baseid | ⊢ Base = Slot ( Base ‘ ndx ) | |
| 8 | starvndxnbasendx | ⊢ ( *𝑟 ‘ ndx ) ≠ ( Base ‘ ndx ) | |
| 9 | 8 | necomi | ⊢ ( Base ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) |
| 10 | 1 2 3 4 5 7 9 6 | hlhilslem | ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝑅 ) ) |