P. 428 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42701-42800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hgmaprnlem4N 42701*	Lemma for hgmaprnN 42703. 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 42702	Lemma for hgmaprnN 42703. 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 42703	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 42704	The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐺‘𝑋) = (𝐺‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	hgmapf1oN 42705	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 42706	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 42707	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 42708	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 42709	Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 + 𝑌)) = (((𝑆‘𝑍)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑌)))
Theorem	hdmaplns1 42710	Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝑁 = (-g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 − 𝑌)) = (((𝑆‘𝑍)‘𝑋)𝑁((𝑆‘𝑍)‘𝑌)))
Theorem	hdmaplnm1 42711	Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑌)‘(𝐴 · 𝑋)) = (𝐴 × ((𝑆‘𝑌)‘𝑋)))
Theorem	hdmaplna2 42712	Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ ⨣ = (+g‘𝑅)    &   ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑆‘(𝑌 + 𝑍))‘𝑋) = (((𝑆‘𝑌)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑋)))
Theorem	hdmapglnm2 42713	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 42714	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 42715	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 42716	Membership in the kernel (as shown by hdmaplkr 42715) 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 42717	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 42718	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 42719	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 42720	Line 27 in [Baer] p. 110. We use 𝐶 for Baer's u. Our unit vector 𝐸 has the required properties for his w by hdmapevec2 42638. 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 42721	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 42722	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 42723	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 42638. 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 42724	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 42725	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 42726	Lemma for hgmapvv 42728. 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 42727	Lemma for hgmapvv 42728. 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 42728	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 42729*	Lemma for hdmapg 42732. (Contributed by NM, 14-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝑈)    &   ⊢ 𝑅 = (Scalar‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ⊕ = (LSSum‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ (𝑂‘{𝐸})∃𝑘 ∈ 𝐵 𝑋 = ((𝑘 · 𝐸) + 𝑢))
Theorem	hdmapglem7b 42730	Lemma for hdmapg 42732. (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 42731	Lemma for hdmapg 42732. 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 42732	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 42733*	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 42734	Extend class notation with the final constructed Hilbert space.
class HLHil
Definition	df-hlhil 42735*	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 42736*	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 42737	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 42738	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 42739	The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝐿)    ⇒   ⊢ (𝜑 → + = (+g‘𝑈))
Theorem	hlhilslem 42740	Lemma for hlhilsbase 42741 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 42741	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 42742	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 42743	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 42744	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 42745	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 42746	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 42747	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 42748	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 42749	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 42750*	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 42751	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 42752	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 42753	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 42754	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 42755	Lemma for hlhilsrng 42756. (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 42756	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 42757	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 42758	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 42759	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 42760	The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 42738 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 42761*	Lemma for hlhil 25613. (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 42762*	Lemma for hlhil 25613. (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 42763	Construction of a Hilbert space (df-hil 21865) 𝑈 from a Hilbert lattice (df-hlat 40153) 𝐾, where 𝑊 is a fixed but arbitrary hyperplane (co-atom) in 𝐾. The Hilbert space 𝑈 is identical to the vector space ((DVecH‘𝐾)‘𝑊) (see dvhlvec 41911) 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 41911. 𝑊 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 21865. 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 42764	Extend class notation with the class of all commutative semirings.
class CSRing
Definition	df-csring 42765	Define the class of all commutative semirings. (Contributed by metakunt, 4-Apr-2025.)
⊢ CSRing = {𝑓 ∈ SRing ∣ (mulGrp‘𝑓) ∈ CMnd}
Theorem	iscsrg 42766	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 42767	Evaluation of integers across a ring homomorphism. (Contributed by metakunt, 4-Jun-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ ℤ)    &   ⊢ 𝑀 = (ℤRHom‘𝑅)    &   ⊢ 𝑁 = (ℤRHom‘𝑆)    ⇒   ⊢ (𝜑 → (𝐹‘(𝑀‘𝑋)) = (𝑁‘𝑋))
Theorem	zndvdchrrhm 42768*	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 42769	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 42770	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 42771	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 42772	The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.)
⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 2 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝑌)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌))
Theorem	uzindd 42773*	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 42774	Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑂 ∈ ℤ)    &   ⊢ (𝜑 → 𝑃 ∈ ℤ)    &   ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑂...𝑃))    &   ⊢ (𝜑 → 𝑄 = (𝑀 + 𝑂))    &   ⊢ (𝜑 → 𝑅 = (𝑁 + 𝑃))    ⇒   ⊢ (𝜑 → (𝐽 + 𝐾) ∈ (𝑄...𝑅))
Theorem	fzne2d 42775	Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))    &   ⊢ (𝜑 → 𝐾 ≠ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 < 𝑁)
Theorem	eqfnfv2d2 42776*	Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	fzsplitnd 42777	Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁)))
Theorem	fzsplitnr 42778	Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁)))
Theorem	addassnni 42779	Associative law for addition. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐶 ∈ ℕ    ⇒   ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Theorem	addcomnni 42780	Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴)
Theorem	mulassnni 42781	Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐶 ∈ ℕ    ⇒   ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Theorem	mulcomnni 42782	Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)
Theorem	gcdcomnni 42783	Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)
Theorem	gcdnegnni 42784	Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁)
Theorem	neggcdnni 42785	Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁)
Theorem	bccl2d 42786	Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ)
Theorem	recbothd 42787	Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐵 / 𝐴) = (𝐷 / 𝐶)))
Theorem	gcdmultiplei 42788	The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd (𝑀 · 𝑁)) = 𝑀
Theorem	gcdaddmzz2nni 42789	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 42790	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 42791	Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑀 gcd 𝑁) ∈ ℕ
Theorem	muldvds1d 42792	If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∥ 𝑁)
Theorem	muldvds2d 42793	If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝑀 ∥ 𝑁)
Theorem	nndivdvdsd 42794	A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds 16325. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℕ))
Theorem	nnproddivdvdsd 42795	A product of natural numbers divides a natural number if and only if a factor divides the quotient, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐾 · 𝑀) ∥ 𝑁 ↔ 𝐾 ∥ (𝑁 / 𝑀)))
Theorem	coprmdvds2d 42796	If an integer is divisible by two coprime integers, then it is divisible by their product, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → (𝐾 gcd 𝑀) = 1)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑁)    &   ⊢ (𝜑 → 𝑀 ∥ 𝑁)    ⇒   ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁)
Theorem	imadomfi 42797	An image of a function under a finite set is dominated by the set. (Contributed by SN, 10-May-2025.)
⊢ ((𝐴 ∈ Fin ∧ Fun 𝐹) → (𝐹 “ 𝐴) ≼ 𝐴)
21.29.3  Some gcd and lcm results
Theorem	12gcd5e1 42798	The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;12 gcd 5) = 1
Theorem	60gcd6e6 42799	The gcd of 60 and 6 is 6. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;60 gcd 6) = 6
Theorem	60gcd7e1 42800	The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024.)
⊢ (;60 gcd 7) = 1