P. 411 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41001-41100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hdmapffval 41001*	Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑋 → (HDMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
Theorem	hdmapfval 41002*	Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑆 = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))
Theorem	hdmapval 41003*	Value of map from vectors to functionals in the closed kernel dual space. This is the function sigma on line 27 above part 9 in [Baer] p. 48. We select a convenient fixed reference vector 𝐸 to be ⟨0, 1⟩ (corresponding to vector u on p. 48 line 7) whose span is the lattice isomorphism map of the fiducial atom 𝑃 = ((oc‘𝐾)‘𝑊) (see dvheveccl 40287). (𝐽‘𝐸) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap 40944 shows in Baer's notation (Fu)* = Gu'). Baer's independent vectors v and w on line 7 correspond to our 𝑧 that the ∀𝑧 ∈ 𝑉 ranges over. The middle term (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) provides isolation to allow 𝐸 and 𝑇 to assume the same value without conflict. Closure is shown by hdmapcl 41005. If a separate auxiliary vector is known, hdmapval2 41007 provides a version without quantification. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑆‘𝑇) = (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑇⟩))))
Theorem	hdmapfnN 41004	Functionality of map from vectors to functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑆 Fn 𝑉)
Theorem	hdmapcl 41005	Closure of map from vectors to functionals with closed kernels. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑆‘𝑇) ∈ 𝐷)
Theorem	hdmapval2lem 41006*	Lemma for hdmapval2 41007. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑇) = 𝐹 ↔ ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑇})) → 𝐹 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑇⟩))))
Theorem	hdmapval2 41007	Value of map from vectors to functionals with a specific auxiliary vector. TODO: Would shorter proofs result if the .ne hypothesis were changed to two ≠ hypothesis? Consider hdmaplem1 40946 through hdmaplem4 40949, which would become obsolete. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑇})))    ⇒   ⊢ (𝜑 → (𝑆‘𝑇) = (𝐼‘⟨𝑋, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑋⟩), 𝑇⟩))
Theorem	hdmapval0 41008	Value of map from vectors to functionals at zero. Note: we use dvh3dim 40621 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 41019 could be derived from the other to shorten proof. (Contributed by NM, 17-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → (𝑆‘ 0 ) = 𝑄)
Theorem	hdmapeveclem 41009	Lemma for hdmapevec 41010. TODO: combine with hdmapevec 41010 if it shortens overall. (Contributed by NM, 16-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝐸})))    ⇒   ⊢ (𝜑 → (𝑆‘𝐸) = (𝐽‘𝐸))
Theorem	hdmapevec 41010	Value of map from vectors to functionals at the reference vector 𝐸. (Contributed by NM, 16-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → (𝑆‘𝐸) = (𝐽‘𝐸))
Theorem	hdmapevec2 41011	The inner product of the reference vector 𝐸 with itself is nonzero. This shows the inner product condition in the proof of Theorem 3.6 of [Holland95] p. 14 line 32, [ e , e ] ≠ 0 is satisfied. TODO: remove redundant hypothesis hdmapevec.j. (Contributed by NM, 1-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑆‘𝐸)‘𝐸) = 1 )
Theorem	hdmapval3lemN 41012	Value of map from vectors to functionals at arguments not colinear with the reference vector 𝐸. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑁‘{𝑇}) ≠ (𝑁‘{𝐸}))    &   ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ {(0g‘𝑈)}))    &   ⊢ (𝜑 → 𝑥 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑥 ∈ (𝑁‘{𝐸, 𝑇}))    ⇒   ⊢ (𝜑 → (𝑆‘𝑇) = (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑇⟩))
Theorem	hdmapval3N 41013	Value of map from vectors to functionals at arguments not colinear with the reference vector 𝐸. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑁‘{𝑇}) ≠ (𝑁‘{𝐸}))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑆‘𝑇) = (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑇⟩))
Theorem	hdmap10lem 41014	Lemma for hdmap10 41015. (Contributed by NM, 17-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑇})) = (𝐿‘{(𝑆‘𝑇)}))
Theorem	hdmap10 41015	Part 10 in [Baer] p. 48 line 33, (Ft)* = G(tS) in their notation (S = sigma). (Contributed by NM, 17-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑇})) = (𝐿‘{(𝑆‘𝑇)}))
Theorem	hdmap11lem1 41016	Lemma for hdmapadd 41018. (Contributed by NM, 26-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → 𝑧 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))    &   ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{𝐸}))    ⇒   ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌)))
Theorem	hdmap11lem2 41017	Lemma for hdmapadd 41018. (Contributed by NM, 26-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    ⇒   ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌)))
Theorem	hdmapadd 41018	Part 11 in [Baer] p. 48 line 35, (a+b)S = aS+bS in their notation (S = sigma). (Contributed by NM, 22-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌)))
Theorem	hdmapeq0 41019	Part of proof of part 12 in [Baer] p. 49 line 3. (Contributed by NM, 22-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑇) = 𝑄 ↔ 𝑇 = 0 ))
Theorem	hdmapnzcl 41020	Nonzero vector closure of map from vectors to functionals with closed kernels. (Contributed by NM, 27-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑆‘𝑇) ∈ (𝐷 ∖ {𝑄}))
Theorem	hdmapneg 41021	Part of proof of part 12 in [Baer] p. 49 line 4. The sigma map of a negative is the negative of the sigma map. (Contributed by NM, 24-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑀 = (invg‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐼 = (invg‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑆‘(𝑀‘𝑇)) = (𝐼‘(𝑆‘𝑇)))
Theorem	hdmapsub 41022	Part of proof of part 12 in [Baer] p. 49 line 5, (a-b)S = aS-bS in their notation (S = sigma). (Contributed by NM, 26-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (-g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑆‘(𝑋 − 𝑌)) = ((𝑆‘𝑋)𝑁(𝑆‘𝑌)))
Theorem	hdmap11 41023	Part of proof of part 12 in [Baer] p. 49 line 4, aS=bS iff a=b in their notation (S = sigma). The sigma map is one-to-one. (Contributed by NM, 26-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑋) = (𝑆‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	hdmaprnlem1N 41024	Part of proof of part 12 in [Baer] p. 49 line 10, Gu' ≠ Gs. Our (𝑁‘{𝑣}) is Baer's T. (Contributed by NM, 26-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄}))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    &   ⊢ (𝜑 → 𝑢 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣}))    ⇒   ⊢ (𝜑 → (𝐿‘{(𝑆‘𝑢)}) ≠ (𝐿‘{𝑠}))
Theorem	hdmaprnlem3N 41025	Part of proof of part 12 in [Baer] p. 49 line 15, T ≠ P. Our (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) is Baer's P, where P* = G(u'+s). (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄}))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    &   ⊢ (𝜑 → 𝑢 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣}))    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑣}) ≠ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})))
Theorem	hdmaprnlem3uN 41026	Part of proof of part 12 in [Baer] p. 49. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄}))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    &   ⊢ (𝜑 → 𝑢 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣}))    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑢}) ≠ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})))
Theorem	hdmaprnlem4tN 41027	Lemma for hdmaprnN 41039. TODO: This lemma doesn't quite pay for itself even though used six times. Maybe prove this directly instead. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄}))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    &   ⊢ (𝜑 → 𝑢 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣}))    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 }))    ⇒   ⊢ (𝜑 → 𝑡 ∈ 𝑉)
Theorem	hdmaprnlem4N 41028	Part of proof of part 12 in [Baer] p. 49 line 19. (T* =) (Ft)* = Gs. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄}))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    &   ⊢ (𝜑 → 𝑢 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣}))    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑡})) = (𝐿‘{𝑠}))
Theorem	hdmaprnlem6N 41029	Part of proof of part 12 in [Baer] p. 49 line 18, G(u'+s) = G(u'+t). (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄}))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    &   ⊢ (𝜑 → 𝑢 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣}))    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) = (𝑀‘(𝑁‘{(𝑢 + 𝑡)})))    ⇒   ⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) = (𝐿‘{((𝑆‘𝑢) ✚ (𝑆‘𝑡))}))
Theorem	hdmaprnlem7N 41030	Part of proof of part 12 in [Baer] p. 49 line 19, s-St ∈ G(u'+s) = P*. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄}))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    &   ⊢ (𝜑 → 𝑢 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣}))    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) = (𝑀‘(𝑁‘{(𝑢 + 𝑡)})))    ⇒   ⊢ (𝜑 → (𝑠(-g‘𝐶)(𝑆‘𝑡)) ∈ (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}))
Theorem	hdmaprnlem8N 41031	Part of proof of part 12 in [Baer] p. 49 line 19, s-St ∈ (Ft)* = T*. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄}))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    &   ⊢ (𝜑 → 𝑢 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣}))    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) = (𝑀‘(𝑁‘{(𝑢 + 𝑡)})))    ⇒   ⊢ (𝜑 → (𝑠(-g‘𝐶)(𝑆‘𝑡)) ∈ (𝑀‘(𝑁‘{𝑡})))
Theorem	hdmaprnlem9N 41032	Part of proof of part 12 in [Baer] p. 49 line 21, s=S(t). TODO: we seem to be going back and forth with mapd11 40814 and mapdcnv11N 40834. Use better hypotheses and/or theorems? (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄}))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    &   ⊢ (𝜑 → 𝑢 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣}))    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) = (𝑀‘(𝑁‘{(𝑢 + 𝑡)})))    ⇒   ⊢ (𝜑 → 𝑠 = (𝑆‘𝑡))
Theorem	hdmaprnlem3eN 41033*	Lemma for hdmaprnN 41039. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄}))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    &   ⊢ (𝜑 → 𝑢 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣}))    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ + = (+g‘𝑈)    ⇒   ⊢ (𝜑 → ∃𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) = (𝑀‘(𝑁‘{(𝑢 + 𝑡)})))
Theorem	hdmaprnlem10N 41034*	Lemma for hdmaprnN 41039. Show 𝑠 is in the range of 𝑆. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄}))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    &   ⊢ (𝜑 → 𝑢 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣}))    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ + = (+g‘𝑈)    ⇒   ⊢ (𝜑 → ∃𝑡 ∈ 𝑉 (𝑆‘𝑡) = 𝑠)
Theorem	hdmaprnlem11N 41035*	Lemma for hdmaprnN 41039. Show 𝑠 is in the range of 𝑆. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄}))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    &   ⊢ (𝜑 → 𝑢 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣}))    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ + = (+g‘𝑈)    ⇒   ⊢ (𝜑 → 𝑠 ∈ ran 𝑆)
Theorem	hdmaprnlem15N 41036*	Lemma for hdmaprnN 41039. Eliminate 𝑢. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 0 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑣 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}))    ⇒   ⊢ (𝜑 → 𝑠 ∈ ran 𝑆)
Theorem	hdmaprnlem16N 41037	Lemma for hdmaprnN 41039. Eliminate 𝑣. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 0 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ { 0 }))    ⇒   ⊢ (𝜑 → 𝑠 ∈ ran 𝑆)
Theorem	hdmaprnlem17N 41038	Lemma for hdmaprnN 41039. Include zero. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 0 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑠 ∈ 𝐷)    ⇒   ⊢ (𝜑 → 𝑠 ∈ ran 𝑆)
Theorem	hdmaprnN 41039	Part of proof of part 12 in [Baer] p. 49 line 21, As=B. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ran 𝑆 = 𝐷)
Theorem	hdmapf1oN 41040	Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 41018, this shows the map is an automorphism from the additive group of vectors to the additive group of functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑆:𝑉–1-1-onto→𝐷)
Theorem	hdmap14lem1a 41041	Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐹 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐿‘{(𝑆‘𝑋)}) = (𝐿‘{(𝑆‘(𝐹 · 𝑋))}))
Theorem	hdmap14lem2a 41042*	Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include 𝐹 = 0 so it can be used in hdmap14lem10 41052. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem1 41043	Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑄 = (0g‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ∖ {𝑍}))    ⇒   ⊢ (𝜑 → (𝐿‘{(𝑆‘𝑋)}) = (𝐿‘{(𝑆‘(𝐹 · 𝑋))}))
Theorem	hdmap14lem2N 41044*	Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include 𝐹 = 𝑍 so it can be used in hdmap14lem10 41052. (Contributed by NM, 31-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑄 = (0g‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ∖ {𝑍}))    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ (𝐴 ∖ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem3 41045*	Prior to part 14 in [Baer] p. 49, line 26. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑄 = (0g‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ∖ {𝑍}))    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ (𝐴 ∖ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem4a 41046*	Simplify (𝐴 ∖ {𝑄}) in hdmap14lem3 41045 to provide a slightly simpler definition later. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑄 = (0g‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ∖ {𝑍}))    ⇒   ⊢ (𝜑 → (∃!𝑔 ∈ (𝐴 ∖ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) ↔ ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋))))
Theorem	hdmap14lem4 41047*	Simplify (𝐴 ∖ {𝑄}) in hdmap14lem3 41045 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 41046 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 41046 into this one. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑄 = (0g‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ∖ {𝑍}))    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem6 41048*	Case where 𝐹 is zero. (Contributed by NM, 1-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑄 = (0g‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 = 𝑍)    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem7 41049*	Combine cases of 𝐹. TODO: Can this be done at once in hdmap14lem3 41045, in order to get rid of hdmap14lem6 41048? Perhaps modify lspsneu 20882 to become ∃!𝑘 ∈ 𝐾 instead of ∃!𝑘 ∈ (𝐾 ∖ { 0 })? (Contributed by NM, 1-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem8 41050	Part of proof of part 14 in [Baer] p. 49 lines 33-35. (Contributed by NM, 1-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = (𝐺 ∙ (𝑆‘𝑋)))    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑌)) = (𝐼 ∙ (𝑆‘𝑌)))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → 𝐽 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑆‘(𝐹 · (𝑋 + 𝑌))) = (𝐽 ∙ (𝑆‘(𝑋 + 𝑌))))    ⇒   ⊢ (𝜑 → ((𝐽 ∙ (𝑆‘𝑋)) ✚ (𝐽 ∙ (𝑆‘𝑌))) = ((𝐺 ∙ (𝑆‘𝑋)) ✚ (𝐼 ∙ (𝑆‘𝑌))))
Theorem	hdmap14lem9 41051	Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 1-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = (𝐺 ∙ (𝑆‘𝑋)))    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑌)) = (𝐼 ∙ (𝑆‘𝑌)))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → 𝐽 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑆‘(𝐹 · (𝑋 + 𝑌))) = (𝐽 ∙ (𝑆‘(𝑋 + 𝑌))))    ⇒   ⊢ (𝜑 → 𝐺 = 𝐼)
Theorem	hdmap14lem10 41052	Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 3-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = (𝐺 ∙ (𝑆‘𝑋)))    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑌)) = (𝐼 ∙ (𝑆‘𝑌)))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → 𝐺 = 𝐼)
Theorem	hdmap14lem11 41053	Part of proof of part 14 in [Baer] p. 50 line 3. (Contributed by NM, 3-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = (𝐺 ∙ (𝑆‘𝑋)))    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑌)) = (𝐼 ∙ (𝑆‘𝑌)))    ⇒   ⊢ (𝜑 → 𝐺 = 𝐼)
Theorem	hdmap14lem12 41054*	Lemma for proof of part 14 in [Baer] p. 50. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑆‘(𝐹 · 𝑋)) = (𝐺 ∙ (𝑆‘𝑋)) ↔ ∀𝑦 ∈ (𝑉 ∖ { 0 })(𝑆‘(𝐹 · 𝑦)) = (𝐺 ∙ (𝑆‘𝑦))))
Theorem	hdmap14lem13 41055*	Lemma for proof of part 14 in [Baer] p. 50. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑆‘(𝐹 · 𝑋)) = (𝐺 ∙ (𝑆‘𝑋)) ↔ ∀𝑦 ∈ 𝑉 (𝑆‘(𝐹 · 𝑦)) = (𝐺 ∙ (𝑆‘𝑦))))
Theorem	hdmap14lem14 41056*	Part of proof of part 14 in [Baer] p. 50 line 3. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ 𝐴 ∀𝑥 ∈ 𝑉 (𝑆‘(𝐹 · 𝑥)) = (𝑔 ∙ (𝑆‘𝑥)))
Theorem	hdmap14lem15 41057*	Part of proof of part 14 in [Baer] p. 50 line 3. Convert scalar base of dual to scalar base of vector space. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ 𝐵 ∀𝑥 ∈ 𝑉 (𝑆‘(𝐹 · 𝑥)) = (𝑔 ∙ (𝑆‘𝑥)))
Syntax	chg 41058	Extend class notation with g-map.
class HGMap
Definition	df-hgmap 41059*	Define map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
⊢ HGMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 ∀𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠 ‘𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚‘𝑣))))}))
Theorem	hgmapffval 41060*	Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑋 → (HGMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 ∀𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠 ‘𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚‘𝑣))))}))
Theorem	hgmapfval 41061*	Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑀 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐼 = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 ∀𝑣 ∈ 𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 ∙ (𝑀‘𝑣)))))
Theorem	hgmapval 41062*	Value of map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. Function sigma of scalar f in part 14 of [Baer] p. 50 line 4. TODO: variable names are inherited from older version. Maybe make more consistent with hdmap14lem15 41057. (Contributed by NM, 25-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑀 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) = (℩𝑦 ∈ 𝐵 ∀𝑣 ∈ 𝑉 (𝑀‘(𝑋 · 𝑣)) = (𝑦 ∙ (𝑀‘𝑣))))
Theorem	hgmapfnN 41063	Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐺 Fn 𝐵)
Theorem	hgmapcl 41064	Closure of scalar sigma map i.e. the map from the vector space scalar base to the dual space scalar base. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘𝐹) ∈ 𝐵)
Theorem	hgmapdcl 41065	Closure of the vector space to dual space scalar map, in the scalar sigma map. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑄 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑄)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘𝐹) ∈ 𝐴)
Theorem	hgmapvs 41066	Part 15 of [Baer] p. 50 line 6. Also line 15 in [Holland95] p. 14. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = ((𝐺‘𝐹) ∙ (𝑆‘𝑋)))
Theorem	hgmapval0 41067	Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → (𝐺‘ 0 ) = 0 )
Theorem	hgmapval1 41068	Value of the scalar sigma map at one. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → (𝐺‘ 1 ) = 1 )
Theorem	hgmapadd 41069	Part 15 of [Baer] p. 50 line 13. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘(𝑋 + 𝑌)) = ((𝐺‘𝑋) + (𝐺‘𝑌)))
Theorem	hgmapmul 41070	Part 15 of [Baer] p. 50 line 16. The multiplication is reversed after converting to the dual space scalar to the vector space scalar. (Contributed by NM, 7-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘(𝑋 · 𝑌)) = ((𝐺‘𝑌) · (𝐺‘𝑋)))
Theorem	hgmaprnlem1N 41071	Lemma for hgmaprnN 41076. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑡 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑠 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆‘𝑠) = (𝑧 ∙ (𝑆‘𝑡)))    &   ⊢ (𝜑 → 𝑘 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑠 = (𝑘 · 𝑡))    ⇒   ⊢ (𝜑 → 𝑧 ∈ ran 𝐺)
Theorem	hgmaprnlem2N 41072	Lemma for hgmaprnN 41076. Part 15 of [Baer] p. 50 line 20. We only require a subset relation, rather than equality, so that the case of zero 𝑧 is taken care of automatically. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑡 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑠 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆‘𝑠) = (𝑧 ∙ (𝑆‘𝑡)))    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LSpan‘𝐶)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑠}) ⊆ (𝑁‘{𝑡}))
Theorem	hgmaprnlem3N 41073*	Lemma for hgmaprnN 41076. Eliminate 𝑘. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑡 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑠 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆‘𝑠) = (𝑧 ∙ (𝑆‘𝑡)))    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LSpan‘𝐶)    ⇒   ⊢ (𝜑 → 𝑧 ∈ ran 𝐺)
Theorem	hgmaprnlem4N 41074*	Lemma for hgmaprnN 41076. Eliminate 𝑠. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑡 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → 𝑧 ∈ ran 𝐺)
Theorem	hgmaprnlem5N 41075	Lemma for hgmaprnN 41076. Eliminate 𝑡. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑧 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑧 ∈ ran 𝐺)
Theorem	hgmaprnN 41076	Part of proof of part 16 in [Baer] p. 50 line 23, Fs=G, except that we use the original vector space scalars for the range. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ran 𝐺 = 𝐵)
Theorem	hgmap11 41077	The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐺‘𝑋) = (𝐺‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	hgmapf1oN 41078	The scalar sigma map is a one-to-one onto function. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐵)
Theorem	hgmapeq0 41079	The scalar sigma map is zero iff its argument is zero. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐺‘𝑋) = 0 ↔ 𝑋 = 0 ))
Theorem	hdmapipcl 41080	The inner product (Hermitian form) (𝑋, 𝑌) will be defined as ((𝑆‘𝑌)‘𝑋). Show closure. (Contributed by NM, 7-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑌)‘𝑋) ∈ 𝐵)
Theorem	hdmapln1 41081	Linearity property that will be used for inner product. TODO: try to combine hypotheses in hdmap*ln* series. (Contributed by NM, 7-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑍)‘((𝐴 · 𝑋) + 𝑌)) = ((𝐴 × ((𝑆‘𝑍)‘𝑋)) ⨣ ((𝑆‘𝑍)‘𝑌)))
Theorem	hdmaplna1 41082	Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 + 𝑌)) = (((𝑆‘𝑍)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑌)))
Theorem	hdmaplns1 41083	Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝑁 = (-g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 − 𝑌)) = (((𝑆‘𝑍)‘𝑋)𝑁((𝑆‘𝑍)‘𝑌)))
Theorem	hdmaplnm1 41084	Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑌)‘(𝐴 · 𝑋)) = (𝐴 × ((𝑆‘𝑌)‘𝑋)))
Theorem	hdmaplna2 41085	Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘(𝑌 + 𝑍))‘𝑋) = (((𝑆‘𝑌)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑋)))
Theorem	hdmapglnm2 41086	g-linear property of second (inner product) argument. Line 19 in [Holland95] p. 14. (Contributed by NM, 10-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑆‘(𝐴 · 𝑌))‘𝑋) = (((𝑆‘𝑌)‘𝑋) × (𝐺‘𝐴)))
Theorem	hdmapgln2 41087	g-linear property that will be used for inner product. (Contributed by NM, 14-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑆‘((𝐴 · 𝑌) + 𝑍))‘𝑋) = ((((𝑆‘𝑌)‘𝑋) × (𝐺‘𝐴)) ⨣ ((𝑆‘𝑍)‘𝑋)))
Theorem	hdmaplkr 41088	Kernel of the vector to dual map. Line 16 in [Holland95] p. 14. TODO: eliminate 𝐹 hypothesis. (Contributed by NM, 9-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝑌 = (LKer‘𝑈)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑌‘(𝑆‘𝑋)) = (𝑂‘{𝑋}))
Theorem	hdmapellkr 41089	Membership in the kernel (as shown by hdmaplkr 41088) of the vector to dual map. Line 17 in [Holland95] p. 14. (Contributed by NM, 16-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑌) = 0 ↔ 𝑌 ∈ (𝑂‘{𝑋})))
Theorem	hdmapip0 41090	Zero property that will be used for inner product. (Contributed by NM, 9-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑋) = 𝑍 ↔ 𝑋 = 0 ))
Theorem	hdmapip1 41091	Construct a proportional vector 𝑌 whose inner product with the original 𝑋 equals one. (Contributed by NM, 13-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invr‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ 𝑌 = ((𝑁‘((𝑆‘𝑋)‘𝑋)) · 𝑋)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑋)‘𝑌) = 1 )
Theorem	hdmapip0com 41092	Commutation property of Baer's sigma map (Holland's A map). Line 20 of [Holland95] p. 14. Also part of Lemma 1 of [Baer] p. 110 line 7. (Contributed by NM, 9-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑌) = 0 ↔ ((𝑆‘𝑌)‘𝑋) = 0 ))
Theorem	hdmapinvlem1 41093	Line 27 in [Baer] p. 110. We use 𝐶 for Baer's u. Our unit vector 𝐸 has the required properties for his w by hdmapevec2 41011. Our ((𝑆‘𝐸)‘𝐶) means the inner product ⟨𝐶, 𝐸⟩ i.e. his f(u,w) (note argument reversal). (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    ⇒   ⊢ (𝜑 → ((𝑆‘𝐸)‘𝐶) = 0 )
Theorem	hdmapinvlem2 41094	Line 28 in [Baer] p. 110, 0 = f(w,u). (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    ⇒   ⊢ (𝜑 → ((𝑆‘𝐶)‘𝐸) = 0 )
Theorem	hdmapinvlem3 41095	Line 30 in [Baer] p. 110, f(sw + u, tw - v) = 0. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐼 × (𝐺‘𝐽)) = ((𝑆‘𝐷)‘𝐶))    ⇒   ⊢ (𝜑 → ((𝑆‘((𝐽 · 𝐸) − 𝐷))‘((𝐼 · 𝐸) + 𝐶)) = 0 )
Theorem	hdmapinvlem4 41096	Part 1.1 of Proposition 1 of [Baer] p. 110. We use 𝐶, 𝐷, 𝐼, and 𝐽 for Baer's u, v, s, and t. Our unit vector 𝐸 has the required properties for his w by hdmapevec2 41011. Our ((𝑆‘𝐷)‘𝐶) means his f(u,v) (note argument reversal). (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐼 × (𝐺‘𝐽)) = ((𝑆‘𝐷)‘𝐶))    ⇒   ⊢ (𝜑 → (𝐽 × (𝐺‘𝐼)) = ((𝑆‘𝐶)‘𝐷))
Theorem	hdmapglem5 41097	Part 1.2 in [Baer] p. 110 line 34, f(u,v) alpha = f(v,u). (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘((𝑆‘𝐷)‘𝐶)) = ((𝑆‘𝐶)‘𝐷))
Theorem	hgmapvvlem1 41098	Involution property of scalar sigma map. Line 10 in [Baer] p. 111, t sigma squared = t. Our 𝐸, 𝐶, 𝐷, 𝑌, 𝑋 correspond to Baer's w, h, k, s, t. (Contributed by NM, 13-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invr‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → ((𝑆‘𝐷)‘𝐶) = 1 )    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑌 × (𝐺‘𝑋)) = 1 )    ⇒   ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋)
Theorem	hgmapvvlem2 41099	Lemma for hgmapvv 41101. Eliminate 𝑌 (Baer's s). (Contributed by NM, 13-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invr‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → ((𝑆‘𝐷)‘𝐶) = 1 )    ⇒   ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋)
Theorem	hgmapvvlem3 41100	Lemma for hgmapvv 41101. Eliminate ((𝑆‘𝐷)‘𝐶) = 1 (Baer's f(h,k)=1). (Contributed by NM, 13-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invr‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋)