P. 427 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42601-42700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mapdh8i 42601*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 11-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇}))    &   ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑇}))    &   ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑇}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑌, (𝐼‘⟨𝑋, 𝐹, 𝑌⟩), 𝑇⟩) = (𝐼‘⟨𝑍, (𝐼‘⟨𝑋, 𝐹, 𝑍⟩), 𝑇⟩))
Theorem	mapdh8j 42602*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇}))    &   ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑇}))    &   ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑌, (𝐼‘⟨𝑋, 𝐹, 𝑌⟩), 𝑇⟩) = (𝐼‘⟨𝑍, (𝐼‘⟨𝑋, 𝐹, 𝑍⟩), 𝑇⟩))
Theorem	mapdh8 42603*	Part (8) in [Baer] p. 48. Given a reference vector 𝑋, the value of function 𝐼 at a vector 𝑇 is independent of the choice of auxiliary vectors 𝑌 and 𝑍. Unlike Baer's, our version does not require 𝑋, 𝑌, and 𝑍 to be independent, and also is defined for all 𝑌 and 𝑍 that are not colinear with 𝑋 or 𝑇. We do this to make the definition of Baer's sigma function more straightforward. (This part eliminates 𝑇 ≠ 0.) (Contributed by NM, 13-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇}))    &   ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑇}))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑌, (𝐼‘⟨𝑋, 𝐹, 𝑌⟩), 𝑇⟩) = (𝐼‘⟨𝑍, (𝐼‘⟨𝑋, 𝐹, 𝑍⟩), 𝑇⟩))
Theorem	mapdh9a 42604*	Lemma for part (9) in [Baer] p. 48. TODO: why is this 50% larger than mapdh9aOLDN 42605? (Contributed by NM, 14-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑋, 𝐹, 𝑧⟩), 𝑇⟩)))
Theorem	mapdh9aOLDN 42605*	Lemma for part (9) in [Baer] p. 48. (Contributed by NM, 14-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇}) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑋, 𝐹, 𝑧⟩), 𝑇⟩)))
Syntax	chdma1 42606	Extend class notation with preliminary map from vectors to functionals in the closed kernel dual space.
class HDMap1
Syntax	chdma 42607	Extend class notation with map from vectors to functionals in the closed kernel dual space.
class HDMap
Definition	df-hdmap1 42608*	Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 42611 description for more details. (Contributed by NM, 14-May-2015.)
⊢ HDMap1 = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))}))
Definition	df-hdmap 42609*	Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 42642 description for more details. (Contributed by NM, 15-May-2015.)
⊢ HDMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
Theorem	hdmap1ffval 42610*	Preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 14-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑋 → (HDMap1‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))}))
Theorem	hdmap1fval 42611*	Preliminary map from vectors to functionals in the closed kernel dual space. TODO: change span 𝐽 to the convention 𝐿 for this section. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))))
Theorem	hdmap1vallem 42612*	Value of preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ ((𝑉 × 𝐷) × 𝑉))    ⇒   ⊢ (𝜑 → (𝐼‘𝑇) = if((2nd ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑇)) − (2nd ‘𝑇))})) = (𝐽‘{((2nd ‘(1st ‘𝑇))𝑅ℎ)})))))
Theorem	hdmap1val 42613*	Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval 42539.) TODO: change 𝐼 = (𝑥 ∈ V ↦... to (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌 > ) =... in e.g. mapdh8 42603 to shorten proofs with no $d on 𝑥. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = if(𝑌 = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)})))))
Theorem	hdmap1val0 42614	Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 42540.) (Contributed by NM, 17-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 0 ⟩) = 𝑄)
Theorem	hdmap1val2 42615*	Value of preliminary map from vectors to functionals in the closed kernel dual space, for nonzero 𝑌. (Contributed by NM, 16-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐿‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐿‘{(𝐹𝑅ℎ)}))))
Theorem	hdmap1eq 42616	The defining equation for h(x,x',y)=y' in part (2) in [Baer] p. 45 line 24. (Contributed by NM, 16-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    ⇒   ⊢ (𝜑 → ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺 ↔ ((𝑀‘(𝑁‘{𝑌})) = (𝐿‘{𝐺}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐿‘{(𝐹𝑅𝐺)}))))
Theorem	hdmap1cbv 42617*	Frequently used lemma to change bound variables in 𝐿 hypothesis. (Contributed by NM, 15-May-2015.)
⊢ 𝐿 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    ⇒   ⊢ 𝐿 = (𝑦 ∈ V ↦ if((2nd ‘𝑦) = 0 , 𝑄, (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑦)) − (2nd ‘𝑦))})) = (𝐽‘{((2nd ‘(1st ‘𝑦))𝑅𝑖)})))))
Theorem	hdmap1valc 42618*	Connect the value of the preliminary map from vectors to functionals 𝐼 to the hypothesis 𝐿 used by earlier theorems. Note: the 𝑋 ∈ (𝑉 ∖ { 0 }) hypothesis could be the more general 𝑋 ∈ 𝑉 but the former will be easier to use. TODO: use the 𝐼 function directly in those theorems, so this theorem becomes unnecessary? TODO: The hdmap1cbv 42617 is probably unnecessary, but it would mean different $d's later on. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ 𝐿 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = (𝐿‘⟨𝑋, 𝐹, 𝑌⟩))
Theorem	hdmap1cl 42619	Convert closure theorem mapdhcl 42542 to use HDMap1 function. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ∈ 𝐷)
Theorem	hdmap1eq2 42620	Convert mapdheq2 42544 to use HDMap1 function. (Contributed by NM, 16-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑋⟩) = 𝐹)
Theorem	hdmap1eq4N 42621	Convert mapdheq4 42547 to use HDMap1 function. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺)    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑍⟩) = 𝐵)
Theorem	hdmap1l6lem1 42622	Lemma for hdmap1l6 42636. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺)    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐸)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − (𝑌 + 𝑍))})) = (𝐿‘{(𝐹𝑅(𝐺 ✚ 𝐸))}))
Theorem	hdmap1l6lem2 42623	Lemma for hdmap1l6 42636. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺)    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐸)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑌 + 𝑍)})) = (𝐿‘{(𝐺 ✚ 𝐸)}))
Theorem	hdmap1l6a 42624	Lemma for hdmap1l6 42636. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺)    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐸)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	hdmap1l6b0N 42625	Lemmma for hdmap1l6 42636. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ (𝑁‘{𝑌, 𝑍})) = { 0 })    ⇒   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
Theorem	hdmap1l6b 42626	Lemmma for hdmap1l6 42636. (Contributed by NM, 24-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → 𝑌 = 0 )    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	hdmap1l6c 42627	Lemmma for hdmap1l6 42636. (Contributed by NM, 24-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 = 0 )    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	hdmap1l6d 42628	Lemmma for hdmap1l6 42636. (Contributed by NM, 1-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩)))
Theorem	hdmap1l6e 42629	Lemmma for hdmap1l6 42636. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, ((𝑤 + 𝑌) + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, (𝑤 + 𝑌)⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	hdmap1l6f 42630	Lemmma for hdmap1l6 42636. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑤 + 𝑌)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑌⟩)))
Theorem	hdmap1l6g 42631	Lemmma for hdmap1l6 42636. Part (6) of [Baer] p. 47 line 39. (Contributed by NM, 1-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩)) = (((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑌⟩)) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	hdmap1l6h 42632	Lemmma for hdmap1l6 42636. Part (6) of [Baer] p. 48 line 2. (Contributed by NM, 1-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	hdmap1l6i 42633	Lemmma for hdmap1l6 42636. Eliminate auxiliary vector 𝑤. (Contributed by NM, 1-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	hdmap1l6j 42634	Lemmma for hdmap1l6 42636. Eliminate (𝑁 { Y } ) = ( N {𝑍}) hypothesis. (Contributed by NM, 1-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	hdmap1l6k 42635	Lemmma for hdmap1l6 42636. Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	hdmap1l6 42636	Part (6) of [Baer] p. 47 line 6. Note that we use ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) which is equivalent to Baer's "Fx ∩ (Fy + Fz)" by lspdisjb 21287. (Convert mapdh6N 42562 to use the function HDMap1.) (Contributed by NM, 17-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	hdmap1eulem 42637*	Lemma for hdmap1eu 42639. TODO: combine with hdmap1eu 42639 or at least share some hypotheses. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ 𝐿 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    ⇒   ⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑋, 𝐹, 𝑧⟩), 𝑇⟩)))
Theorem	hdmap1eulemOLDN 42638*	Lemma for hdmap1euOLDN 42640. TODO: combine with hdmap1euOLDN 42640 or at least share some hypotheses. (Contributed by NM, 15-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ 𝐿 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    ⇒   ⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇}) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑋, 𝐹, 𝑧⟩), 𝑇⟩)))
Theorem	hdmap1eu 42639*	Convert mapdh9a 42604 to use the HDMap1 notation. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑋, 𝐹, 𝑧⟩), 𝑇⟩)))
Theorem	hdmap1euOLDN 42640*	Convert mapdh9aOLDN 42605 to use the HDMap1 notation. (Contributed by NM, 15-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇}) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑋, 𝐹, 𝑧⟩), 𝑇⟩)))
Theorem	hdmapffval 42641*	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 42642*	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 42643*	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 41927). (𝐽‘𝐸) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap 42584 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 42645. If a separate auxiliary vector is known, hdmapval2 42647 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 42644	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 42645	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 42646*	Lemma for hdmapval2 42647. (Contributed by NM, 15-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑇) = 𝐹 ↔ ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑇})) → 𝐹 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑇⟩))))
Theorem	hdmapval2 42647	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 42586 through hdmaplem4 42589, 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 42648	Value of map from vectors to functionals at zero. Note: we use dvh3dim 42261 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 42659 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 42649	Lemma for hdmapevec 42650. TODO: combine with hdmapevec 42650 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 42650	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 42651	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 42652	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 42653	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 42654	Lemma for hdmap10 42655. (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 42655	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 42656	Lemma for hdmapadd 42658. (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 42657	Lemma for hdmapadd 42658. (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 42658	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 42659	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 42660	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 42661	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 42662	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 42663	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 42664	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 42665	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 42666	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 42667	Lemma for hdmaprnN 42679. 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 42668	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 42669	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 42670	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 42671	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 42672	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 42454 and mapdcnv11N 42474. 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 42673*	Lemma for hdmaprnN 42679. (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 42674*	Lemma for hdmaprnN 42679. 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 42675*	Lemma for hdmaprnN 42679. 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 42676*	Lemma for hdmaprnN 42679. 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 42677	Lemma for hdmaprnN 42679. 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 42678	Lemma for hdmaprnN 42679. 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 42679	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 42680	Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 42658, 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 42681	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 42682*	Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include 𝐹 = 0 so it can be used in hdmap14lem10 42692. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem1 42683	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 42684*	Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include 𝐹 = 𝑍 so it can be used in hdmap14lem10 42692. (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 42685*	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 42686*	Simplify (𝐴 ∖ {𝑄}) in hdmap14lem3 42685 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 42687*	Simplify (𝐴 ∖ {𝑄}) in hdmap14lem3 42685 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 42686 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 42686 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 42688*	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 42689*	Combine cases of 𝐹. TODO: Can this be done at once in hdmap14lem3 42685, in order to get rid of hdmap14lem6 42688? Perhaps modify lspsneu 21284 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 42690	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 42691	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 42692	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 42693	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 42694*	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 42695*	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 42696*	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 42697*	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 42698	Extend class notation with g-map.
class HGMap
Definition	df-hgmap 42699*	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 42700*	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‘𝐾)‘𝑤))(𝑚‘𝑣))))}))