P. 418 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41701-41800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mapdindp3 41701	Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑤 + 𝑌)}))
Theorem	mapdindp4 41702	Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, (𝑤 + 𝑌)}))
Theorem	mapdhval 41703*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐸)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = if(𝑌 = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)})))))
Theorem	mapdhval0 41704*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 0 ⟩) = 𝑄)
Theorem	mapdhval2 41705*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)}))))
Theorem	mapdhcl 41706*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ∈ 𝐷)
Theorem	mapdheq 41707*	Lemmma for ~? mapdh . The defining equation for h(x,x',y)=y' in part (2) in [Baer] p. 45 line 24. (Contributed by NM, 4-Apr-2015.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺 ↔ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅𝐺)}))))
Theorem	mapdheq2 41708*	Lemmma for ~? mapdh . One direction of part (2) in [Baer] p. 45. (Contributed by NM, 4-Apr-2015.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺 → (𝐼‘⟨𝑌, 𝐺, 𝑋⟩) = 𝐹))
Theorem	mapdheq2biN 41709*	Lemmma for ~? mapdh . Part (2) in [Baer] p. 45. The bidirectional version of mapdheq2 41708 seems to require an additional hypothesis not mentioned in Baer. TODO fix ref. TODO: We probably don't need this; delete if never used. (Contributed by NM, 4-Apr-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}))    ⇒   ⊢ (𝜑 → ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺 ↔ (𝐼‘⟨𝑌, 𝐺, 𝑋⟩) = 𝐹))
Theorem	mapdheq4lem 41710*	Lemma for mapdheq4 41711. Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺)    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐸)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑌 − 𝑍)})) = (𝐽‘{(𝐺𝑅𝐸)}))
Theorem	mapdheq4 41711*	Lemma for ~? mapdh . Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺)    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐸)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑍⟩) = 𝐸)
Theorem	mapdh6lem1N 41712*	Lemma for mapdh6N 41726. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺)    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐸)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − (𝑌 + 𝑍))})) = (𝐽‘{(𝐹𝑅(𝐺 ✚ 𝐸))}))
Theorem	mapdh6lem2N 41713*	Lemma for mapdh6N 41726. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺)    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐸)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑌 + 𝑍)})) = (𝐽‘{(𝐺 ✚ 𝐸)}))
Theorem	mapdh6aN 41714*	Lemma for mapdh6N 41726. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺)    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐸)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	mapdh6b0N 41715*	Lemmma for mapdh6N 41726. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ (𝑁‘{𝑌, 𝑍})) = { 0 })    ⇒   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
Theorem	mapdh6bN 41716*	Lemmma for mapdh6N 41726. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑌 = 0 )    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	mapdh6cN 41717*	Lemmma for mapdh6N 41726. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 = 0 )    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	mapdh6dN 41718*	Lemmma for mapdh6N 41726. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩)))
Theorem	mapdh6eN 41719*	Lemmma for mapdh6N 41726. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, ((𝑤 + 𝑌) + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, (𝑤 + 𝑌)⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	mapdh6fN 41720*	Lemmma for mapdh6N 41726. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑤 + 𝑌)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑌⟩)))
Theorem	mapdh6gN 41721*	Lemmma for mapdh6N 41726. Part (6) of [Baer] p. 47 line 39. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩)) = (((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑌⟩)) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	mapdh6hN 41722*	Lemmma for mapdh6N 41726. Part (6) of [Baer] p. 48 line 2. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	mapdh6iN 41723*	Lemmma for mapdh6N 41726. Eliminate auxiliary vector 𝑤. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	mapdh6jN 41724*	Lemmma for mapdh6N 41726. Eliminate (𝑁‘{𝑌}) = (𝑁‘{𝑍}) hypothesis. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	mapdh6kN 41725*	Lemmma for mapdh6N 41726. Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑈)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	mapdh6N 41726*	Part (6) of [Baer] p. 47 line 6. Note that we use ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) which is equivalent to Baer's "Fx ∩ (Fy + Fz)" by lspdisjb 21051. TODO: If disjoint variable conditions with 𝐼 and 𝜑 become a problem later, use cbv* theorems on 𝐼 variables here to get rid of them. Maybe reorder hypotheses in lemmas to the more consistent order of this theorem, so they can be shared with this theorem. TODO: may be deleted (with its lemmas), if not needed, in view of hdmap1l6 41800. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))
Theorem	mapdh7eN 41727*	Part (7) of [Baer] p. 48 line 10 (5 of 6 cases). (Note: 1 of 6 and 2 of 6 are hypotheses a and b.) (Contributed by NM, 2-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 }))    &   ⊢ (𝜑 → 𝑣 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑢}) ≠ (𝑁‘{𝑣}))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑢, 𝑣}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑢, 𝐹, 𝑤⟩) = 𝐸)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑤, 𝐸, 𝑢⟩) = 𝐹)
Theorem	mapdh7cN 41728*	Part (7) of [Baer] p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-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 }))    &   ⊢ (𝜑 → 𝑣 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑢}) ≠ (𝑁‘{𝑣}))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑢, 𝑣}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑢, 𝐹, 𝑣⟩) = 𝐺)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑣, 𝐺, 𝑢⟩) = 𝐹)
Theorem	mapdh7dN 41729*	Part (7) of [Baer] p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-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 }))    &   ⊢ (𝜑 → 𝑣 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑢}) ≠ (𝑁‘{𝑣}))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑢, 𝑣}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑢, 𝐹, 𝑣⟩) = 𝐺)    &   ⊢ (𝜑 → (𝐼‘⟨𝑢, 𝐹, 𝑤⟩) = 𝐸)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑣, 𝐺, 𝑤⟩) = 𝐸)
Theorem	mapdh7fN 41730*	Part (7) of [Baer] p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-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 }))    &   ⊢ (𝜑 → 𝑣 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑢}) ≠ (𝑁‘{𝑣}))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑢, 𝑣}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑢, 𝐹, 𝑣⟩) = 𝐺)    &   ⊢ (𝜑 → (𝐼‘⟨𝑢, 𝐹, 𝑤⟩) = 𝐸)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑤, 𝐸, 𝑣⟩) = 𝐺)
Theorem	mapdh75e 41731*	Part (7) of [Baer] p. 48 line 10 (5 of 6 cases). 𝑋, 𝑌, 𝑍 are Baer's u, v, w. (Note: Cases 1 of 6 and 2 of 6 are hypotheses mapdh75b here and mapdh75a in mapdh75cN 41732.) (Contributed by NM, 2-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 }))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑍, 𝐸, 𝑋⟩) = 𝐹)
Theorem	mapdh75cN 41732*	Part (7) of [Baer] p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-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 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑋⟩) = 𝐹)
Theorem	mapdh75d 41733*	Part (7) of [Baer] p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-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	mapdh75fN 41734*	Part (7) of [Baer] p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-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 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑍, 𝐸, 𝑌⟩) = 𝐺)
Syntax	chvm 41735	Extend class notation with vector to dual map.
class HVMap
Definition	df-hvmap 41736*	Extend class notation with a map from each nonzero vector 𝑥 to a unique nonzero functional in the closed kernel dual space. (We could extend it to include the zero vector, but that is unnecessary for our purposes.) TODO: This pattern is used several times earlier, e.g., lcf1o 41530, dochfl1 41455- should we update those to use this definition? (Contributed by NM, 23-Mar-2015.)
⊢ HVMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (℩𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))))
Theorem	hvmapffval 41737*	Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑋 → (HVMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖ {(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝐾)‘𝑤))𝑥)))))))
Theorem	hvmapfval 41738*	Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑀 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥))))))
Theorem	hvmapval 41739*	Value of map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) = (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑋})𝑣 = (𝑡 + (𝑗 · 𝑋)))))
Theorem	hvmapvalvalN 41740*	Value of value of map (i.e. functional value) from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑀‘𝑋)‘𝑌) = (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑋})𝑌 = (𝑡 + (𝑗 · 𝑋))))
Theorem	hvmapidN 41741	The value of the vector to functional map, at the vector, is one. (Contributed by NM, 23-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 1 = (1r‘𝑆)    &   ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → ((𝑀‘𝑋)‘𝑋) = 1 )
Theorem	hvmap1o 41742*	The vector to functional map provides a bijection from nonzero vectors 𝑉 to nonzero functionals with closed kernels 𝐶. (Contributed by NM, 27-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑀:(𝑉 ∖ { 0 })–1-1-onto→(𝐶 ∖ {𝑄}))
Theorem	hvmapclN 41743*	Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (0g‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ (𝐶 ∖ {𝑄}))
Theorem	hvmap1o2 41744	The vector to functional map provides a bijection from nonzero vectors 𝑉 to nonzero functionals with closed kernels 𝐶. (Contributed by NM, 27-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑂 = (0g‘𝐶)    &   ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑀:(𝑉 ∖ { 0 })–1-1-onto→(𝐹 ∖ {𝑂}))
Theorem	hvmapcl2 41745	Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑂 = (0g‘𝐶)    &   ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ (𝐹 ∖ {𝑂}))
Theorem	hvmaplfl 41746	The vector to functional map value is a functional. (Contributed by NM, 28-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ 𝐹)
Theorem	hvmaplkr 41747	Kernel of the vector to functional map. TODO: make this become lcfrlem11 41532. (Contributed by NM, 29-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐿‘(𝑀‘𝑋)) = (𝑂‘{𝑋}))
Theorem	mapdhvmap 41748	Relationship between mapd and HVMap, which can be used to satisfy the last hypothesis of mapdpg 41685. Equation 10 of [Baer] p. 48. (Contributed by NM, 29-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑃 = ((HVMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{(𝑃‘𝑋)}))
Theorem	lspindp5 41749	Obtain an independent vector set 𝑈, 𝑋, 𝑌 from a vector 𝑈 dependent on 𝑋 and 𝑍 and another independent set 𝑍, 𝑋, 𝑌. (Here we don't show the (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) part of the independence, which passes straight through. We also don't show nonzero vector requirements that are redundant for this theorem. Different orderings can be obtained using lspexch 21054 and prcom 4686.) (Contributed by NM, 4-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑁‘{𝑋, 𝑈}))    &   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑈 ∈ (𝑁‘{𝑋, 𝑌}))
Theorem	hdmaplem1 41750	Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑍 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑋}))
Theorem	hdmaplem2N 41751	Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑍 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑌}))
Theorem	hdmaplem3 41752	Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑍 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))
Theorem	hdmaplem4 41753	Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑋}))    &   ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑍 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑌})))
Theorem	mapdh8a 41754*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 5-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	mapdh8aa 41755*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 12-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	mapdh8ab 41756*	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	mapdh8ac 41757*	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 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑇}))    &   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑤⟩) = 𝐵)    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑤}))    &   ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑤, 𝑍}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑇⟩) = (𝐼‘⟨𝑍, 𝐸, 𝑇⟩))
Theorem	mapdh8ad 41758*	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	mapdh8b 41759*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-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	mapdh8c 41760*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-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	mapdh8d0N 41761*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 10-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 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇}))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑇}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑤}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑇}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑇⟩) = (𝐼‘⟨𝑋, 𝐹, 𝑇⟩))
Theorem	mapdh8d 41762*	Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-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	mapdh8e 41763*	Part of Part (8) in [Baer] p. 48. Eliminate 𝑤. (Contributed by NM, 10-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	mapdh8g 41764*	Part of Part (8) in [Baer] p. 48. Eliminate 𝑋 ∈ (𝑁‘{𝑌, 𝑇}). TODO: break out 𝑇 ≠ 0 in mapdh8e 41763 so we can share hypotheses. Also, look at hypothesis sharing for earlier mapdh8* and mapdh75* stuff. (Contributed by NM, 10-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	mapdh8i 41765*	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 41766*	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 41767*	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 41768*	Lemma for part (9) in [Baer] p. 48. TODO: why is this 50% larger than mapdh9aOLDN 41769? (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 41769*	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 41770	Extend class notation with preliminary map from vectors to functionals in the closed kernel dual space.
class HDMap1
Syntax	chdma 41771	Extend class notation with map from vectors to functionals in the closed kernel dual space.
class HDMap
Definition	df-hdmap1 41772*	Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 41775 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 41773*	Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 41806 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 41774*	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 41775*	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 41776*	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 41777*	Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval 41703.) TODO: change 𝐼 = (𝑥 ∈ V ↦... to (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌 > ) =... in e.g. mapdh8 41767 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 41778	Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 41704.) (Contributed by NM, 17-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 0 ⟩) = 𝑄)
Theorem	hdmap1val2 41779*	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 41780	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 41781*	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 41782*	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 41781 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 41783	Convert closure theorem mapdhcl 41706 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 41784	Convert mapdheq2 41708 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 41785	Convert mapdheq4 41711 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 41786	Lemma for hdmap1l6 41800. 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 41787	Lemma for hdmap1l6 41800. 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 41788	Lemma for hdmap1l6 41800. 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 41789	Lemmma for hdmap1l6 41800. (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 41790	Lemmma for hdmap1l6 41800. (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 41791	Lemmma for hdmap1l6 41800. (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 41792	Lemmma for hdmap1l6 41800. (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 41793	Lemmma for hdmap1l6 41800. 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 41794	Lemmma for hdmap1l6 41800. 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 41795	Lemmma for hdmap1l6 41800. 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 41796	Lemmma for hdmap1l6 41800. 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 41797	Lemmma for hdmap1l6 41800. 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 41798	Lemmma for hdmap1l6 41800. 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 41799	Lemmma for hdmap1l6 41800. 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 41800	Part (6) of [Baer] p. 47 line 6. Note that we use ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) which is equivalent to Baer's "Fx ∩ (Fy + Fz)" by lspdisjb 21051. (Convert mapdh6N 41726 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 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))