P. 420 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41901-42000   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	chg 41901	Extend class notation with g-map.
class HGMap
Definition	df-hgmap 41902*	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 41903*	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 41904*	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 41905*	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 41900. (Contributed by NM, 25-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑀 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ 𝐼 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) = (℩𝑦 ∈ 𝐵 ∀𝑣 ∈ 𝑉 (𝑀‘(𝑋 · 𝑣)) = (𝑦 ∙ (𝑀‘𝑣))))
Theorem	hgmapfnN 41906	Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐺 Fn 𝐵)
Theorem	hgmapcl 41907	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 41908	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 41909	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 41910	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 41911	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 41912	Part 15 of [Baer] p. 50 line 13. (Contributed by NM, 6-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘(𝑋 + 𝑌)) = ((𝐺‘𝑋) + (𝐺‘𝑌)))
Theorem	hgmapmul 41913	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 41914	Lemma for hgmaprnN 41919. (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 41915	Lemma for hgmaprnN 41919. 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 41916*	Lemma for hgmaprnN 41919. 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 41917*	Lemma for hgmaprnN 41919. 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 41918	Lemma for hgmaprnN 41919. 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 41919	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 41920	The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐺‘𝑋) = (𝐺‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	hgmapf1oN 41921	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 41922	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 41923	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 41924	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 41925	Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 + 𝑌)) = (((𝑆‘𝑍)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑌)))
Theorem	hdmaplns1 41926	Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝑁 = (-g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 − 𝑌)) = (((𝑆‘𝑍)‘𝑋)𝑁((𝑆‘𝑍)‘𝑌)))
Theorem	hdmaplnm1 41927	Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑌)‘(𝐴 · 𝑋)) = (𝐴 × ((𝑆‘𝑌)‘𝑋)))
Theorem	hdmaplna2 41928	Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘(𝑌 + 𝑍))‘𝑋) = (((𝑆‘𝑌)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑋)))
Theorem	hdmapglnm2 41929	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 41930	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 41931	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 41932	Membership in the kernel (as shown by hdmaplkr 41931) 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 41933	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 41934	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 41935	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 41936	Line 27 in [Baer] p. 110. We use 𝐶 for Baer's u. Our unit vector 𝐸 has the required properties for his w by hdmapevec2 41854. 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 41937	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 41938	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 41939	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 41854. 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 41940	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 41941	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 41942	Lemma for hgmapvv 41944. 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 41943	Lemma for hgmapvv 41944. 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 41944	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 41945*	Lemma for hdmapg 41948. (Contributed by NM, 14-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ (𝑂‘{𝐸})∃𝑘 ∈ 𝐵 𝑋 = ((𝑘 · 𝐸) + 𝑢))
Theorem	hdmapglem7b 41946	Lemma for hdmapg 41948. (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 41947	Lemma for hdmapg 41948. 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 41948	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 41949*	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 41950	Extend class notation with the final constructed Hilbert space.
class HLHil
Definition	df-hlhil 41951*	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 41952*	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 41953	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 41954	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 41955	The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝐿)    ⇒   ⊢ (𝜑 → + = (+g‘𝑈))
Theorem	hlhilslem 41956	Lemma for hlhilsbase 41957 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 41957	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 41958	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 41959	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 41960	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 41961	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 41962	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 41963	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 41964	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 41965	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 41966*	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 41967	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 41968	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 41969	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 41970	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 41971	Lemma for hlhilsrng 41972. (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 41972	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 41973	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 41974	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 41975	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 41976	The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 41954 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 41977*	Lemma for hlhil 25363. (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 41978*	Lemma for hlhil 25363. (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 41979	Construction of a Hilbert space (df-hil 21634) 𝑈 from a Hilbert lattice (df-hlat 39369) 𝐾, where 𝑊 is a fixed but arbitrary hyperplane (co-atom) in 𝐾. The Hilbert space 𝑈 is identical to the vector space ((DVecH‘𝐾)‘𝑊) (see dvhlvec 41127) 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 41127. 𝑊 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 21634. 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 41980	Extend class notation with the class of all commutative semirings.
class CSRing
Definition	df-csring 41981	Define the class of all commutative semirings. (Contributed by metakunt, 4-Apr-2025.)
⊢ CSRing = {𝑓 ∈ SRing ∣ (mulGrp‘𝑓) ∈ CMnd}
Theorem	iscsrg 41982	A commutative semiring is a semiring whose multiplication is a commutative monoid. (Contributed by metakunt, 4-Apr-2025.)
⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ CSRing ↔ (𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd))
21.29.2  General helpful statements
Theorem	rhmzrhval 41983	Evaluation of integers across a ring homomorphism. (Contributed by metakunt, 4-Jun-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ ℤ)    &   ⊢ 𝑀 = (ℤRHom‘𝑅)    &   ⊢ 𝑁 = (ℤRHom‘𝑆)    ⇒   ⊢ (𝜑 → (𝐹‘(𝑀‘𝑋)) = (𝑁‘𝑋))
Theorem	zndvdchrrhm 41984*	Construction of a ring homomorphism from ℤ/nℤ to 𝑅 when the characteristic of 𝑅 divides 𝑁. (Contributed by metakunt, 4-Jun-2025.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (chr‘𝑅) ∈ ℤ)    &   ⊢ (𝜑 → (chr‘𝑅) ∥ 𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = (𝑥 ∈ (Base‘𝑍) ↦ ∪ ((ℤRHom‘𝑅) “ 𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑍 RingHom 𝑅))
Theorem	relogbcld 41985	Closure of the general logarithm with a positive real base on positive reals, a deduction version. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝑋)    &   ⊢ (𝜑 → 𝐵 ≠ 1)    ⇒   ⊢ (𝜑 → (𝐵 logb 𝑋) ∈ ℝ)
Theorem	relogbexpd 41986	Identity law for general logarithm: the logarithm of a power to the base is the exponent, a deduction version. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ≠ 1)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐵 logb (𝐵↑𝑀)) = 𝑀)
Theorem	relogbzexpd 41987	Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power, a deduction version. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ≠ 1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐵 logb (𝐶↑𝑁)) = (𝑁 · (𝐵 logb 𝐶)))
Theorem	logblebd 41988	The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 2 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝑌)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌))
Theorem	uzindd 41989*	Induction on the upper integers that start at 𝑀. The first four hypotheses give us the substitution instances we need; the following two are the basis and the induction step, a deduction version. (Contributed by metakunt, 8-Jun-2024.)
⊢ (𝑗 = 𝑀 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑗 = 𝑘 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑗 = (𝑘 + 1) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑗 = 𝑁 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃 ∧ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘)) → 𝜏)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	fzadd2d 41990	Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑂 ∈ ℤ)    &   ⊢ (𝜑 → 𝑃 ∈ ℤ)    &   ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑂...𝑃))    &   ⊢ (𝜑 → 𝑄 = (𝑀 + 𝑂))    &   ⊢ (𝜑 → 𝑅 = (𝑁 + 𝑃))    ⇒   ⊢ (𝜑 → (𝐽 + 𝐾) ∈ (𝑄...𝑅))
Theorem	zltp1led 41991	Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
Theorem	fzne2d 41992	Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))    &   ⊢ (𝜑 → 𝐾 ≠ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 < 𝑁)
Theorem	eqfnfv2d2 41993*	Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	fzsplitnd 41994	Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁)))
Theorem	fzsplitnr 41995	Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁)))
Theorem	addassnni 41996	Associative law for addition. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐶 ∈ ℕ    ⇒   ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Theorem	addcomnni 41997	Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴)
Theorem	mulassnni 41998	Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐶 ∈ ℕ    ⇒   ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Theorem	mulcomnni 41999	Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)
Theorem	gcdcomnni 42000	Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)