P. 426 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42501-42600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hdmapf1oN 42501	Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 42479, this shows the map is an automorphism from the additive group of vectors to the additive group of functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑆:𝑉–1-1-onto→𝐷)
Theorem	hdmap14lem1a 42502	Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐹 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐿‘{(𝑆‘𝑋)}) = (𝐿‘{(𝑆‘(𝐹 · 𝑋))}))
Theorem	hdmap14lem2a 42503*	Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include 𝐹 = 0 so it can be used in hdmap14lem10 42513. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem1 42504	Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑄 = (0g‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ∖ {𝑍}))    ⇒   ⊢ (𝜑 → (𝐿‘{(𝑆‘𝑋)}) = (𝐿‘{(𝑆‘(𝐹 · 𝑋))}))
Theorem	hdmap14lem2N 42505*	Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include 𝐹 = 𝑍 so it can be used in hdmap14lem10 42513. (Contributed by NM, 31-May-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑄 = (0g‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ∖ {𝑍}))    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ (𝐴 ∖ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem3 42506*	Prior to part 14 in [Baer] p. 49, line 26. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑄 = (0g‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ∖ {𝑍}))    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ (𝐴 ∖ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem4a 42507*	Simplify (𝐴 ∖ {𝑄}) in hdmap14lem3 42506 to provide a slightly simpler definition later. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑄 = (0g‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ∖ {𝑍}))    ⇒   ⊢ (𝜑 → (∃!𝑔 ∈ (𝐴 ∖ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) ↔ ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋))))
Theorem	hdmap14lem4 42508*	Simplify (𝐴 ∖ {𝑄}) in hdmap14lem3 42506 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 42507 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 42507 into this one. (Contributed by NM, 31-May-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑄 = (0g‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ∖ {𝑍}))    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem6 42509*	Case where 𝐹 is zero. (Contributed by NM, 1-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝐿 = (LSpan‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑄 = (0g‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 = 𝑍)    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem7 42510*	Combine cases of 𝐹. TODO: Can this be done at once in hdmap14lem3 42506, in order to get rid of hdmap14lem6 42509? Perhaps modify lspsneu 21216 to become ∃!𝑘 ∈ 𝐾 instead of ∃!𝑘 ∈ (𝐾 ∖ { 0 })? (Contributed by NM, 1-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
Theorem	hdmap14lem8 42511	Part of proof of part 14 in [Baer] p. 49 lines 33-35. (Contributed by NM, 1-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = (𝐺 ∙ (𝑆‘𝑋)))    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑌)) = (𝐼 ∙ (𝑆‘𝑌)))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → 𝐽 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑆‘(𝐹 · (𝑋 + 𝑌))) = (𝐽 ∙ (𝑆‘(𝑋 + 𝑌))))    ⇒   ⊢ (𝜑 → ((𝐽 ∙ (𝑆‘𝑋)) ✚ (𝐽 ∙ (𝑆‘𝑌))) = ((𝐺 ∙ (𝑆‘𝑋)) ✚ (𝐼 ∙ (𝑆‘𝑌))))
Theorem	hdmap14lem9 42512	Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 1-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = (𝐺 ∙ (𝑆‘𝑋)))    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑌)) = (𝐼 ∙ (𝑆‘𝑌)))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → 𝐽 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑆‘(𝐹 · (𝑋 + 𝑌))) = (𝐽 ∙ (𝑆‘(𝑋 + 𝑌))))    ⇒   ⊢ (𝜑 → 𝐺 = 𝐼)
Theorem	hdmap14lem10 42513	Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 3-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = (𝐺 ∙ (𝑆‘𝑋)))    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑌)) = (𝐼 ∙ (𝑆‘𝑌)))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → 𝐺 = 𝐼)
Theorem	hdmap14lem11 42514	Part of proof of part 14 in [Baer] p. 50 line 3. (Contributed by NM, 3-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = (𝐺 ∙ (𝑆‘𝑋)))    &   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑌)) = (𝐼 ∙ (𝑆‘𝑌)))    ⇒   ⊢ (𝜑 → 𝐺 = 𝐼)
Theorem	hdmap14lem12 42515*	Lemma for proof of part 14 in [Baer] p. 50. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑆‘(𝐹 · 𝑋)) = (𝐺 ∙ (𝑆‘𝑋)) ↔ ∀𝑦 ∈ (𝑉 ∖ { 0 })(𝑆‘(𝐹 · 𝑦)) = (𝐺 ∙ (𝑆‘𝑦))))
Theorem	hdmap14lem13 42516*	Lemma for proof of part 14 in [Baer] p. 50. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑆‘(𝐹 · 𝑋)) = (𝐺 ∙ (𝑆‘𝑋)) ↔ ∀𝑦 ∈ 𝑉 (𝑆‘(𝐹 · 𝑦)) = (𝐺 ∙ (𝑆‘𝑦))))
Theorem	hdmap14lem14 42517*	Part of proof of part 14 in [Baer] p. 50 line 3. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ 𝐴 ∀𝑥 ∈ 𝑉 (𝑆‘(𝐹 · 𝑥)) = (𝑔 ∙ (𝑆‘𝑥)))
Theorem	hdmap14lem15 42518*	Part of proof of part 14 in [Baer] p. 50 line 3. Convert scalar base of dual to scalar base of vector space. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ 𝐵 ∀𝑥 ∈ 𝑉 (𝑆‘(𝐹 · 𝑥)) = (𝑔 ∙ (𝑆‘𝑥)))
Syntax	chg 42519	Extend class notation with g-map.
class HGMap
Definition	df-hgmap 42520*	Define map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
⊢ HGMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 ∀𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠 ‘𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚‘𝑣))))}))
Theorem	hgmapffval 42521*	Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑋 → (HGMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 ∀𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠 ‘𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚‘𝑣))))}))
Theorem	hgmapfval 42522*	Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑀 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐼 = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 ∀𝑣 ∈ 𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 ∙ (𝑀‘𝑣)))))
Theorem	hgmapval 42523*	Value of map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. Function sigma of scalar f in part 14 of [Baer] p. 50 line 4. TODO: variable names are inherited from older version. Maybe make more consistent with hdmap14lem15 42518. (Contributed by NM, 25-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑀 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) = (℩𝑦 ∈ 𝐵 ∀𝑣 ∈ 𝑉 (𝑀‘(𝑋 · 𝑣)) = (𝑦 ∙ (𝑀‘𝑣))))
Theorem	hgmapfnN 42524	Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐺 Fn 𝐵)
Theorem	hgmapcl 42525	Closure of scalar sigma map i.e. the map from the vector space scalar base to the dual space scalar base. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘𝐹) ∈ 𝐵)
Theorem	hgmapdcl 42526	Closure of the vector space to dual space scalar map, in the scalar sigma map. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑄 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑄)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘𝐹) ∈ 𝐴)
Theorem	hgmapvs 42527	Part 15 of [Baer] p. 50 line 6. Also line 15 in [Holland95] p. 14. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = ((𝐺‘𝐹) ∙ (𝑆‘𝑋)))
Theorem	hgmapval0 42528	Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → (𝐺‘ 0 ) = 0 )
Theorem	hgmapval1 42529	Value of the scalar sigma map at one. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → (𝐺‘ 1 ) = 1 )
Theorem	hgmapadd 42530	Part 15 of [Baer] p. 50 line 13. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘(𝑋 + 𝑌)) = ((𝐺‘𝑋) + (𝐺‘𝑌)))
Theorem	hgmapmul 42531	Part 15 of [Baer] p. 50 line 16. The multiplication is reversed after converting to the dual space scalar to the vector space scalar. (Contributed by NM, 7-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘(𝑋 · 𝑌)) = ((𝐺‘𝑌) · (𝐺‘𝑋)))
Theorem	hgmaprnlem1N 42532	Lemma for hgmaprnN 42537. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑡 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑠 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆‘𝑠) = (𝑧 ∙ (𝑆‘𝑡)))    &   ⊢ (𝜑 → 𝑘 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑠 = (𝑘 · 𝑡))    ⇒   ⊢ (𝜑 → 𝑧 ∈ ran 𝐺)
Theorem	hgmaprnlem2N 42533	Lemma for hgmaprnN 42537. Part 15 of [Baer] p. 50 line 20. We only require a subset relation, rather than equality, so that the case of zero 𝑧 is taken care of automatically. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑡 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑠 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆‘𝑠) = (𝑧 ∙ (𝑆‘𝑡)))    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LSpan‘𝐶)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑠}) ⊆ (𝑁‘{𝑡}))
Theorem	hgmaprnlem3N 42534*	Lemma for hgmaprnN 42537. Eliminate 𝑘. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑡 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑠 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑆‘𝑠) = (𝑧 ∙ (𝑆‘𝑡)))    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐿 = (LSpan‘𝐶)    ⇒   ⊢ (𝜑 → 𝑧 ∈ ran 𝐺)
Theorem	hgmaprnlem4N 42535*	Lemma for hgmaprnN 42537. Eliminate 𝑠. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑡 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → 𝑧 ∈ ran 𝐺)
Theorem	hgmaprnlem5N 42536	Lemma for hgmaprnN 42537. Eliminate 𝑡. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (Base‘𝐶)    &   ⊢ 𝑃 = (Scalar‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑄 = (0g‘𝐶)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑧 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑧 ∈ ran 𝐺)
Theorem	hgmaprnN 42537	Part of proof of part 16 in [Baer] p. 50 line 23, Fs=G, except that we use the original vector space scalars for the range. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ran 𝐺 = 𝐵)
Theorem	hgmap11 42538	The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐺‘𝑋) = (𝐺‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	hgmapf1oN 42539	The scalar sigma map is a one-to-one onto function. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐵)
Theorem	hgmapeq0 42540	The scalar sigma map is zero iff its argument is zero. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐺‘𝑋) = 0 ↔ 𝑋 = 0 ))
Theorem	hdmapipcl 42541	The inner product (Hermitian form) (𝑋, 𝑌) will be defined as ((𝑆‘𝑌)‘𝑋). Show closure. (Contributed by NM, 7-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑌)‘𝑋) ∈ 𝐵)
Theorem	hdmapln1 42542	Linearity property that will be used for inner product. TODO: try to combine hypotheses in hdmap*ln* series. (Contributed by NM, 7-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑍)‘((𝐴 · 𝑋) + 𝑌)) = ((𝐴 × ((𝑆‘𝑍)‘𝑋)) ⨣ ((𝑆‘𝑍)‘𝑌)))
Theorem	hdmaplna1 42543	Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 + 𝑌)) = (((𝑆‘𝑍)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑌)))
Theorem	hdmaplns1 42544	Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝑁 = (-g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 − 𝑌)) = (((𝑆‘𝑍)‘𝑋)𝑁((𝑆‘𝑍)‘𝑌)))
Theorem	hdmaplnm1 42545	Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑌)‘(𝐴 · 𝑋)) = (𝐴 × ((𝑆‘𝑌)‘𝑋)))
Theorem	hdmaplna2 42546	Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘(𝑌 + 𝑍))‘𝑋) = (((𝑆‘𝑌)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑋)))
Theorem	hdmapglnm2 42547	g-linear property of second (inner product) argument. Line 19 in [Holland95] p. 14. (Contributed by NM, 10-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑆‘(𝐴 · 𝑌))‘𝑋) = (((𝑆‘𝑌)‘𝑋) × (𝐺‘𝐴)))
Theorem	hdmapgln2 42548	g-linear property that will be used for inner product. (Contributed by NM, 14-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑆‘((𝐴 · 𝑌) + 𝑍))‘𝑋) = ((((𝑆‘𝑌)‘𝑋) × (𝐺‘𝐴)) ⨣ ((𝑆‘𝑍)‘𝑋)))
Theorem	hdmaplkr 42549	Kernel of the vector to dual map. Line 16 in [Holland95] p. 14. TODO: eliminate 𝐹 hypothesis. (Contributed by NM, 9-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝑌 = (LKer‘𝑈)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑌‘(𝑆‘𝑋)) = (𝑂‘{𝑋}))
Theorem	hdmapellkr 42550	Membership in the kernel (as shown by hdmaplkr 42549) of the vector to dual map. Line 17 in [Holland95] p. 14. (Contributed by NM, 16-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑌) = 0 ↔ 𝑌 ∈ (𝑂‘{𝑋})))
Theorem	hdmapip0 42551	Zero property that will be used for inner product. (Contributed by NM, 9-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑋) = 𝑍 ↔ 𝑋 = 0 ))
Theorem	hdmapip1 42552	Construct a proportional vector 𝑌 whose inner product with the original 𝑋 equals one. (Contributed by NM, 13-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invr‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ 𝑌 = ((𝑁‘((𝑆‘𝑋)‘𝑋)) · 𝑋)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑋)‘𝑌) = 1 )
Theorem	hdmapip0com 42553	Commutation property of Baer's sigma map (Holland's A map). Line 20 of [Holland95] p. 14. Also part of Lemma 1 of [Baer] p. 110 line 7. (Contributed by NM, 9-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑌) = 0 ↔ ((𝑆‘𝑌)‘𝑋) = 0 ))
Theorem	hdmapinvlem1 42554	Line 27 in [Baer] p. 110. We use 𝐶 for Baer's u. Our unit vector 𝐸 has the required properties for his w by hdmapevec2 42472. Our ((𝑆‘𝐸)‘𝐶) means the inner product ⟨𝐶, 𝐸⟩ i.e. his f(u,w) (note argument reversal). (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    ⇒   ⊢ (𝜑 → ((𝑆‘𝐸)‘𝐶) = 0 )
Theorem	hdmapinvlem2 42555	Line 28 in [Baer] p. 110, 0 = f(w,u). (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    ⇒   ⊢ (𝜑 → ((𝑆‘𝐶)‘𝐸) = 0 )
Theorem	hdmapinvlem3 42556	Line 30 in [Baer] p. 110, f(sw + u, tw - v) = 0. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐼 × (𝐺‘𝐽)) = ((𝑆‘𝐷)‘𝐶))    ⇒   ⊢ (𝜑 → ((𝑆‘((𝐽 · 𝐸) − 𝐷))‘((𝐼 · 𝐸) + 𝐶)) = 0 )
Theorem	hdmapinvlem4 42557	Part 1.1 of Proposition 1 of [Baer] p. 110. We use 𝐶, 𝐷, 𝐼, and 𝐽 for Baer's u, v, s, and t. Our unit vector 𝐸 has the required properties for his w by hdmapevec2 42472. Our ((𝑆‘𝐷)‘𝐶) means his f(u,v) (note argument reversal). (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐼 × (𝐺‘𝐽)) = ((𝑆‘𝐷)‘𝐶))    ⇒   ⊢ (𝜑 → (𝐽 × (𝐺‘𝐼)) = ((𝑆‘𝐶)‘𝐷))
Theorem	hdmapglem5 42558	Part 1.2 in [Baer] p. 110 line 34, f(u,v) alpha = f(v,u). (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘((𝑆‘𝐷)‘𝐶)) = ((𝑆‘𝐶)‘𝐷))
Theorem	hgmapvvlem1 42559	Involution property of scalar sigma map. Line 10 in [Baer] p. 111, t sigma squared = t. Our 𝐸, 𝐶, 𝐷, 𝑌, 𝑋 correspond to Baer's w, h, k, s, t. (Contributed by NM, 13-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invr‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → ((𝑆‘𝐷)‘𝐶) = 1 )    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑌 × (𝐺‘𝑋)) = 1 )    ⇒   ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋)
Theorem	hgmapvvlem2 42560	Lemma for hgmapvv 42562. Eliminate 𝑌 (Baer's s). (Contributed by NM, 13-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invr‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → ((𝑆‘𝐷)‘𝐶) = 1 )    ⇒   ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋)
Theorem	hgmapvvlem3 42561	Lemma for hgmapvv 42562. Eliminate ((𝑆‘𝐷)‘𝐶) = 1 (Baer's f(h,k)=1). (Contributed by NM, 13-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invr‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋)
Theorem	hgmapvv 42562	Value of a double involution. Part 1.2 of [Baer] p. 110 line 37. (Contributed by NM, 13-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋)
Theorem	hdmapglem7a 42563*	Lemma for hdmapg 42566. (Contributed by NM, 14-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ (𝑂‘{𝐸})∃𝑘 ∈ 𝐵 𝑋 = ((𝑘 · 𝐸) + 𝑢))
Theorem	hdmapglem7b 42564	Lemma for hdmapg 42566. (Contributed by NM, 14-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ ✚ = (+g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑂‘{𝐸}))    &   ⊢ (𝜑 → 𝑚 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑛 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑆‘((𝑚 · 𝐸) + 𝑥))‘((𝑛 · 𝐸) + 𝑦)) = ((𝑛 × (𝐺‘𝑚)) ✚ ((𝑆‘𝑥)‘𝑦)))
Theorem	hdmapglem7 42565	Lemma for hdmapg 42566. Line 15 in [Baer] p. 111, f(x,y) alpha = f(y,x). In the proof, our 𝐸, (𝑂‘{𝐸}), 𝑋, 𝑌, 𝑘, 𝑢, 𝑙, and 𝑣 correspond respectively to Baer's w, H, x, y, x', x'', y', and y'', and our ((𝑆‘𝑌)‘𝑋) corresponds to Baer's f(x,y). (Contributed by NM, 14-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ ✚ = (+g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐺‘((𝑆‘𝑌)‘𝑋)) = ((𝑆‘𝑋)‘𝑌))
Theorem	hdmapg 42566	Apply the scalar sigma function (involution) 𝐺 to an inner product reverses the arguments. The inner product of 𝑋 and 𝑌 is represented by ((𝑆‘𝑌)‘𝑋). Line 15 in [Baer] p. 111, f(x,y) alpha = f(y,x). (Contributed by NM, 14-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐺‘((𝑆‘𝑌)‘𝑋)) = ((𝑆‘𝑋)‘𝑌))
Theorem	hdmapoc 42567*	Express our constructed orthocomplement (polarity) in terms of the Hilbert space definition of orthocomplement. Lines 24 and 25 in [Holland95] p. 14. (Contributed by NM, 17-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑂‘𝑋) = {𝑦 ∈ 𝑉 ∣ ∀𝑧 ∈ 𝑋 ((𝑆‘𝑧)‘𝑦) = 0 })
Syntax	chlh 42568	Extend class notation with the final constructed Hilbert space.
class HLHil
Definition	df-hlhil 42569*	Define our final Hilbert space constructed from a Hilbert lattice. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ HLHil = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g‘𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠 ‘𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})))
Theorem	hlhilset 42570*	The final Hilbert space constructed from a Hilbert lattice 𝐾 and an arbitrary hyperplane 𝑊 in 𝐾. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐿 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (𝐸 sSet ⟨(*𝑟‘ndx), 𝐺⟩)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ , = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑉 ↦ ((𝑆‘𝑦)‘𝑥))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐿 = ({⟨(Base‘ndx), 𝑉⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}))
Theorem	hlhilsca 42571	The scalar of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (𝐸 sSet ⟨(*𝑟‘ndx), 𝐺⟩)    ⇒   ⊢ (𝜑 → 𝑅 = (Scalar‘𝑈))
Theorem	hlhilbase 42572	The base set of the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = (Base‘𝐿)    ⇒   ⊢ (𝜑 → 𝑀 = (Base‘𝑈))
Theorem	hlhilplus 42573	The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝐿)    ⇒   ⊢ (𝜑 → + = (+g‘𝑈))
Theorem	hlhilslem 42574	Lemma for hlhilsbase 42575 etc. (Contributed by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐹 = Slot (𝐹‘ndx)    &   ⊢ (𝐹‘ndx) ≠ (*𝑟‘ndx)    &   ⊢ 𝐶 = (𝐹‘𝐸)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐹‘𝑅))
Theorem	hlhilsbase 42575	The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → 𝐶 = (Base‘𝑅))
Theorem	hlhilsplus 42576	Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ + = (+g‘𝐸)    ⇒   ⊢ (𝜑 → + = (+g‘𝑅))
Theorem	hlhilsmul 42577	Scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ · = (.r‘𝐸)    ⇒   ⊢ (𝜑 → · = (.r‘𝑅))
Theorem	hlhilsbase2 42578	The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐿)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝜑 → 𝐶 = (Base‘𝑅))
Theorem	hlhilsplus2 42579	Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐿)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ (𝜑 → + = (+g‘𝑅))
Theorem	hlhilsmul2 42580	Scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐿)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ · = (.r‘𝑆)    ⇒   ⊢ (𝜑 → · = (.r‘𝑅))
Theorem	hlhils0 42581	The scalar ring zero for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐿)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ (𝜑 → 0 = (0g‘𝑅))
Theorem	hlhils1N 42582	The scalar ring unity for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐿)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 1 = (1r‘𝑆)    ⇒   ⊢ (𝜑 → 1 = (1r‘𝑅))
Theorem	hlhilvsca 42583	The scalar product for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐿)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → · = ( ·𝑠 ‘𝑈))
Theorem	hlhilip 42584*	Inner product operation for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝐿)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ , = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑉 ↦ ((𝑆‘𝑦)‘𝑥))    ⇒   ⊢ (𝜑 → , = (·𝑖‘𝑈))
Theorem	hlhilipval 42585	Value of inner product operation for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝐿)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ , = (·𝑖‘𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 , 𝑌) = ((𝑆‘𝑌)‘𝑋))
Theorem	hlhilnvl 42586	The involution operation of the star division ring for the final constructed Hilbert space. (Contributed by NM, 20-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ ∗ = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ∗ = (*𝑟‘𝑅))
Theorem	hlhillvec 42587	The final constructed Hilbert space is a vector space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑈 ∈ LVec)
Theorem	hlhildrng 42588	The star division ring for the final constructed Hilbert space is a division ring. (Contributed by NM, 20-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝑅 = (Scalar‘𝑈)    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	hlhilsrnglem 42589	Lemma for hlhilsrng 42590. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐿)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ · = (.r‘𝑆)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    ⇒   ⊢ (𝜑 → 𝑅 ∈ *-Ring)
Theorem	hlhilsrng 42590	The star division ring for the final constructed Hilbert space is a division ring. (Contributed by NM, 21-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝑅 = (Scalar‘𝑈)    ⇒   ⊢ (𝜑 → 𝑅 ∈ *-Ring)
Theorem	hlhil0 42591	The zero vector for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 0 = (0g‘𝐿)    ⇒   ⊢ (𝜑 → 0 = (0g‘𝑈))
Theorem	hlhillsm 42592	The vector sum operation for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ ⊕ = (LSSum‘𝐿)    ⇒   ⊢ (𝜑 → ⊕ = (LSSum‘𝑈))
Theorem	hlhilocv 42593	The orthocomplement for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝑉 = (Base‘𝐿)    &   ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (ocv‘𝑈)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑉)    ⇒   ⊢ (𝜑 → (𝑂‘𝑋) = (𝑁‘𝑋))
Theorem	hlhillcs 42594	The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 42572 is applied over and over to conclusion rather than applied once to antecedent - would compressed proof be shorter if applied once to antecedent? (Contributed by NM, 23-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝐶 = (ClSubSp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐶 = ran 𝐼)
Theorem	hlhilphllem 42595*	Lemma for hlhil 25563. (Contributed by NM, 23-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐹 = (Scalar‘𝑈)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝐿)    &   ⊢ + = (+g‘𝐿)    &   ⊢ · = ( ·𝑠 ‘𝐿)    &   ⊢ 𝑅 = (Scalar‘𝐿)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑄 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝐿)    &   ⊢ , = (·𝑖‘𝑈)    &   ⊢ 𝐽 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ 𝐸 = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑉 ↦ ((𝐽‘𝑦)‘𝑥))    ⇒   ⊢ (𝜑 → 𝑈 ∈ PreHil)
Theorem	hlhilhillem 42596*	Lemma for hlhil 25563. (Contributed by NM, 23-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐹 = (Scalar‘𝑈)    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝐿)    &   ⊢ + = (+g‘𝐿)    &   ⊢ · = ( ·𝑠 ‘𝐿)    &   ⊢ 𝑅 = (Scalar‘𝐿)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑄 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝐿)    &   ⊢ , = (·𝑖‘𝑈)    &   ⊢ 𝐽 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ 𝐸 = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑉 ↦ ((𝐽‘𝑦)‘𝑥))    &   ⊢ 𝑂 = (ocv‘𝑈)    &   ⊢ 𝐶 = (ClSubSp‘𝑈)    ⇒   ⊢ (𝜑 → 𝑈 ∈ Hil)
Theorem	hlathil 42597	Construction of a Hilbert space (df-hil 21814) 𝑈 from a Hilbert lattice (df-hlat 39987) 𝐾, where 𝑊 is a fixed but arbitrary hyperplane (co-atom) in 𝐾. The Hilbert space 𝑈 is identical to the vector space ((DVecH‘𝐾)‘𝑊) (see dvhlvec 41745) except that it is extended with involution and inner product components. The construction of these two components is provided by Theorem 3.6 in [Holland95] p. 13, whose proof we follow loosely. An example of involution is the complex conjugate when the division ring is the field of complex numbers. The nature of the division ring we constructed is indeterminate, however, until we specialize the initial Hilbert lattice with additional conditions found by Maria Solèr in 1995 and refined by René Mayet in 1998 that result in a division ring isomorphic to ℂ. See additional discussion at https://us.metamath.org/qlegif/mmql.html#what 41745. 𝑊 corresponds to the w in the proof of Theorem 13.4 of [Crawley] p. 111. Such a 𝑊 always exists since HL has lattice rank of at least 4 by df-hil 21814. It can be eliminated if we just want to show the existence of a Hilbert space, as is done in the literature. (Contributed by NM, 23-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑈 ∈ Hil)
21.29  Mathbox for metakunt
21.29.1  Commutative Semiring
Syntax	ccsrg 42598	Extend class notation with the class of all commutative semirings.
class CSRing
Definition	df-csring 42599	Define the class of all commutative semirings. (Contributed by metakunt, 4-Apr-2025.)
⊢ CSRing = {𝑓 ∈ SRing ∣ (mulGrp‘𝑓) ∈ CMnd}
Theorem	iscsrg 42600	A commutative semiring is a semiring whose multiplication is a commutative monoid. (Contributed by metakunt, 4-Apr-2025.)
⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ CSRing ↔ (𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd))