HomeTheorem List (p. 418 of 498)
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. 418 of 498) | < 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-30854) |
Hilbert Space Explorer
(30855-32377) |
Users' Mathboxes
(32378-49798) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mapdpglem29 41701* | Lemma for mapdpg 41707. 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 41702* | Lemma for mapdpg 41707. 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 41703* | Lemma for mapdpg 41707. Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 41702, using lvecindp2 21056) that v = 1 and v = u...". TODO: would it be shorter to have only the 𝑣 = (1r‘𝐴) part and use mapdpglem28.u2 in mapdpglem31 41704? (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 41704* | Lemma for mapdpg 41707. 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 41705* | Lemma for mapdpg 41707. Existence part - consolidate hypotheses in mapdpglem23 41695. (Contributed by NM, 21-Mar-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) ⇒ ⊢ (𝜑 → ∃ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))) | ||
| Theorem | mapdpglem32 41706* | Lemma for mapdpg 41707. Uniqueness part - consolidate hypotheses in mapdpglem31 41704. (Contributed by NM, 23-Mar-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) ⇒ ⊢ ((𝜑 ∧ (ℎ ∈ 𝐹 ∧ 𝑖 ∈ 𝐹) ∧ (((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)})) ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)})))) → ℎ = 𝑖) | ||
| Theorem | mapdpg 41707* | 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 41725. (Contributed by NM, 22-Mar-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) ⇒ ⊢ (𝜑 → ∃!ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))) | ||
| Theorem | baerlem3lem1 41708 | Lemma for baerlem3 41714. (Contributed by NM, 9-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ (𝜑 → 𝑎 ∈ 𝐵) & ⊢ (𝜑 → 𝑏 ∈ 𝐵) & ⊢ (𝜑 → 𝑑 ∈ 𝐵) & ⊢ (𝜑 → 𝑒 ∈ 𝐵) & ⊢ (𝜑 → 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) & ⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) ⇒ ⊢ (𝜑 → 𝑗 = (𝑎 · (𝑌 − 𝑍))) | ||
| Theorem | baerlem5alem1 41709 | Lemma for baerlem5a 41715. (Contributed by NM, 13-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ (𝜑 → 𝑎 ∈ 𝐵) & ⊢ (𝜑 → 𝑏 ∈ 𝐵) & ⊢ (𝜑 → 𝑑 ∈ 𝐵) & ⊢ (𝜑 → 𝑒 ∈ 𝐵) & ⊢ (𝜑 → 𝑗 = ((𝑎 · (𝑋 − 𝑌)) + (𝑏 · 𝑍))) & ⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − 𝑍)) + (𝑒 · 𝑌))) ⇒ ⊢ (𝜑 → 𝑗 = (𝑎 · (𝑋 − (𝑌 + 𝑍)))) | ||
| Theorem | baerlem5blem1 41710 | Lemma for baerlem5b 41716. (Contributed by NM, 9-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ (𝜑 → 𝑎 ∈ 𝐵) & ⊢ (𝜑 → 𝑏 ∈ 𝐵) & ⊢ (𝜑 → 𝑑 ∈ 𝐵) & ⊢ (𝜑 → 𝑒 ∈ 𝐵) & ⊢ (𝜑 → 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) & ⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − (𝑌 + 𝑍))) + (𝑒 · 𝑋))) ⇒ ⊢ (𝜑 → 𝑗 = ((𝐼‘𝑑) · (𝑌 + 𝑍))) | ||
| Theorem | baerlem3lem2 41711 | Lemma for baerlem3 41714. (Contributed by NM, 9-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)})))) | ||
| Theorem | baerlem5alem2 41712 | Lemma for baerlem5a 41715. (Contributed by NM, 9-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) = (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)}) ⊕ (𝑁‘{𝑌})))) | ||
| Theorem | baerlem5blem2 41713 | Lemma for baerlem5b 41716. (Contributed by NM, 13-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝐿 = (-g‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 + 𝑍))}) ⊕ (𝑁‘{𝑋})))) | ||
| Theorem | baerlem3 41714 | 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 41715 | 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 41716 | 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 41717 | 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 41719 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 − 𝑍))}) = (((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 + 𝑍)}) ⊕ (𝑁‘{𝑌})))) | ||
| Theorem | baerlem5bmN 41718 | 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 41719 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ + = (+g‘𝑊) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 − 𝑍))}) ⊕ (𝑁‘{𝑋})))) | ||
| Theorem | baerlem5abmN 41719 | 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 41720 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) & ⊢ (𝜑 → (𝑌 + 𝑍) ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) = (𝑁‘{𝑌})) | ||
| Theorem | mapdindp1 41721 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑌 + 𝑍)})) | ||
| Theorem | mapdindp2 41722 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)})) | ||
| Theorem | mapdindp3 41723 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑤 + 𝑌)})) | ||
| Theorem | mapdindp4 41724 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, (𝑤 + 𝑌)})) | ||
| Theorem | mapdhval 41725* | 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 41726* | 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 41727* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
| ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)})))) | ||
| Theorem | mapdhcl 41728* | 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 41729* | 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 41730* | 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 41731* | Lemmma for ~? mapdh . Part (2) in [Baer] p. 45. The bidirectional version of mapdheq2 41730 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 41732* | Lemma for mapdheq4 41733. 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 41733* | 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 41734* | Lemma for mapdh6N 41748. 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 41735* | Lemma for mapdh6N 41748. 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 41736* | Lemma for mapdh6N 41748. 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 41737* | Lemmma for mapdh6N 41748. (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 41738* | Lemmma for mapdh6N 41748. (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 41739* | Lemmma for mapdh6N 41748. (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 41740* | Lemmma for mapdh6N 41748. (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 41741* | Lemmma for mapdh6N 41748. 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 41742* | Lemmma for mapdh6N 41748. 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 41743* | Lemmma for mapdh6N 41748. 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 41744* | Lemmma for mapdh6N 41748. 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 41745* | Lemmma for mapdh6N 41748. 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 41746* | Lemmma for mapdh6N 41748. 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 41747* | Lemmma for mapdh6N 41748. 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 41748* | Part (6) of [Baer] p. 47 line 6. Note that we use ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) which is equivalent to Baer's "Fx ∩ (Fy + Fz)" by lspdisjb 21043. 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 41822. (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 41749* | 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 41750* | 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 41751* | 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 41752* | 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 41753* | 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 41754.) (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 41754* | 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 41755* | 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 41756* | 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 41757 | Extend class notation with vector to dual map. |
| class HVMap | ||
| Definition | df-hvmap 41758* | 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 41552, dochfl1 41477- 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 41759* | 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 41760* | 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 41761* | 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 41762* | 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 41763 | 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 41764* | 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 41765* | 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 41766 | 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 41767 | 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 41768 | 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 41769 | Kernel of the vector to functional map. TODO: make this become lcfrlem11 41554. (Contributed by NM, 29-Mar-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐿‘(𝑀‘𝑋)) = (𝑂‘{𝑋})) | ||
| Theorem | mapdhvmap 41770 | Relationship between mapd and HVMap, which can be used to satisfy the last hypothesis of mapdpg 41707. 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 41771 | 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 21046 and prcom 4699.) (Contributed by NM, 4-May-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ (𝑁‘{𝑋, 𝑈})) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑈 ∈ (𝑁‘{𝑋, 𝑌})) | ||
| Theorem | hdmaplem1 41772 | 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 41773 | 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 41774 | 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 41775 | 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 41776* | 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 41777* | 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 41778* | 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 41779* | 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 41780* | 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 41781* | 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 41782* | 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 41783* | 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 41784* | 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 41785* | 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 41786* | Part of Part (8) in [Baer] p. 48. Eliminate 𝑋 ∈ (𝑁‘{𝑌, 𝑇}). TODO: break out 𝑇 ≠ 0 in mapdh8e 41785 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 41787* | 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 41788* | 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 41789* | 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 41790* | Lemma for part (9) in [Baer] p. 48. TODO: why is this 50% larger than mapdh9aOLDN 41791? (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 41791* | 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 41792 | Extend class notation with preliminary map from vectors to functionals in the closed kernel dual space. |
| class HDMap1 | ||
| Syntax | chdma 41793 | Extend class notation with map from vectors to functionals in the closed kernel dual space. |
| class HDMap | ||
| Definition | df-hdmap1 41794* | Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 41797 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 41795* | Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 41828 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 41796* | 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 41797* | 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 41798* | 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 41799* | Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval 41725.) TODO: change 𝐼 = (𝑥 ∈ V ↦... to (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌 > ) =... in e.g. mapdh8 41789 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 41800 | Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 41726.) (Contributed by NM, 17-May-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 0 ⟩) = 𝑄) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |