Home | Metamath
Proof Explorer Theorem List (p. 389 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mapdcnvatN 38801 | Atoms are preserved by the map defined by df-mapd 38760. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐵 = (LSAtoms‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) ⇒ ⊢ (𝜑 → (◡𝑀‘𝑄) ∈ 𝐴) | ||
Theorem | mapdat 38802 | Atoms are preserved by the map defined by df-mapd 38760. Property (g) in [Baer] p. 41. (Contributed by NM, 14-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐵 = (LSAtoms‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑀‘𝑄) ∈ 𝐵) | ||
Theorem | mapdspex 38803* | 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 38804 | 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 38805 | 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 38806 | 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 38807 | Lemma for mapdpg 38841. 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 38808* | Lemma for mapdpg 38841. 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 38809* | Lemma for mapdpg 38841. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) ⇒ ⊢ (𝜑 → 𝑡 ∈ 𝐹) | ||
Theorem | mapdpglem3 38810* | Lemma for mapdpg 38841. 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 38811* | Lemma for mapdpg 38841. (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 38812* | Lemma for mapdpg 38841. (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 38813* | Lemma for mapdpg 38841. 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 38814* | Lemma for mapdpg 38841. 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 38815* | Lemma for mapdpg 38841. 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 38816* | Lemma for mapdpg 38841. 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 38817* | Lemma for mapdpg 38841. (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 38818* | Lemma for mapdpg 38841. TODO: Can some commonality with mapdpglem6 38813 through mapdpglem11 38817 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 38819* | Lemma for mapdpg 38841. (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 38820* | Lemma for mapdpg 38841. (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 38821* | Lemma for mapdpg 38841. (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 38822* | Lemma for mapdpg 38841. 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 38823* | Lemma for mapdpg 38841. 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 38824* | Lemma for mapdpg 38841. 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 38825* | Lemma for mapdpg 38841. 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 38826* | Lemma for mapdpg 38841. 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 38827* | Lemma for mapdpg 38841. (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 38828* | Lemma for mapdpg 38841. 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 38829* | Lemma for mapdpg 38841. 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 38830 | Lemma for mapdpg 38841. (Contributed by NM, 22-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) ⇒ ⊢ (𝜑 → 𝐺 ≠ (0g‘𝐶)) | ||
Theorem | mapdpglem30b 38831 | Lemma for mapdpg 38841. (Contributed by NM, 22-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ (𝜑 → (ℎ ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)})))) & ⊢ (𝜑 → (𝑖 ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)})))) ⇒ ⊢ (𝜑 → 𝑖 ≠ (0g‘𝐶)) | ||
Theorem | mapdpglem25 38832 | Lemma for mapdpg 38841. 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 38833* | Lemma for mapdpg 38841. 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 38834* | Lemma for mapdpg 38841. 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 38835* | Lemma for mapdpg 38841. 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 38836* | Lemma for mapdpg 38841. 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 38837* | Lemma for mapdpg 38841. Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 38836, using lvecindp2 19910) that v = 1 and v = u...". TODO: would it be shorter to have only the 𝑣 = (1r‘𝐴) part and use mapdpglem28.u2 in mapdpglem31 38838? (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 38838* | Lemma for mapdpg 38841. 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 38839* | Lemma for mapdpg 38841. Existence part - consolidate hypotheses in mapdpglem23 38829. (Contributed by NM, 21-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) ⇒ ⊢ (𝜑 → ∃ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))) | ||
Theorem | mapdpglem32 38840* | Lemma for mapdpg 38841. Uniqueness part - consolidate hypotheses in mapdpglem31 38838. (Contributed by NM, 23-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) ⇒ ⊢ ((𝜑 ∧ (ℎ ∈ 𝐹 ∧ 𝑖 ∈ 𝐹) ∧ (((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)})) ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)})))) → ℎ = 𝑖) | ||
Theorem | mapdpg 38841* | 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 38859. (Contributed by NM, 22-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) ⇒ ⊢ (𝜑 → ∃!ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))) | ||
Theorem | baerlem3lem1 38842 | Lemma for baerlem3 38848. (Contributed by NM, 9-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ (𝜑 → 𝑎 ∈ 𝐵) & ⊢ (𝜑 → 𝑏 ∈ 𝐵) & ⊢ (𝜑 → 𝑑 ∈ 𝐵) & ⊢ (𝜑 → 𝑒 ∈ 𝐵) & ⊢ (𝜑 → 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) & ⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) ⇒ ⊢ (𝜑 → 𝑗 = (𝑎 · (𝑌 − 𝑍))) | ||
Theorem | baerlem5alem1 38843 | Lemma for baerlem5a 38849. (Contributed by NM, 13-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ (𝜑 → 𝑎 ∈ 𝐵) & ⊢ (𝜑 → 𝑏 ∈ 𝐵) & ⊢ (𝜑 → 𝑑 ∈ 𝐵) & ⊢ (𝜑 → 𝑒 ∈ 𝐵) & ⊢ (𝜑 → 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) & ⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) ⇒ ⊢ (𝜑 → 𝑗 = (𝑎 · (𝑋 − (𝑌 + 𝑍)))) | ||
Theorem | baerlem5blem1 38844 | Lemma for baerlem5b 38850. (Contributed by NM, 9-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ (𝜑 → 𝑎 ∈ 𝐵) & ⊢ (𝜑 → 𝑏 ∈ 𝐵) & ⊢ (𝜑 → 𝑑 ∈ 𝐵) & ⊢ (𝜑 → 𝑒 ∈ 𝐵) & ⊢ (𝜑 → 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) & ⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − (𝑌 + 𝑍))) + (𝑒 · 𝑋))) ⇒ ⊢ (𝜑 → 𝑗 = ((𝐼‘𝑑) · (𝑌 + 𝑍))) | ||
Theorem | baerlem3lem2 38845 | Lemma for baerlem3 38848. (Contributed by NM, 9-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)})))) | ||
Theorem | baerlem5alem2 38846 | Lemma for baerlem5a 38849. (Contributed by NM, 9-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) = (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌})))) | ||
Theorem | baerlem5blem2 38847 | Lemma for baerlem5b 38850. (Contributed by NM, 13-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 + 𝑍))}) ⊕ (𝑁‘{𝑋})))) | ||
Theorem | baerlem3 38848 | 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 38849 | 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 38850 | 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 38851 | 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 38853 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 − 𝑍))}) = (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 + 𝑍)}) ⊕ (𝑁‘{𝑌})))) | ||
Theorem | baerlem5bmN 38852 | 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 38853 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 − 𝑍))}) ⊕ (𝑁‘{𝑋})))) | ||
Theorem | baerlem5abmN 38853 | 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 38854 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) & ⊢ (𝜑 → (𝑌 + 𝑍) ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) = (𝑁‘{𝑌})) | ||
Theorem | mapdindp1 38855 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑌 + 𝑍)})) | ||
Theorem | mapdindp2 38856 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)})) | ||
Theorem | mapdindp3 38857 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑤 + 𝑌)})) | ||
Theorem | mapdindp4 38858 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, (𝑤 + 𝑌)})) | ||
Theorem | mapdhval 38859* | 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 38860* | 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 38861* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)})))) | ||
Theorem | mapdhcl 38862* | 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 38863* | 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 38864* | 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 38865* | Lemmma for ~? mapdh . Part (2) in [Baer] p. 45. The bidirectional version of mapdheq2 38864 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 38866* | Lemma for mapdheq4 38867. 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 38867* | 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 38868* | Lemma for mapdh6N 38882. 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 38869* | Lemma for mapdh6N 38882. 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 38870* | Lemma for mapdh6N 38882. 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 38871* | Lemmma for mapdh6N 38882. (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 38872* | Lemmma for mapdh6N 38882. (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 38873* | Lemmma for mapdh6N 38882. (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 38874* | Lemmma for mapdh6N 38882. (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 38875* | Lemmma for mapdh6N 38882. 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 38876* | Lemmma for mapdh6N 38882. 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 38877* | Lemmma for mapdh6N 38882. 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 38878* | Lemmma for mapdh6N 38882. 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 38879* | Lemmma for mapdh6N 38882. 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 38880* | Lemmma for mapdh6N 38882. 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 38881* | Lemmma for mapdh6N 38882. 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 38882* | Part (6) of [Baer] p. 47 line 6. Note that we use ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) which is equivalent to Baer's "Fx ∩ (Fy + Fz)" by lspdisjb 19897. 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 38956. (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 38883* | 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 38884* | 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 38885* | 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 38886* | 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 38887* | 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 38888.) (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 38888* | 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 38889* | 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 38890* | 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 38891 | Extend class notation with vector to dual map. |
class HVMap | ||
Definition | df-hvmap 38892* | 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 38686, dochfl1 38611- 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 38893* | 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 38894* | 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 38895* | 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 38896* | 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 38897 | 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 38898* | 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 38899* | 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 38900 | 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→(𝐹 ∖ {𝑂})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |