P. 415 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41401-41500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hgmaprnlem1N 41401	Lemma for hgmaprnN 41406. (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 41402	Lemma for hgmaprnN 41406. 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 41403*	Lemma for hgmaprnN 41406. 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 41404*	Lemma for hgmaprnN 41406. 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 41405	Lemma for hgmaprnN 41406. 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 41406	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 41407	The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐺‘𝑋) = (𝐺‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	hgmapf1oN 41408	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 41409	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 41410	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 41411	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 41412	Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 + 𝑌)) = (((𝑆‘𝑍)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑌)))
Theorem	hdmaplns1 41413	Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝑁 = (-g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 − 𝑌)) = (((𝑆‘𝑍)‘𝑋)𝑁((𝑆‘𝑍)‘𝑌)))
Theorem	hdmaplnm1 41414	Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑌)‘(𝐴 · 𝑋)) = (𝐴 × ((𝑆‘𝑌)‘𝑋)))
Theorem	hdmaplna2 41415	Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘(𝑌 + 𝑍))‘𝑋) = (((𝑆‘𝑌)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑋)))
Theorem	hdmapglnm2 41416	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 41417	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 41418	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 41419	Membership in the kernel (as shown by hdmaplkr 41418) 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 41420	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 41421	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 41422	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 41423	Line 27 in [Baer] p. 110. We use 𝐶 for Baer's u. Our unit vector 𝐸 has the required properties for his w by hdmapevec2 41341. 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 41424	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 41425	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 41426	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 41341. 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 41427	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 41428	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 41429	Lemma for hgmapvv 41431. 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 41430	Lemma for hgmapvv 41431. 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 41431	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 41432*	Lemma for hdmapg 41435. (Contributed by NM, 14-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ (𝑂‘{𝐸})∃𝑘 ∈ 𝐵 𝑋 = ((𝑘 · 𝐸) + 𝑢))
Theorem	hdmapglem7b 41433	Lemma for hdmapg 41435. (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 41434	Lemma for hdmapg 41435. 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 41435	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 41436*	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 41437	Extend class notation with the final constructed Hilbert space.
class HLHil
Definition	df-hlhil 41438*	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 41439*	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 41440	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 41441	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 41442	The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝐿)    ⇒   ⊢ (𝜑 → + = (+g‘𝑈))
Theorem	hlhilslem 41443	Lemma for hlhilsbase 41445 etc. (Contributed by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐹 = Slot (𝐹‘ndx)    &   ⊢ (𝐹‘ndx) ≠ (*𝑟‘ndx)    &   ⊢ 𝐶 = (𝐹‘𝐸)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐹‘𝑅))
Theorem	hlhilslemOLD 41444	Obsolete version of hlhilslem 41443 as of 6-Nov-2024. Lemma for hlhilsbase 41445. (Contributed by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐹 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑁 < 4    &   ⊢ 𝐶 = (𝐹‘𝐸)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐹‘𝑅))
Theorem	hlhilsbase 41445	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	hlhilsbaseOLD 41446	Obsolete version of hlhilsbase 41445 as of 6-Nov-2024. The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐶 = (Base‘𝐸)    ⇒   ⊢ (𝜑 → 𝐶 = (Base‘𝑅))
Theorem	hlhilsplus 41447	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	hlhilsplusOLD 41448	Obsolete version of hlhilsplus 41447 as of 6-Nov-2024. The scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ + = (+g‘𝐸)    ⇒   ⊢ (𝜑 → + = (+g‘𝑅))
Theorem	hlhilsmul 41449	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	hlhilsmulOLD 41450	Obsolete version of hlhilsmul 41449 as of 6-Nov-2024. The scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ · = (.r‘𝐸)    ⇒   ⊢ (𝜑 → · = (.r‘𝑅))
Theorem	hlhilsbase2 41451	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 41452	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 41453	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 41454	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 41455	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 41456	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 41457*	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 41458	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 41459	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 41460	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 41461	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 41462	Lemma for hlhilsrng 41463. (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 41463	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 41464	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 41465	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 41466	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 41467	The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 41441 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 41468*	Lemma for hlhil 25391. (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 41469*	Lemma for hlhil 25391. (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 41470	Construction of a Hilbert space (df-hil 21645) 𝑈 from a Hilbert lattice (df-hlat 38855) 𝐾, where 𝑊 is a fixed but arbitrary hyperplane (co-atom) in 𝐾. The Hilbert space 𝑈 is identical to the vector space ((DVecH‘𝐾)‘𝑊) (see dvhlvec 40614) 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 40614. 𝑊 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 21645. 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.27  Mathbox for metakunt
21.27.1  Commutative Semiring
Syntax	ccsrg 41471	Extend class notation with the class of all commutative semirings.
class CSRing
Definition	df-csring 41472	Define the class of all commutative semirings. (Contributed by metakunt, 4-Apr-2025.)
⊢ CSRing = {𝑓 ∈ SRing ∣ (mulGrp‘𝑓) ∈ CMnd}
Theorem	iscsrg 41473	A commutative semiring is a semiring whose multiplication is a commutative monoid. (Contributed by metakunt, 4-Apr-2025.)
⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ CSRing ↔ (𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd))
21.27.2  General helpful statements
Theorem	leexp1ad 41474	Weak base ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐵↑𝑁))
Theorem	relogbcld 41475	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 41476	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 41477	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 41478	The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 2 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝑌)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌))
Theorem	uzindd 41479*	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 41480	Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑂 ∈ ℤ)    &   ⊢ (𝜑 → 𝑃 ∈ ℤ)    &   ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑂...𝑃))    &   ⊢ (𝜑 → 𝑄 = (𝑀 + 𝑂))    &   ⊢ (𝜑 → 𝑅 = (𝑁 + 𝑃))    ⇒   ⊢ (𝜑 → (𝐽 + 𝐾) ∈ (𝑄...𝑅))
Theorem	zltlem1d 41481	Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1)))
Theorem	zltp1led 41482	Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
Theorem	fzne2d 41483	Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))    &   ⊢ (𝜑 → 𝐾 ≠ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 < 𝑁)
Theorem	eqfnfv2d2 41484*	Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	fzsplitnd 41485	Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁)))
Theorem	fzsplitnr 41486	Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁)))
Theorem	addassnni 41487	Associative law for addition. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐶 ∈ ℕ    ⇒   ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Theorem	addcomnni 41488	Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴)
Theorem	mulassnni 41489	Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐶 ∈ ℕ    ⇒   ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Theorem	mulcomnni 41490	Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)
Theorem	gcdcomnni 41491	Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)
Theorem	gcdnegnni 41492	Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁)
Theorem	neggcdnni 41493	Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁)
Theorem	bccl2d 41494	Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ)
Theorem	recbothd 41495	Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐵 / 𝐴) = (𝐷 / 𝐶)))
Theorem	gcdmultiplei 41496	The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd (𝑀 · 𝑁)) = 𝑀
Theorem	gcdaddmzz2nni 41497	Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + (𝐾 · 𝑀)))
Theorem	gcdaddmzz2nncomi 41498	Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))
Theorem	gcdnncli 41499	Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd 𝑁) ∈ ℕ
Theorem	muldvds1d 41500	If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∥ 𝑁)