Description: Closure of the vector space to dual space scalar map, in the scalar sigma map. (Contributed by NM, 6-Jun-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hgmapdcl.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| hgmapdcl.u | ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | ||
| hgmapdcl.r | ⊢ 𝑅 = ( Scalar ‘ 𝑈 ) | ||
| hgmapdcl.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | ||
| hgmapdcl.c | ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) | ||
| hgmapdcl.q | ⊢ 𝑄 = ( Scalar ‘ 𝐶 ) | ||
| hgmapdcl.a | ⊢ 𝐴 = ( Base ‘ 𝑄 ) | ||
| hgmapdcl.g | ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) | ||
| hgmapdcl.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | ||
| hgmapdcl.f | ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 ) | ||
| Assertion | hgmapdcl | ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐹 ) ∈ 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hgmapdcl.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| 2 | hgmapdcl.u | ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | |
| 3 | hgmapdcl.r | ⊢ 𝑅 = ( Scalar ‘ 𝑈 ) | |
| 4 | hgmapdcl.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
| 5 | hgmapdcl.c | ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) | |
| 6 | hgmapdcl.q | ⊢ 𝑄 = ( Scalar ‘ 𝐶 ) | |
| 7 | hgmapdcl.a | ⊢ 𝐴 = ( Base ‘ 𝑄 ) | |
| 8 | hgmapdcl.g | ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) | |
| 9 | hgmapdcl.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | |
| 10 | hgmapdcl.f | ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 ) | |
| 11 | 1 2 3 4 8 9 10 | hgmapcl | ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐹 ) ∈ 𝐵 ) |
| 12 | 1 2 3 4 5 6 7 9 | lcdsbase | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) |
| 13 | 11 12 | eleqtrrd | ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐹 ) ∈ 𝐴 ) |