P. 406 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40501-40600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mapdsn2 40501*	Value of the map defined by df-mapd 40484 at the span of a singleton. (Contributed by NM, 16-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐿‘𝐺) = (𝑂‘{𝑋}))    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = {𝑓 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑓)})
Theorem	mapdsn3 40502	Value of the map defined by df-mapd 40484 at the span of a singleton. (Contributed by NM, 17-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑃 = (LSpan‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐿‘𝐺) = (𝑂‘{𝑋}))    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝑃‘{𝐺}))
Theorem	mapd1dim2lem1N 40503*	Value of the map defined by df-mapd 40484 at an atom. (Contributed by NM, 10-Feb-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑀‘𝑄) = {𝑓 ∈ 𝐹 ∣ ∃𝑣 ∈ 𝑄 (𝑂‘{𝑣}) = (𝐿‘𝑓)})
Theorem	mapdrvallem2 40504*	Lemma for mapdrval 40506. TODO: very long antecedents are dragged through proof in some places - see if it shortens proof to remove unused conjuncts. (Contributed by NM, 2-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝐶)    &   ⊢ 𝑄 = ∪ ℎ ∈ 𝑅 (𝑂‘(𝐿‘ℎ))    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑌 = (0g‘𝐷)    ⇒   ⊢ (𝜑 → {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑄} ⊆ 𝑅)
Theorem	mapdrvallem3 40505*	Lemma for mapdrval 40506. (Contributed by NM, 2-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝐶)    &   ⊢ 𝑄 = ∪ ℎ ∈ 𝑅 (𝑂‘(𝐿‘ℎ))    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑌 = (0g‘𝐷)    ⇒   ⊢ (𝜑 → {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑄} = 𝑅)
Theorem	mapdrval 40506*	Given a dual subspace 𝑅 (of functionals with closed kernels), reconstruct the subspace 𝑄 that maps to it. (Contributed by NM, 12-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝐶)    &   ⊢ 𝑄 = ∪ ℎ ∈ 𝑅 (𝑂‘(𝐿‘ℎ))    ⇒   ⊢ (𝜑 → (𝑀‘𝑄) = 𝑅)
Theorem	mapd1o 40507*	The map defined by df-mapd 40484 is one-to-one and onto the set of dual subspaces of functionals with closed kernels. This shows 𝑀 satisfies part of the definition of projectivity of [Baer] p. 40. TODO: change theorems leading to this (lcfr 40444, mapdrval 40506, lclkrs 40398, lclkr 40392,...) to use 𝑇 ∩ 𝒫 𝐶? TODO: maybe get rid of $d's for 𝑔 versus 𝐾𝑈𝑊; propagate to mapdrn 40508 and any others. (Contributed by NM, 12-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑀:𝑆–1-1-onto→(𝑇 ∩ 𝒫 𝐶))
Theorem	mapdrn 40508*	Range of the map defined by df-mapd 40484. (Contributed by NM, 12-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ran 𝑀 = (𝑇 ∩ 𝒫 𝐶))
Theorem	mapdunirnN 40509*	Union of the range of the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ∪ ran 𝑀 = 𝐶)
Theorem	mapdrn2 40510	Range of the map defined by df-mapd 40484. TODO: this seems to be needed a lot in hdmaprnlem3eN 40717 etc. Would it be better to change df-mapd 40484 theorems to use LSubSp‘𝐶 instead of ran 𝑀? (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑇 = (LSubSp‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ran 𝑀 = 𝑇)
Theorem	mapdcnvcl 40511	Closure of the converse of the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑀)    ⇒   ⊢ (𝜑 → (◡𝑀‘𝑋) ∈ 𝑆)
Theorem	mapdcl 40512	Closure the value of the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ ran 𝑀)
Theorem	mapdcnvid1N 40513	Converse of the value of the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (◡𝑀‘(𝑀‘𝑋)) = 𝑋)
Theorem	mapdsord 40514	Strong ordering property of themap defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝑀‘𝑋) ⊊ (𝑀‘𝑌) ↔ 𝑋 ⊊ 𝑌))
Theorem	mapdcl2 40515	The mapping of a subspace of vector space H is a subspace in the dual space of functionals with closed kernels. (Contributed by NM, 31-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑇 = (LSubSp‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝑅) ∈ 𝑇)
Theorem	mapdcnvid2 40516	Value of the converse of the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑀)    ⇒   ⊢ (𝜑 → (𝑀‘(◡𝑀‘𝑋)) = 𝑋)
Theorem	mapdcnvordN 40517	Ordering property of the converse of the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑀)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝑀)    ⇒   ⊢ (𝜑 → ((◡𝑀‘𝑋) ⊆ (◡𝑀‘𝑌) ↔ 𝑋 ⊆ 𝑌))
Theorem	mapdcnv11N 40518	The converse of the map defined by df-mapd 40484 is one-to-one. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑀)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝑀)    ⇒   ⊢ (𝜑 → ((◡𝑀‘𝑋) = (◡𝑀‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	mapdcv 40519	Covering property of the converse of the map defined by df-mapd 40484. (Contributed by NM, 14-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐶 = ( ⋖L ‘𝑈)    &   ⊢ 𝐷 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ( ⋖L ‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋𝐶𝑌 ↔ (𝑀‘𝑋)𝐸(𝑀‘𝑌)))
Theorem	mapdincl 40520	Closure of dual subspace intersection for the map defined by df-mapd 40484. (Contributed by NM, 12-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑀)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝑀)    ⇒   ⊢ (𝜑 → (𝑋 ∩ 𝑌) ∈ ran 𝑀)
Theorem	mapdin 40521	Subspace intersection is preserved by the map defined by df-mapd 40484. Part of property (e) in [Baer] p. 40. (Contributed by NM, 12-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑋 ∩ 𝑌)) = ((𝑀‘𝑋) ∩ (𝑀‘𝑌)))
Theorem	mapdlsmcl 40522	Closure of dual subspace sum for the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑀)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝑀)    ⇒   ⊢ (𝜑 → (𝑋 ⊕ 𝑌) ∈ ran 𝑀)
Theorem	mapdlsm 40523	Subspace sum is preserved by the map defined by df-mapd 40484. Part of property (e) in [Baer] p. 40. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (LSSum‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑋 ⊕ 𝑌)) = ((𝑀‘𝑋) ✚ (𝑀‘𝑌)))
Theorem	mapd0 40524	Projectivity map of the zero subspace. Part of property (f) in [Baer] p. 40. TODO: does proof need to be this long for this simple fact? (Contributed by NM, 15-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 0 = (0g‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → (𝑀‘{𝑂}) = { 0 })
Theorem	mapdcnvatN 40525	Atoms are preserved by the map defined by df-mapd 40484. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐵 = (LSAtoms‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (◡𝑀‘𝑄) ∈ 𝐴)
Theorem	mapdat 40526	Atoms are preserved by the map defined by df-mapd 40484. Property (g) in [Baer] p. 41. (Contributed by NM, 14-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐵 = (LSAtoms‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑀‘𝑄) ∈ 𝐵)
Theorem	mapdspex 40527*	The map of a span equals the dual span of some vector (functional). (Contributed by NM, 15-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝐵 (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝑔}))
Theorem	mapdn0 40528	Transfer nonzero property from domain to range of projectivity mapd. (Contributed by NM, 12-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑍 = (0g‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐷 ∖ {𝑍}))
Theorem	mapdncol 40529	Transfer non-colinearity from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝐽‘{𝐹}) ≠ (𝐽‘{𝐺}))
Theorem	mapdindp 40530	Transfer (part of) vector independence condition from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐷)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸}))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    ⇒   ⊢ (𝜑 → ¬ 𝐹 ∈ (𝐽‘{𝐺, 𝐸}))
Theorem	mapdpglem1 40531	Lemma for mapdpg 40565. Baer p. 44, last line: "(F(x-y))* <= (Fx)*+(Fy)*." (Contributed by NM, 15-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) ⊆ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))
Theorem	mapdpglem2 40532*	Lemma for mapdpg 40565. Baer p. 45, lines 1 and 2: "we have (F(x-y))* = Gt where t necessarily belongs to (Fx)*+(Fy)*." (We scope $d 𝑡𝜑 locally to avoid clashes with later substitutions into 𝜑.) (Contributed by NM, 15-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    ⇒   ⊢ (𝜑 → ∃𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))(𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))
Theorem	mapdpglem2a 40533*	Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    ⇒   ⊢ (𝜑 → 𝑡 ∈ 𝐹)
Theorem	mapdpglem3 40534*	Lemma for mapdpg 40565. Baer p. 45, line 3: "infer ... the existence of a number g in G and of an element z in (Fy)* such that t = gx'-z." (We scope $d 𝑔𝑤𝑧𝜑 locally to avoid clashes with later substitutions into 𝜑.) (Contributed by NM, 18-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝐵 ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = ((𝑔 · 𝐺)𝑅𝑧))
Theorem	mapdpglem4N 40535*	Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ≠ 𝑄)
Theorem	mapdpglem5N 40536*	Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    ⇒   ⊢ (𝜑 → 𝑡 ≠ (0g‘𝐶))
Theorem	mapdpglem6 40537*	Lemma for mapdpg 40565. Baer p. 45, line 4: "If g were 0, then t would be in (Fy)*..." (Contributed by NM, 18-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑔 = 0 )    ⇒   ⊢ (𝜑 → 𝑡 ∈ (𝑀‘(𝑁‘{𝑌})))
Theorem	mapdpglem8 40538*	Lemma for mapdpg 40565. Baer p. 45, line 4: "...so that (F(x-y))* <= (Fy)*. This would imply that F(x-y) <= F(y)..." (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑔 = 0 )    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑌)}) ⊆ (𝑁‘{𝑌}))
Theorem	mapdpglem9 40539*	Lemma for mapdpg 40565. Baer p. 45, line 4: "...so that x would consequently belong to Fy." (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑔 = 0 )    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌}))
Theorem	mapdpglem10 40540*	Lemma for mapdpg 40565. Baer p. 45, line 6: "Hence Fx=Fy, an impossibility." (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑔 = 0 )    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))
Theorem	mapdpglem11 40541*	Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    ⇒   ⊢ (𝜑 → 𝑔 ≠ 0 )
Theorem	mapdpglem12 40542*	Lemma for mapdpg 40565. TODO: Can some commonality with mapdpglem6 40537 through mapdpglem11 40541 be exploited? Also, some consolidation of small lemmas here could be done. (Contributed by NM, 18-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑧 = (0g‘𝐶))    ⇒   ⊢ (𝜑 → 𝑡 ∈ (𝑀‘(𝑁‘{𝑋})))
Theorem	mapdpglem13 40543*	Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑧 = (0g‘𝐶))    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑌)}) ⊆ (𝑁‘{𝑋}))
Theorem	mapdpglem14 40544*	Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑧 = (0g‘𝐶))    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋}))
Theorem	mapdpglem15 40545*	Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑧 = (0g‘𝐶))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))
Theorem	mapdpglem16 40546*	Lemma for mapdpg 40565. Baer p. 45, line 7: "Likewise we see that z =/= 0." (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑄)    ⇒   ⊢ (𝜑 → 𝑧 ≠ (0g‘𝐶))
Theorem	mapdpglem17N 40547*	Lemma for mapdpg 40565. Baer p. 45, line 7: "Hence we may form y' = g^-1 z." (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑄)    &   ⊢ 𝐸 = (((invr‘𝐴)‘𝑔) · 𝑧)    ⇒   ⊢ (𝜑 → 𝐸 ∈ 𝐹)
Theorem	mapdpglem18 40548*	Lemma for mapdpg 40565. Baer p. 45, line 7: "Then y =/= 0..." (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑄)    &   ⊢ 𝐸 = (((invr‘𝐴)‘𝑔) · 𝑧)    ⇒   ⊢ (𝜑 → 𝐸 ≠ (0g‘𝐶))
Theorem	mapdpglem19 40549*	Lemma for mapdpg 40565. Baer p. 45, line 8: "...is in (Fy)*..." (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑄)    &   ⊢ 𝐸 = (((invr‘𝐴)‘𝑔) · 𝑧)    ⇒   ⊢ (𝜑 → 𝐸 ∈ (𝑀‘(𝑁‘{𝑌})))
Theorem	mapdpglem20 40550*	Lemma for mapdpg 40565. Baer p. 45, line 8: "...so that (Fy)*=Gy'." (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑄)    &   ⊢ 𝐸 = (((invr‘𝐴)‘𝑔) · 𝑧)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐸}))
Theorem	mapdpglem21 40551*	Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑄)    &   ⊢ 𝐸 = (((invr‘𝐴)‘𝑔) · 𝑧)    ⇒   ⊢ (𝜑 → (((invr‘𝐴)‘𝑔) · 𝑡) = (𝐺𝑅𝐸))
Theorem	mapdpglem22 40552*	Lemma for mapdpg 40565. Baer p. 45, line 9: "(F(x-y))* = ... = G(x'-y')." (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑄)    &   ⊢ 𝐸 = (((invr‘𝐴)‘𝑔) · 𝑧)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝐸)}))
Theorem	mapdpglem23 40553*	Lemma for mapdpg 40565. Baer p. 45, line 10: "and so y' meets all our requirements." Our ℎ is Baer's y'. (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ⊕ = (LSSum‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ 𝑄 = (0g‘𝑈)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}))    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌})))    &   ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑄)    &   ⊢ 𝐸 = (((invr‘𝐴)‘𝑔) · 𝑧)    ⇒   ⊢ (𝜑 → ∃ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)})))
Theorem	mapdpglem30a 40554	Lemma for mapdpg 40565. (Contributed by NM, 22-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    ⇒   ⊢ (𝜑 → 𝐺 ≠ (0g‘𝐶))
Theorem	mapdpglem30b 40555	Lemma for mapdpg 40565. (Contributed by NM, 22-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ (𝜑 → (ℎ ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))))    &   ⊢ (𝜑 → (𝑖 ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))    ⇒   ⊢ (𝜑 → 𝑖 ≠ (0g‘𝐶))
Theorem	mapdpglem25 40556	Lemma for mapdpg 40565. Baer p. 45 line 12: "Then we have Gy' = Gy'' and G(x'-y') = G(x'-y'')." (Contributed by NM, 21-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ (𝜑 → (ℎ ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))))    &   ⊢ (𝜑 → (𝑖 ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))    ⇒   ⊢ (𝜑 → ((𝐽‘{ℎ}) = (𝐽‘{𝑖}) ∧ (𝐽‘{(𝐺𝑅ℎ)}) = (𝐽‘{(𝐺𝑅𝑖)})))
Theorem	mapdpglem26 40557*	Lemma for mapdpg 40565. Baer p. 45 line 14: "Consequently there exist numbers u,v in G neither of which is 0 such that y = uy'' and..." (We scope $d 𝑢𝜑 locally to avoid clashes with later substitutions into 𝜑.) (Contributed by NM, 22-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ (𝜑 → (ℎ ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))))    &   ⊢ (𝜑 → (𝑖 ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑂 = (0g‘𝐴)    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ (𝐵 ∖ {𝑂})ℎ = (𝑢 · 𝑖))
Theorem	mapdpglem27 40558*	Lemma for mapdpg 40565. Baer p. 45 line 16: "v(x'-y'') = x'-y'" (with equality swapped). (Contributed by NM, 22-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ (𝜑 → (ℎ ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))))    &   ⊢ (𝜑 → (𝑖 ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑂 = (0g‘𝐴)    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ (𝐵 ∖ {𝑂})(𝐺𝑅ℎ) = (𝑣 · (𝐺𝑅𝑖)))
Theorem	mapdpglem29 40559*	Lemma for mapdpg 40565. Baer p. 45 line 16: "But Gx' and Gy'' are distinct points and so x' and y'' are independent elements in B. (Contributed by NM, 22-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ (𝜑 → (ℎ ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))))    &   ⊢ (𝜑 → (𝑖 ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑂 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑣 ∈ 𝐵)    &   ⊢ (𝜑 → ℎ = (𝑢 · 𝑖))    &   ⊢ (𝜑 → (𝐺𝑅ℎ) = (𝑣 · (𝐺𝑅𝑖)))    ⇒   ⊢ (𝜑 → (𝐽‘{𝐺}) ≠ (𝐽‘{𝑖}))
Theorem	mapdpglem28 40560*	Lemma for mapdpg 40565. Baer p. 45 line 18: "vx'-vy'' = x'-uy''". (Contributed by NM, 22-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ (𝜑 → (ℎ ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))))    &   ⊢ (𝜑 → (𝑖 ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑂 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑣 ∈ 𝐵)    &   ⊢ (𝜑 → ℎ = (𝑢 · 𝑖))    &   ⊢ (𝜑 → (𝐺𝑅ℎ) = (𝑣 · (𝐺𝑅𝑖)))    ⇒   ⊢ (𝜑 → ((𝑣 · 𝐺)𝑅(𝑣 · 𝑖)) = (𝐺𝑅(𝑢 · 𝑖)))
Theorem	mapdpglem30 40561*	Lemma for mapdpg 40565. Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 40560, using lvecindp2 20744) that v = 1 and v = u...". TODO: would it be shorter to have only the 𝑣 = (1r‘𝐴) part and use mapdpglem28.u2 in mapdpglem31 40562? (Contributed by NM, 22-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ (𝜑 → (ℎ ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))))    &   ⊢ (𝜑 → (𝑖 ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑂 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑣 ∈ 𝐵)    &   ⊢ (𝜑 → ℎ = (𝑢 · 𝑖))    &   ⊢ (𝜑 → (𝐺𝑅ℎ) = (𝑣 · (𝐺𝑅𝑖)))    &   ⊢ (𝜑 → 𝑢 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑣 = (1r‘𝐴) ∧ 𝑣 = 𝑢))
Theorem	mapdpglem31 40562*	Lemma for mapdpg 40565. Baer p. 45 line 19: "...and we have consequently that y' = y'', as we claimed." (Contributed by NM, 23-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    &   ⊢ (𝜑 → (ℎ ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))))    &   ⊢ (𝜑 → (𝑖 ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))    &   ⊢ 𝐴 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑂 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑣 ∈ 𝐵)    &   ⊢ (𝜑 → ℎ = (𝑢 · 𝑖))    &   ⊢ (𝜑 → (𝐺𝑅ℎ) = (𝑣 · (𝐺𝑅𝑖)))    &   ⊢ (𝜑 → 𝑢 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ℎ = 𝑖)
Theorem	mapdpglem24 40563*	Lemma for mapdpg 40565. Existence part - consolidate hypotheses in mapdpglem23 40553. (Contributed by NM, 21-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    ⇒   ⊢ (𝜑 → ∃ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)})))
Theorem	mapdpglem32 40564*	Lemma for mapdpg 40565. Uniqueness part - consolidate hypotheses in mapdpglem31 40562. (Contributed by NM, 23-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    ⇒   ⊢ ((𝜑 ∧ (ℎ ∈ 𝐹 ∧ 𝑖 ∈ 𝐹) ∧ (((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)})) ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)})))) → ℎ = 𝑖)
Theorem	mapdpg 40565*	Part 1 of proof of the first fundamental theorem of projective geometry. Part (1) in [Baer] p. 44. Our notation corresponds to Baer's as follows: 𝑀 for *, 𝑁‘{} for F(), 𝐽‘{} for G(), 𝑋 for x, 𝐺 for x', 𝑌 for y, ℎ for y'. TODO: Rename variables per mapdhval 40583. (Contributed by NM, 22-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑅 = (-g‘𝐶)    &   ⊢ 𝐽 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))    ⇒   ⊢ (𝜑 → ∃!ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)})))
Theorem	baerlem3lem1 40566	Lemma for baerlem3 40572. (Contributed by NM, 9-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝐿 = (-g‘𝑅)    &   ⊢ 𝑄 = (0g‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑎 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑏 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑑 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑒 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍)))    &   ⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍))))    ⇒   ⊢ (𝜑 → 𝑗 = (𝑎 · (𝑌 − 𝑍)))
Theorem	baerlem5alem1 40567	Lemma for baerlem5a 40573. (Contributed by NM, 13-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝐿 = (-g‘𝑅)    &   ⊢ 𝑄 = (0g‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑎 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑏 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑑 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑒 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍)))    &   ⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌)))    ⇒   ⊢ (𝜑 → 𝑗 = (𝑎 · (𝑋 − (𝑌 + 𝑍))))
Theorem	baerlem5blem1 40568	Lemma for baerlem5b 40574. (Contributed by NM, 9-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝐿 = (-g‘𝑅)    &   ⊢ 𝑄 = (0g‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑎 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑏 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑑 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑒 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍)))    &   ⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − (𝑌 + 𝑍))) + (𝑒 · 𝑋)))    ⇒   ⊢ (𝜑 → 𝑗 = ((𝐼‘𝑑) · (𝑌 + 𝑍)))
Theorem	baerlem3lem2 40569	Lemma for baerlem3 40572. (Contributed by NM, 9-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝐿 = (-g‘𝑅)    &   ⊢ 𝑄 = (0g‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)}))))
Theorem	baerlem5alem2 40570	Lemma for baerlem5a 40573. (Contributed by NM, 9-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝐿 = (-g‘𝑅)    &   ⊢ 𝑄 = (0g‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) = (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌}))))
Theorem	baerlem5blem2 40571	Lemma for baerlem5b 40574. (Contributed by NM, 13-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝐿 = (-g‘𝑅)    &   ⊢ 𝑄 = (0g‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 + 𝑍))}) ⊕ (𝑁‘{𝑋}))))
Theorem	baerlem3 40572	An equality that holds when 𝑋, 𝑌, 𝑍 are independent (non-colinear) vectors. Part (3) in [Baer] p. 45. TODO fix ref. (Contributed by NM, 9-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)}))))
Theorem	baerlem5a 40573	An equality that holds when 𝑋, 𝑌, 𝑍 are independent (non-colinear) vectors. First equation of part (5) in [Baer] p. 46. (Contributed by NM, 10-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) = (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌}))))
Theorem	baerlem5b 40574	An equality that holds when 𝑋, 𝑌, 𝑍 are independent (non-colinear) vectors. Second equation of part (5) in [Baer] p. 46. (Contributed by NM, 13-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 + 𝑍))}) ⊕ (𝑁‘{𝑋}))))
Theorem	baerlem5amN 40575	An equality that holds when 𝑋, 𝑌, 𝑍 are independent (non-colinear) vectors. Subtraction version of first equation of part (5) in [Baer] p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN 40577 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 − 𝑍))}) = (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 + 𝑍)}) ⊕ (𝑁‘{𝑌}))))
Theorem	baerlem5bmN 40576	An equality that holds when 𝑋, 𝑌, 𝑍 are independent (non-colinear) vectors. Subtraction version of second equation of part (5) in [Baer] p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN 40577 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 − 𝑍))}) ⊕ (𝑁‘{𝑋}))))
Theorem	baerlem5abmN 40577	An equality that holds when 𝑋, 𝑌, 𝑍 are independent (non-colinear) vectors. Subtraction versions of first and second equations of part (5) in [Baer] p. 46, conjoined to share commonality in their proofs. TODO: Delete if not needed. (Contributed by NM, 24-May-2015.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ (𝜑 → ((𝑁‘{(𝑋 − (𝑌 − 𝑍))}) = (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 + 𝑍)}) ⊕ (𝑁‘{𝑌}))) ∧ (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 − 𝑍))}) ⊕ (𝑁‘{𝑋})))))
Theorem	mapdindp0 40578	Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    &   ⊢ (𝜑 → (𝑌 + 𝑍) ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) = (𝑁‘{𝑌}))
Theorem	mapdindp1 40579	Vector independence lemma. (Contributed by NM, 1-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑌 + 𝑍)}))
Theorem	mapdindp2 40580	Vector independence lemma. (Contributed by NM, 1-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)}))
Theorem	mapdindp3 40581	Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑤 + 𝑌)}))
Theorem	mapdindp4 40582	Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, (𝑤 + 𝑌)}))
Theorem	mapdhval 40583*	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 40584*	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 40585*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)}))))
Theorem	mapdhcl 40586*	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 40587*	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 40588*	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 40589*	Lemmma for ~? mapdh . Part (2) in [Baer] p. 45. The bidirectional version of mapdheq2 40588 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 40590*	Lemma for mapdheq4 40591. 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 40591*	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 40592*	Lemma for mapdh6N 40606. 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 40593*	Lemma for mapdh6N 40606. 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 40594*	Lemma for mapdh6N 40606. 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 40595*	Lemmma for mapdh6N 40606. (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 40596*	Lemmma for mapdh6N 40606. (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 40597*	Lemmma for mapdh6N 40606. (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 40598*	Lemmma for mapdh6N 40606. (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 40599*	Lemmma for mapdh6N 40606. 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 40600*	Lemmma for mapdh6N 40606. 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 }))    &   ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑤 + 𝑌)⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑌⟩)))