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