Description: The unit scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ldual1.r | ⊢ 𝑅 = ( Scalar ‘ 𝑊 ) | |
ldual1.u | ⊢ 1 = ( 1r ‘ 𝑅 ) | ||
ldual1.d | ⊢ 𝐷 = ( LDual ‘ 𝑊 ) | ||
ldual1.s | ⊢ 𝑆 = ( Scalar ‘ 𝐷 ) | ||
ldual1.i | ⊢ 𝐼 = ( 1r ‘ 𝑆 ) | ||
ldual1.w | ⊢ ( 𝜑 → 𝑊 ∈ LMod ) | ||
Assertion | ldual1 | ⊢ ( 𝜑 → 𝐼 = 1 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ldual1.r | ⊢ 𝑅 = ( Scalar ‘ 𝑊 ) | |
2 | ldual1.u | ⊢ 1 = ( 1r ‘ 𝑅 ) | |
3 | ldual1.d | ⊢ 𝐷 = ( LDual ‘ 𝑊 ) | |
4 | ldual1.s | ⊢ 𝑆 = ( Scalar ‘ 𝐷 ) | |
5 | ldual1.i | ⊢ 𝐼 = ( 1r ‘ 𝑆 ) | |
6 | ldual1.w | ⊢ ( 𝜑 → 𝑊 ∈ LMod ) | |
7 | eqid | ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 ) | |
8 | 1 7 3 4 6 | ldualsca | ⊢ ( 𝜑 → 𝑆 = ( oppr ‘ 𝑅 ) ) |
9 | 8 | fveq2d | ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 1r ‘ ( oppr ‘ 𝑅 ) ) ) |
10 | 7 2 | oppr1 | ⊢ 1 = ( 1r ‘ ( oppr ‘ 𝑅 ) ) |
11 | 9 5 10 | 3eqtr4g | ⊢ ( 𝜑 → 𝐼 = 1 ) |