HomeTheorem List (p. 419 of 500)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 419 of 500) | < 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-30898) |
Hilbert Space Explorer
(30899-32421) |
Users' Mathboxes
(32422-49905) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mapdpglem31 41801* | Lemma for mapdpg 41804. 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 41802* | Lemma for mapdpg 41804. Existence part - consolidate hypotheses in mapdpglem23 41792. (Contributed by NM, 21-Mar-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) ⇒ ⊢ (𝜑 → ∃ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))) | ||
| Theorem | mapdpglem32 41803* | Lemma for mapdpg 41804. Uniqueness part - consolidate hypotheses in mapdpglem31 41801. (Contributed by NM, 23-Mar-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) ⇒ ⊢ ((𝜑 ∧ (ℎ ∈ 𝐹 ∧ 𝑖 ∈ 𝐹) ∧ (((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)})) ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)})))) → ℎ = 𝑖) | ||
| Theorem | mapdpg 41804* | 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 41822. (Contributed by NM, 22-Mar-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) ⇒ ⊢ (𝜑 → ∃!ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))) | ||
| Theorem | baerlem3lem1 41805 | Lemma for baerlem3 41811. (Contributed by NM, 9-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ (𝜑 → 𝑎 ∈ 𝐵) & ⊢ (𝜑 → 𝑏 ∈ 𝐵) & ⊢ (𝜑 → 𝑑 ∈ 𝐵) & ⊢ (𝜑 → 𝑒 ∈ 𝐵) & ⊢ (𝜑 → 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) & ⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) ⇒ ⊢ (𝜑 → 𝑗 = (𝑎 · (𝑌 − 𝑍))) | ||
| Theorem | baerlem5alem1 41806 | Lemma for baerlem5a 41812. (Contributed by NM, 13-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ (𝜑 → 𝑎 ∈ 𝐵) & ⊢ (𝜑 → 𝑏 ∈ 𝐵) & ⊢ (𝜑 → 𝑑 ∈ 𝐵) & ⊢ (𝜑 → 𝑒 ∈ 𝐵) & ⊢ (𝜑 → 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) & ⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) ⇒ ⊢ (𝜑 → 𝑗 = (𝑎 · (𝑋 − (𝑌 + 𝑍)))) | ||
| Theorem | baerlem5blem1 41807 | Lemma for baerlem5b 41813. (Contributed by NM, 9-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ (𝜑 → 𝑎 ∈ 𝐵) & ⊢ (𝜑 → 𝑏 ∈ 𝐵) & ⊢ (𝜑 → 𝑑 ∈ 𝐵) & ⊢ (𝜑 → 𝑒 ∈ 𝐵) & ⊢ (𝜑 → 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) & ⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − (𝑌 + 𝑍))) + (𝑒 · 𝑋))) ⇒ ⊢ (𝜑 → 𝑗 = ((𝐼‘𝑑) · (𝑌 + 𝑍))) | ||
| Theorem | baerlem3lem2 41808 | Lemma for baerlem3 41811. (Contributed by NM, 9-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)})))) | ||
| Theorem | baerlem5alem2 41809 | Lemma for baerlem5a 41812. (Contributed by NM, 9-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) = (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌})))) | ||
| Theorem | baerlem5blem2 41810 | Lemma for baerlem5b 41813. (Contributed by NM, 13-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 + 𝑍))}) ⊕ (𝑁‘{𝑋})))) | ||
| Theorem | baerlem3 41811 | 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 41812 | 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 41813 | 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 41814 | 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 41816 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 − 𝑍))}) = (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 + 𝑍)}) ⊕ (𝑁‘{𝑌})))) | ||
| Theorem | baerlem5bmN 41815 | 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 41816 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 − 𝑍))}) ⊕ (𝑁‘{𝑋})))) | ||
| Theorem | baerlem5abmN 41816 | 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 41817 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) & ⊢ (𝜑 → (𝑌 + 𝑍) ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) = (𝑁‘{𝑌})) | ||
| Theorem | mapdindp1 41818 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑌 + 𝑍)})) | ||
| Theorem | mapdindp2 41819 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)})) | ||
| Theorem | mapdindp3 41820 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑤 + 𝑌)})) | ||
| Theorem | mapdindp4 41821 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, (𝑤 + 𝑌)})) | ||
| Theorem | mapdhval 41822* | 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 41823* | 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 41824* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
| ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)})))) | ||
| Theorem | mapdhcl 41825* | 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 41826* | 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 41827* | 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 41828* | Lemmma for ~? mapdh . Part (2) in [Baer] p. 45. The bidirectional version of mapdheq2 41827 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 41829* | Lemma for mapdheq4 41830. 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 41830* | 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 41831* | Lemma for mapdh6N 41845. 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 41832* | Lemma for mapdh6N 41845. 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 41833* | Lemma for mapdh6N 41845. 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 41834* | Lemmma for mapdh6N 41845. (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 41835* | Lemmma for mapdh6N 41845. (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 41836* | Lemmma for mapdh6N 41845. (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 41837* | Lemmma for mapdh6N 41845. (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 41838* | Lemmma for mapdh6N 41845. 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 41839* | Lemmma for mapdh6N 41845. 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 41840* | Lemmma for mapdh6N 41845. 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 41841* | Lemmma for mapdh6N 41845. 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 41842* | Lemmma for mapdh6N 41845. 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 41843* | Lemmma for mapdh6N 41845. 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 41844* | Lemmma for mapdh6N 41845. 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 41845* | Part (6) of [Baer] p. 47 line 6. Note that we use ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) which is equivalent to Baer's "Fx ∩ (Fy + Fz)" by lspdisjb 21063. 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 41919. (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 41846* | 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 41847* | 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 41848* | 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 41849* | 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 41850* | 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 41851.) (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 41851* | 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 41852* | 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 41853* | 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 41854 | Extend class notation with vector to dual map. |
| class HVMap | ||
| Definition | df-hvmap 41855* | 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 41649, dochfl1 41574- 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 41856* | 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 41857* | 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 41858* | 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 41859* | 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 41860 | 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 41861* | 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 41862* | 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 41863 | The vector to functional map provides a bijection from nonzero vectors 𝑉 to nonzero functionals with closed kernels 𝐶. (Contributed by NM, 27-Mar-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑂 = (0g‘𝐶) & ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑀:(𝑉 ∖ { 0 })–1-1-onto→(𝐹 ∖ {𝑂})) | ||
| Theorem | hvmapcl2 41864 | Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑂 = (0g‘𝐶) & ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑀‘𝑋) ∈ (𝐹 ∖ {𝑂})) | ||
| Theorem | hvmaplfl 41865 | The vector to functional map value is a functional. (Contributed by NM, 28-Mar-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑀‘𝑋) ∈ 𝐹) | ||
| Theorem | hvmaplkr 41866 | Kernel of the vector to functional map. TODO: make this become lcfrlem11 41651. (Contributed by NM, 29-Mar-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐿‘(𝑀‘𝑋)) = (𝑂‘{𝑋})) | ||
| Theorem | mapdhvmap 41867 | Relationship between mapd and HVMap, which can be used to satisfy the last hypothesis of mapdpg 41804. Equation 10 of [Baer] p. 48. (Contributed by NM, 29-Mar-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑃 = ((HVMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{(𝑃‘𝑋)})) | ||
| Theorem | lspindp5 41868 | Obtain an independent vector set 𝑈, 𝑋, 𝑌 from a vector 𝑈 dependent on 𝑋 and 𝑍 and another independent set 𝑍, 𝑋, 𝑌. (Here we don't show the (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) part of the independence, which passes straight through. We also don't show nonzero vector requirements that are redundant for this theorem. Different orderings can be obtained using lspexch 21066 and prcom 4682.) (Contributed by NM, 4-May-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ (𝑁‘{𝑋, 𝑈})) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑈 ∈ (𝑁‘{𝑋, 𝑌})) | ||
| Theorem | hdmaplem1 41869 | Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑍 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑋})) | ||
| Theorem | hdmaplem2N 41870 | Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.) (New usage is discouraged.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑍 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑌})) | ||
| Theorem | hdmaplem3 41871 | Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑍 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) | ||
| Theorem | hdmaplem4 41872 | Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑋})) & ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑍 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑌}))) | ||
| Theorem | mapdh8a 41873* | Part of Part (8) in [Baer] p. 48. (Contributed by NM, 5-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑇})) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑇⟩) = (𝐼‘⟨𝑋, 𝐹, 𝑇⟩)) | ||
| Theorem | mapdh8aa 41874* | Part of Part (8) in [Baer] p. 48. (Contributed by NM, 12-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐸) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑇⟩) = (𝐼‘⟨𝑍, 𝐸, 𝑇⟩)) | ||
| Theorem | mapdh8ab 41875* | Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐸) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑇})) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑇⟩) = (𝐼‘⟨𝑍, 𝐸, 𝑇⟩)) | ||
| Theorem | mapdh8ac 41876* | Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐸) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑤⟩) = 𝐵) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑤})) & ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑤, 𝑍})) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑇⟩) = (𝐼‘⟨𝑍, 𝐸, 𝑇⟩)) | ||
| Theorem | mapdh8ad 41877* | Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = 𝐸) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑇⟩) = (𝐼‘⟨𝑍, 𝐸, 𝑇⟩)) | ||
| Theorem | mapdh8b 41878* | Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺})) & ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑤⟩) = 𝐸) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤})) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑇})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑤})) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑤, 𝐸, 𝑇⟩) = (𝐼‘⟨𝑌, 𝐺, 𝑇⟩)) | ||
| Theorem | mapdh8c 41879* | Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑤⟩) = 𝐸) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤})) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑇})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑤})) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑤, 𝐸, 𝑇⟩) = (𝐼‘⟨𝑋, 𝐹, 𝑇⟩)) | ||
| Theorem | mapdh8d0N 41880* | Part of Part (8) in [Baer] p. 48. (Contributed by NM, 10-May-2015.) (New usage is discouraged.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑤})) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑇})) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑇⟩) = (𝐼‘⟨𝑋, 𝐹, 𝑇⟩)) | ||
| Theorem | mapdh8d 41881* | Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑤})) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑇⟩) = (𝐼‘⟨𝑋, 𝐹, 𝑇⟩)) | ||
| Theorem | mapdh8e 41882* | Part of Part (8) in [Baer] p. 48. Eliminate 𝑤. (Contributed by NM, 10-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑇})) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑇⟩) = (𝐼‘⟨𝑋, 𝐹, 𝑇⟩)) | ||
| Theorem | mapdh8g 41883* | Part of Part (8) in [Baer] p. 48. Eliminate 𝑋 ∈ (𝑁‘{𝑌, 𝑇}). TODO: break out 𝑇 ≠ 0 in mapdh8e 41882 so we can share hypotheses. Also, look at hypothesis sharing for earlier mapdh8* and mapdh75* stuff. (Contributed by NM, 10-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇})) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑇⟩) = (𝐼‘⟨𝑋, 𝐹, 𝑇⟩)) | ||
| Theorem | mapdh8i 41884* | Part of Part (8) in [Baer] p. 48. (Contributed by NM, 11-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑇})) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑌, (𝐼‘⟨𝑋, 𝐹, 𝑌⟩), 𝑇⟩) = (𝐼‘⟨𝑍, (𝐼‘⟨𝑋, 𝐹, 𝑍⟩), 𝑇⟩)) | ||
| Theorem | mapdh8j 41885* | Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑌, (𝐼‘⟨𝑋, 𝐹, 𝑌⟩), 𝑇⟩) = (𝐼‘⟨𝑍, (𝐼‘⟨𝑋, 𝐹, 𝑍⟩), 𝑇⟩)) | ||
| Theorem | mapdh8 41886* | Part (8) in [Baer] p. 48. Given a reference vector 𝑋, the value of function 𝐼 at a vector 𝑇 is independent of the choice of auxiliary vectors 𝑌 and 𝑍. Unlike Baer's, our version does not require 𝑋, 𝑌, and 𝑍 to be independent, and also is defined for all 𝑌 and 𝑍 that are not colinear with 𝑋 or 𝑇. We do this to make the definition of Baer's sigma function more straightforward. (This part eliminates 𝑇 ≠ 0.) (Contributed by NM, 13-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑇})) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑌, (𝐼‘⟨𝑋, 𝐹, 𝑌⟩), 𝑇⟩) = (𝐼‘⟨𝑍, (𝐼‘⟨𝑋, 𝐹, 𝑍⟩), 𝑇⟩)) | ||
| Theorem | mapdh9a 41887* | Lemma for part (9) in [Baer] p. 48. TODO: why is this 50% larger than mapdh9aOLDN 41888? (Contributed by NM, 14-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑋, 𝐹, 𝑧⟩), 𝑇⟩))) | ||
| Theorem | mapdh9aOLDN 41888* | Lemma for part (9) in [Baer] p. 48. (Contributed by NM, 14-May-2015.) (New usage is discouraged.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇}) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑋, 𝐹, 𝑧⟩), 𝑇⟩))) | ||
| Syntax | chdma1 41889 | Extend class notation with preliminary map from vectors to functionals in the closed kernel dual space. |
| class HDMap1 | ||
| Syntax | chdma 41890 | Extend class notation with map from vectors to functionals in the closed kernel dual space. |
| class HDMap | ||
| Definition | df-hdmap1 41891* | Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 41894 description for more details. (Contributed by NM, 14-May-2015.) |
| ⊢ HDMap1 = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))})) | ||
| Definition | df-hdmap 41892* | Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 41925 description for more details. (Contributed by NM, 15-May-2015.) |
| ⊢ HDMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})) | ||
| Theorem | hdmap1ffval 41893* | Preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 14-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑋 → (HDMap1‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝐾)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))})) | ||
| Theorem | hdmap1fval 41894* | Preliminary map from vectors to functionals in the closed kernel dual space. TODO: change span 𝐽 to the convention 𝐿 for this section. (Contributed by NM, 15-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))) | ||
| Theorem | hdmap1vallem 41895* | Value of preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ ((𝑉 × 𝐷) × 𝑉)) ⇒ ⊢ (𝜑 → (𝐼‘𝑇) = if((2nd ‘𝑇) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑇)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑇)) − (2nd ‘𝑇))})) = (𝐽‘{((2nd ‘(1st ‘𝑇))𝑅ℎ)}))))) | ||
| Theorem | hdmap1val 41896* | Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval 41822.) TODO: change 𝐼 = (𝑥 ∈ V ↦... to (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌 > ) =... in e.g. mapdh8 41886 to shorten proofs with no $d on 𝑥. (Contributed by NM, 15-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = if(𝑌 = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)}))))) | ||
| Theorem | hdmap1val0 41897 | Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 41823.) (Contributed by NM, 17-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 0 ⟩) = 𝑄) | ||
| Theorem | hdmap1val2 41898* | Value of preliminary map from vectors to functionals in the closed kernel dual space, for nonzero 𝑌. (Contributed by NM, 16-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐿‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐿‘{(𝐹𝑅ℎ)})))) | ||
| Theorem | hdmap1eq 41899 | The defining equation for h(x,x',y)=y' in part (2) in [Baer] p. 45 line 24. (Contributed by NM, 16-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 ∈ 𝐷) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) ⇒ ⊢ (𝜑 → ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = 𝐺 ↔ ((𝑀‘(𝑁‘{𝑌})) = (𝐿‘{𝐺}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐿‘{(𝐹𝑅𝐺)})))) | ||
| Theorem | hdmap1cbv 41900* | Frequently used lemma to change bound variables in 𝐿 hypothesis. (Contributed by NM, 15-May-2015.) |
| ⊢ 𝐿 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) ⇒ ⊢ 𝐿 = (𝑦 ∈ V ↦ if((2nd ‘𝑦) = 0 , 𝑄, (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑦)) − (2nd ‘𝑦))})) = (𝐽‘{((2nd ‘(1st ‘𝑦))𝑅𝑖)}))))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |