Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hdmap14lem1 Structured version   Visualization version   GIF version

Theorem hdmap14lem1 39122
 Description: Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
Hypotheses
Ref Expression
hdmap14lem1.h 𝐻 = (LHyp‘𝐾)
hdmap14lem1.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
hdmap14lem1.v 𝑉 = (Base‘𝑈)
hdmap14lem1.t · = ( ·𝑠𝑈)
hdmap14lem3.o 0 = (0g𝑈)
hdmap14lem1.r 𝑅 = (Scalar‘𝑈)
hdmap14lem1.b 𝐵 = (Base‘𝑅)
hdmap14lem1.z 𝑍 = (0g𝑅)
hdmap14lem1.c 𝐶 = ((LCDual‘𝐾)‘𝑊)
hdmap14lem2.e = ( ·𝑠𝐶)
hdmap14lem1.l 𝐿 = (LSpan‘𝐶)
hdmap14lem2.p 𝑃 = (Scalar‘𝐶)
hdmap14lem2.a 𝐴 = (Base‘𝑃)
hdmap14lem2.q 𝑄 = (0g𝑃)
hdmap14lem1.s 𝑆 = ((HDMap‘𝐾)‘𝑊)
hdmap14lem1.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
hdmap14lem3.x (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
hdmap14lem1.f (𝜑𝐹 ∈ (𝐵 ∖ {𝑍}))
Assertion
Ref Expression
hdmap14lem1 (𝜑 → (𝐿‘{(𝑆𝑋)}) = (𝐿‘{(𝑆‘(𝐹 · 𝑋))}))

Proof of Theorem hdmap14lem1
StepHypRef Expression
1 hdmap14lem1.h . 2 𝐻 = (LHyp‘𝐾)
2 hdmap14lem1.u . 2 𝑈 = ((DVecH‘𝐾)‘𝑊)
3 hdmap14lem1.v . 2 𝑉 = (Base‘𝑈)
4 hdmap14lem1.t . 2 · = ( ·𝑠𝑈)
5 hdmap14lem1.r . 2 𝑅 = (Scalar‘𝑈)
6 hdmap14lem1.b . 2 𝐵 = (Base‘𝑅)
7 hdmap14lem1.c . 2 𝐶 = ((LCDual‘𝐾)‘𝑊)
8 hdmap14lem2.e . 2 = ( ·𝑠𝐶)
9 hdmap14lem1.l . 2 𝐿 = (LSpan‘𝐶)
10 hdmap14lem2.p . 2 𝑃 = (Scalar‘𝐶)
11 hdmap14lem2.a . 2 𝐴 = (Base‘𝑃)
12 hdmap14lem1.s . 2 𝑆 = ((HDMap‘𝐾)‘𝑊)
13 hdmap14lem1.k . 2 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
14 hdmap14lem3.x . . 3 (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))