Home | Metamath
Proof Explorer Theorem List (p. 390 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mapdh7dN 38901* | 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 38902* | 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 38903* | 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 38904.) (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 38904* | 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 38905* | 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 38906* | 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 38907 | Extend class notation with vector to dual map. |
class HVMap | ||
Definition | df-hvmap 38908* | 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 38702, dochfl1 38627- 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 38909* | 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 38910* | 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 38911* | 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 38912* | 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 38913 | 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 38914* | 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 38915* | 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 38916 | 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 38917 | 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 38918 | 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 38919 | Kernel of the vector to functional map. TODO: make this become lcfrlem11 38704. (Contributed by NM, 29-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐿‘(𝑀‘𝑋)) = (𝑂‘{𝑋})) | ||
Theorem | mapdhvmap 38920 | Relationship between mapd and HVMap, which can be used to satisfy the last hypothesis of mapdpg 38857. 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 38921 | 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 19901 and prcom 4668.) (Contributed by NM, 4-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ (𝑁‘{𝑋, 𝑈})) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑈 ∈ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | hdmaplem1 38922 | 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 38923 | 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 38924 | 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 38925 | 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 38926* | 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 38927* | 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 38928* | 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 38929* | 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 38930* | 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 38931* | 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 38932* | 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 38933* | 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 38934* | 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 38935* | 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 38936* | Part of Part (8) in [Baer] p. 48. Eliminate 𝑋 ∈ (𝑁‘{𝑌, 𝑇}). TODO: break out 𝑇 ≠ 0 in mapdh8e 38935 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 38937* | 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 38938* | 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 38939* | 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 38940* | Lemma for part (9) in [Baer] p. 48. TODO: why is this 50% larger than mapdh9aOLDN 38941? (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 38941* | 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 38942 | Extend class notation with preliminary map from vectors to functionals in the closed kernel dual space. |
class HDMap1 | ||
Syntax | chdma 38943 | Extend class notation with map from vectors to functionals in the closed kernel dual space. |
class HDMap | ||
Definition | df-hdmap1 38944* | Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 38947 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 38945* | Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 38978 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 38946* | 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 38947* | 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 38948* | 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 38949* | Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval 38875.) TODO: change 𝐼 = (𝑥 ∈ V ↦... to (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌 > ) =... in e.g. mapdh8 38939 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 38950 | Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 38876.) (Contributed by NM, 17-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 0 〉) = 𝑄) | ||
Theorem | hdmap1val2 38951* | 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 38952 | 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 38953* | Frequently used lemma to change bound variables in 𝐿 hypothesis. (Contributed by NM, 15-May-2015.) |
⊢ 𝐿 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) ⇒ ⊢ 𝐿 = (𝑦 ∈ V ↦ if((2nd ‘𝑦) = 0 , 𝑄, (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑦)) − (2nd ‘𝑦))})) = (𝐽‘{((2nd ‘(1st ‘𝑦))𝑅𝑖)}))))) | ||
Theorem | hdmap1valc 38954* | Connect the value of the preliminary map from vectors to functionals 𝐼 to the hypothesis 𝐿 used by earlier theorems. Note: the 𝑋 ∈ (𝑉 ∖ { 0 }) hypothesis could be the more general 𝑋 ∈ 𝑉 but the former will be easier to use. TODO: use the 𝐼 function directly in those theorems, so this theorem becomes unnecessary? TODO: The hdmap1cbv 38953 is probably unnecessary, but it would mean different $d's later on. (Contributed by NM, 15-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ 𝐿 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = (𝐿‘〈𝑋, 𝐹, 𝑌〉)) | ||
Theorem | hdmap1cl 38955 | Convert closure theorem mapdhcl 38878 to use HDMap1 function. (Contributed by NM, 15-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) ∈ 𝐷) | ||
Theorem | hdmap1eq2 38956 | Convert mapdheq2 38880 to use HDMap1 function. (Contributed by NM, 16-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = 𝐺) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑌, 𝐺, 𝑋〉) = 𝐹) | ||
Theorem | hdmap1eq4N 38957 | Convert mapdheq4 38883 to use HDMap1 function. (Contributed by NM, 17-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = 𝐺) & ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑍〉) = 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑌, 𝐺, 𝑍〉) = 𝐵) | ||
Theorem | hdmap1l6lem1 38958 | Lemma for hdmap1l6 38972. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = 𝐺) & ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑍〉) = 𝐸) ⇒ ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − (𝑌 + 𝑍))})) = (𝐿‘{(𝐹𝑅(𝐺 ✚ 𝐸))})) | ||
Theorem | hdmap1l6lem2 38959 | Lemma for hdmap1l6 38972. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = 𝐺) & ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑍〉) = 𝐸) ⇒ ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑌 + 𝑍)})) = (𝐿‘{(𝐺 ✚ 𝐸)})) | ||
Theorem | hdmap1l6a 38960 | Lemma for hdmap1l6 38972. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = 𝐺) & ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑍〉) = 𝐸) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉) = ((𝐼‘〈𝑋, 𝐹, 𝑌〉) ✚ (𝐼‘〈𝑋, 𝐹, 𝑍〉))) | ||
Theorem | hdmap1l6b0N 38961 | Lemmma for hdmap1l6 38972. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ (𝑁‘{𝑌, 𝑍})) = { 0 }) ⇒ ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) | ||
Theorem | hdmap1l6b 38962 | Lemmma for hdmap1l6 38972. (Contributed by NM, 24-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → 𝑌 = 0 ) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉) = ((𝐼‘〈𝑋, 𝐹, 𝑌〉) ✚ (𝐼‘〈𝑋, 𝐹, 𝑍〉))) | ||
Theorem | hdmap1l6c 38963 | Lemmma for hdmap1l6 38972. (Contributed by NM, 24-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 = 0 ) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉) = ((𝐼‘〈𝑋, 𝐹, 𝑌〉) ✚ (𝐼‘〈𝑋, 𝐹, 𝑍〉))) | ||
Theorem | hdmap1l6d 38964 | Lemmma for hdmap1l6 38972. (Contributed by NM, 1-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))〉) = ((𝐼‘〈𝑋, 𝐹, 𝑤〉) ✚ (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉))) | ||
Theorem | hdmap1l6e 38965 | Lemmma for hdmap1l6 38972. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, ((𝑤 + 𝑌) + 𝑍)〉) = ((𝐼‘〈𝑋, 𝐹, (𝑤 + 𝑌)〉) ✚ (𝐼‘〈𝑋, 𝐹, 𝑍〉))) | ||
Theorem | hdmap1l6f 38966 | Lemmma for hdmap1l6 38972. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, (𝑤 + 𝑌)〉) = ((𝐼‘〈𝑋, 𝐹, 𝑤〉) ✚ (𝐼‘〈𝑋, 𝐹, 𝑌〉))) | ||
Theorem | hdmap1l6g 38967 | Lemmma for hdmap1l6 38972. Part (6) of [Baer] p. 47 line 39. (Contributed by NM, 1-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ((𝐼‘〈𝑋, 𝐹, 𝑤〉) ✚ (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉)) = (((𝐼‘〈𝑋, 𝐹, 𝑤〉) ✚ (𝐼‘〈𝑋, 𝐹, 𝑌〉)) ✚ (𝐼‘〈𝑋, 𝐹, 𝑍〉))) | ||
Theorem | hdmap1l6h 38968 | Lemmma for hdmap1l6 38972. Part (6) of [Baer] p. 48 line 2. (Contributed by NM, 1-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉) = ((𝐼‘〈𝑋, 𝐹, 𝑌〉) ✚ (𝐼‘〈𝑋, 𝐹, 𝑍〉))) | ||
Theorem | hdmap1l6i 38969 | Lemmma for hdmap1l6 38972. Eliminate auxiliary vector 𝑤. (Contributed by NM, 1-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉) = ((𝐼‘〈𝑋, 𝐹, 𝑌〉) ✚ (𝐼‘〈𝑋, 𝐹, 𝑍〉))) | ||
Theorem | hdmap1l6j 38970 | Lemmma for hdmap1l6 38972. Eliminate (𝑁 { Y } ) = ( N {𝑍}) hypothesis. (Contributed by NM, 1-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉) = ((𝐼‘〈𝑋, 𝐹, 𝑌〉) ✚ (𝐼‘〈𝑋, 𝐹, 𝑍〉))) | ||
Theorem | hdmap1l6k 38971 | Lemmma for hdmap1l6 38972. Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉) = ((𝐼‘〈𝑋, 𝐹, 𝑌〉) ✚ (𝐼‘〈𝑋, 𝐹, 𝑍〉))) | ||
Theorem | hdmap1l6 38972 | Part (6) of [Baer] p. 47 line 6. Note that we use ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) which is equivalent to Baer's "Fx ∩ (Fy + Fz)" by lspdisjb 19898. (Convert mapdh6N 38898 to use the function HDMap1.) (Contributed by NM, 17-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) ⇒ ⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉) = ((𝐼‘〈𝑋, 𝐹, 𝑌〉) ✚ (𝐼‘〈𝑋, 𝐹, 𝑍〉))) | ||
Theorem | hdmap1eulem 38973* | Lemma for hdmap1eu 38975. TODO: combine with hdmap1eu 38975 or at least share some hypotheses. (Contributed by NM, 15-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) & ⊢ 𝐿 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) ⇒ ⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉))) | ||
Theorem | hdmap1eulemOLDN 38974* | Lemma for hdmap1euOLDN 38976. TODO: combine with hdmap1euOLDN 38976 or at least share some hypotheses. (Contributed by NM, 15-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) & ⊢ 𝐿 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)}))))) ⇒ ⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇}) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉))) | ||
Theorem | hdmap1eu 38975* | Convert mapdh9a 38940 to use the HDMap1 notation. (Contributed by NM, 15-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉))) | ||
Theorem | hdmap1euOLDN 38976* | Convert mapdh9aOLDN 38941 to use the HDMap1 notation. (Contributed by NM, 15-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇}) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉))) | ||
Theorem | hdmapffval 38977* | Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑋 → (HDMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})) | ||
Theorem | hdmapfval 38978* | Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑆 = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) | ||
Theorem | hdmapval 38979* | Value of map from vectors to functionals in the closed kernel dual space. This is the function sigma on line 27 above part 9 in [Baer] p. 48. We select a convenient fixed reference vector 𝐸 to be 〈0, 1〉 (corresponding to vector u on p. 48 line 7) whose span is the lattice isomorphism map of the fiducial atom 𝑃 = ((oc‘𝐾)‘𝑊) (see dvheveccl 38263). (𝐽‘𝐸) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap 38920 shows in Baer's notation (Fu)* = Gu'). Baer's independent vectors v and w on line 7 correspond to our 𝑧 that the ∀𝑧 ∈ 𝑉 ranges over. The middle term (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉) provides isolation to allow 𝐸 and 𝑇 to assume the same value without conflict. Closure is shown by hdmapcl 38981. If a separate auxiliary vector is known, hdmapval2 38983 provides a version without quantification. (Contributed by NM, 15-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑆‘𝑇) = (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑇〉)))) | ||
Theorem | hdmapfnN 38980 | Functionality of map from vectors to functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑆 Fn 𝑉) | ||
Theorem | hdmapcl 38981 | Closure of map from vectors to functionals with closed kernels. (Contributed by NM, 15-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑆‘𝑇) ∈ 𝐷) | ||
Theorem | hdmapval2lem 38982* | Lemma for hdmapval2 38983. (Contributed by NM, 15-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) ⇒ ⊢ (𝜑 → ((𝑆‘𝑇) = 𝐹 ↔ ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑇})) → 𝐹 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑇〉)))) | ||
Theorem | hdmapval2 38983 | Value of map from vectors to functionals with a specific auxiliary vector. TODO: Would shorter proofs result if the .ne hypothesis were changed to two ≠ hypothesis? Consider hdmaplem1 38922 through hdmaplem4 38925, which would become obsolete. (Contributed by NM, 15-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑇}))) ⇒ ⊢ (𝜑 → (𝑆‘𝑇) = (𝐼‘〈𝑋, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑋〉), 𝑇〉)) | ||
Theorem | hdmapval0 38984 | Value of map from vectors to functionals at zero. Note: we use dvh3dim 38597 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 38995 could be derived from the other to shorten proof. (Contributed by NM, 17-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → (𝑆‘ 0 ) = 𝑄) | ||
Theorem | hdmapeveclem 38985 | Lemma for hdmapevec 38986. TODO: combine with hdmapevec 38986 if it shortens overall. (Contributed by NM, 16-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝐸}))) ⇒ ⊢ (𝜑 → (𝑆‘𝐸) = (𝐽‘𝐸)) | ||
Theorem | hdmapevec 38986 | Value of map from vectors to functionals at the reference vector 𝐸. (Contributed by NM, 16-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → (𝑆‘𝐸) = (𝐽‘𝐸)) | ||
Theorem | hdmapevec2 38987 | The inner product of the reference vector 𝐸 with itself is nonzero. This shows the inner product condition in the proof of Theorem 3.6 of [Holland95] p. 14 line 32, [ e , e ] ≠ 0 is satisfied. TODO: remove redundant hypothesis hdmapevec.j. (Contributed by NM, 1-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑆‘𝐸)‘𝐸) = 1 ) | ||
Theorem | hdmapval3lemN 38988 | Value of map from vectors to functionals at arguments not colinear with the reference vector 𝐸. (Contributed by NM, 17-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑁‘{𝑇}) ≠ (𝑁‘{𝐸})) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ {(0g‘𝑈)})) & ⊢ (𝜑 → 𝑥 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑥 ∈ (𝑁‘{𝐸, 𝑇})) ⇒ ⊢ (𝜑 → (𝑆‘𝑇) = (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑇〉)) | ||
Theorem | hdmapval3N 38989 | Value of map from vectors to functionals at arguments not colinear with the reference vector 𝐸. (Contributed by NM, 17-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑁‘{𝑇}) ≠ (𝑁‘{𝐸})) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑆‘𝑇) = (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑇〉)) | ||
Theorem | hdmap10lem 38990 | Lemma for hdmap10 38991. (Contributed by NM, 17-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑇})) = (𝐿‘{(𝑆‘𝑇)})) | ||
Theorem | hdmap10 38991 | Part 10 in [Baer] p. 48 line 33, (Ft)* = G(tS) in their notation (S = sigma). (Contributed by NM, 17-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑇})) = (𝐿‘{(𝑆‘𝑇)})) | ||
Theorem | hdmap11lem1 38992 | Lemma for hdmapadd 38994. (Contributed by NM, 26-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) & ⊢ (𝜑 → 𝑧 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌})) & ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{𝐸})) ⇒ ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌))) | ||
Theorem | hdmap11lem2 38993 | Lemma for hdmapadd 38994. (Contributed by NM, 26-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) ⇒ ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌))) | ||
Theorem | hdmapadd 38994 | Part 11 in [Baer] p. 48 line 35, (a+b)S = aS+bS in their notation (S = sigma). (Contributed by NM, 22-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ ✚ = (+g‘𝐶) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌))) | ||
Theorem | hdmapeq0 38995 | Part of proof of part 12 in [Baer] p. 49 line 3. (Contributed by NM, 22-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑆‘𝑇) = 𝑄 ↔ 𝑇 = 0 )) | ||
Theorem | hdmapnzcl 38996 | Nonzero vector closure of map from vectors to functionals with closed kernels. (Contributed by NM, 27-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑆‘𝑇) ∈ (𝐷 ∖ {𝑄})) | ||
Theorem | hdmapneg 38997 | Part of proof of part 12 in [Baer] p. 49 line 4. The sigma map of a negative is the negative of the sigma map. (Contributed by NM, 24-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑀 = (invg‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐼 = (invg‘𝐶) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑆‘(𝑀‘𝑇)) = (𝐼‘(𝑆‘𝑇))) | ||
Theorem | hdmapsub 38998 | Part of proof of part 12 in [Baer] p. 49 line 5, (a-b)S = aS-bS in their notation (S = sigma). (Contributed by NM, 26-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑁 = (-g‘𝐶) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑆‘(𝑋 − 𝑌)) = ((𝑆‘𝑋)𝑁(𝑆‘𝑌))) | ||
Theorem | hdmap11 38999 | Part of proof of part 12 in [Baer] p. 49 line 4, aS=bS iff a=b in their notation (S = sigma). The sigma map is one-to-one. (Contributed by NM, 26-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑆‘𝑋) = (𝑆‘𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | hdmaprnlem1N 39000 | Part of proof of part 12 in [Baer] p. 49 line 10, Gu' ≠ Gs. Our (𝑁‘{𝑣}) is Baer's T. (Contributed by NM, 26-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐿 = (LSpan‘𝐶) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄})) & ⊢ (𝜑 → 𝑣 ∈ 𝑉) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠})) & ⊢ (𝜑 → 𝑢 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣})) ⇒ ⊢ (𝜑 → (𝐿‘{(𝑆‘𝑢)}) ≠ (𝐿‘{𝑠})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |