Description: The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | lcd1.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| lcd1.u | ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | ||
| lcd1.f | ⊢ 𝐹 = ( Scalar ‘ 𝑈 ) | ||
| lcd1.j | ⊢ 1 = ( 1r ‘ 𝐹 ) | ||
| lcd1.c | ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) | ||
| lcd1.s | ⊢ 𝑆 = ( Scalar ‘ 𝐶 ) | ||
| lcd1.i | ⊢ 𝐼 = ( 1r ‘ 𝑆 ) | ||
| lcd1.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | ||
| Assertion | lcd1 | ⊢ ( 𝜑 → 𝐼 = 1 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lcd1.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| 2 | lcd1.u | ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | |
| 3 | lcd1.f | ⊢ 𝐹 = ( Scalar ‘ 𝑈 ) | |
| 4 | lcd1.j | ⊢ 1 = ( 1r ‘ 𝐹 ) | |
| 5 | lcd1.c | ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) | |
| 6 | lcd1.s | ⊢ 𝑆 = ( Scalar ‘ 𝐶 ) | |
| 7 | lcd1.i | ⊢ 𝐼 = ( 1r ‘ 𝑆 ) | |
| 8 | lcd1.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | |
| 9 | eqid | ⊢ ( oppr ‘ 𝐹 ) = ( oppr ‘ 𝐹 ) | |
| 10 | 1 2 3 9 5 6 8 | lcdsca | ⊢ ( 𝜑 → 𝑆 = ( oppr ‘ 𝐹 ) ) |
| 11 | 10 | fveq2d | ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 1r ‘ ( oppr ‘ 𝐹 ) ) ) |
| 12 | 9 4 | oppr1 | ⊢ 1 = ( 1r ‘ ( oppr ‘ 𝐹 ) ) |
| 13 | 11 7 12 | 3eqtr4g | ⊢ ( 𝜑 → 𝐼 = 1 ) |