P. 348 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34701-34800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lkrssv 34701	The kernel of a linear functional is a set of vectors. (Contributed by NM, 1-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐾‘𝐺) ⊆ 𝑉)
Theorem	lkrsc 34702	The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 9-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐾)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑅 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐿‘(𝐺 ∘𝑓 · (𝑉 × {𝑅}))) = (𝐿‘𝐺))
Theorem	lkrscss 34703	The kernel of a scalar product of a functional includes the kernel of the functional. (The inclusion is proper for the zero product and equality otherwise.) (Contributed by NM, 9-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) ⊆ (𝐿‘(𝐺 ∘𝑓 · (𝑉 × {𝑅}))))
Theorem	eqlkr 34704*	Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 18-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
Theorem	eqlkr2 34705*	Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 10-Oct-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 𝐻 = (𝐺 ∘𝑓 · (𝑉 × {𝑟})))
Theorem	eqlkr3 34706	Two functionals with the same kernel are equal if they are equal at any nonzero value. (Contributed by NM, 2-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐾‘𝐺) = (𝐾‘𝐻))    &   ⊢ (𝜑 → (𝐺‘𝑋) = (𝐻‘𝑋))    &   ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 )    ⇒   ⊢ (𝜑 → 𝐺 = 𝐻)
Theorem	lkrlsp 34707	The subspace sum of a kernel and the span of a vector not in the kernel (by ellkr 34694) is the whole vector space. (Contributed by NM, 19-Apr-2014.)
⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹) ∧ (𝐺‘𝑋) ≠ 0 ) → ((𝐾‘𝐺) ⊕ (𝑁‘{𝑋})) = 𝑉)
Theorem	lkrlsp2 34708	The subspace sum of a kernel and the span of a vector not in the kernel is the whole vector space. (Contributed by NM, 12-May-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹) ∧ ¬ 𝑋 ∈ (𝐾‘𝐺)) → ((𝐾‘𝐺) ⊕ (𝑁‘{𝑋})) = 𝑉)
Theorem	lkrlsp3 34709	The subspace sum of a kernel and the span of a vector not in the kernel is the whole vector space. (Contributed by NM, 29-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹) ∧ ¬ 𝑋 ∈ (𝐾‘𝐺)) → (𝑁‘((𝐾‘𝐺) ∪ {𝑋})) = 𝑉)
Theorem	lkrshp 34710	The kernel of a nonzero functional is a hyperplane. (Contributed by NM, 29-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × { 0 })) → (𝐾‘𝐺) ∈ 𝐻)
Theorem	lkrshp3 34711	The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ (𝑉 × { 0 })))
Theorem	lkrshpor 34712	The kernel of a functional is either a hyperplane or the full vector space. (Contributed by NM, 7-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ∨ (𝐾‘𝐺) = 𝑉))
Theorem	lkrshp4 34713	A kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ≠ 𝑉 ↔ (𝐾‘𝐺) ∈ 𝐻))
Theorem	lshpsmreu 34714*	Lemma for lshpkrex 34723. Show uniqueness of ring multiplier 𝑘 when a vector 𝑋 is broken down into components, one in a hyperplane and the other outside of it . TODO: do we need the cbvrexv 3202 for 𝑎 to 𝑐? (Contributed by NM, 4-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ (𝜑 → ∃!𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑋 = (𝑦 + (𝑘 · 𝑍)))
Theorem	lshpkrlem1 34715*	Lemma for lshpkrex 34723. The value of tentative functional 𝐺 is zero iff its argument belongs to hyperplane 𝑈. (Contributed by NM, 14-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ (𝐺‘𝑋) = 0 ))
Theorem	lshpkrlem2 34716*	Lemma for lshpkrex 34723. The value of tentative functional 𝐺 is a scalar. (Contributed by NM, 16-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐾)
Theorem	lshpkrlem3 34717*	Lemma for lshpkrex 34723. Defining property of 𝐺‘𝑋. (Contributed by NM, 15-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑈 𝑋 = (𝑧 + ((𝐺‘𝑋) · 𝑍)))
Theorem	lshpkrlem4 34718*	Lemma for lshpkrex 34723. Part of showing linearity of 𝐺. (Contributed by NM, 16-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑉 ∧ 𝑠 ∈ 𝑉) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)))) → ((𝑙 · 𝑢) + 𝑣) = (((𝑙 · 𝑟) + 𝑠) + (((𝑙(.r‘𝐷)(𝐺‘𝑢))(+g‘𝐷)(𝐺‘𝑣)) · 𝑍)))
Theorem	lshpkrlem5 34719*	Lemma for lshpkrex 34723. Part of showing linearity of 𝐺. (Contributed by NM, 16-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(.r‘𝐷)(𝐺‘𝑢))(+g‘𝐷)(𝐺‘𝑣)))
Theorem	lshpkrlem6 34720*	Lemma for lshpkrex 34723. Show linearlity of 𝐺. (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    ⇒   ⊢ ((𝜑 ∧ (𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉)) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(.r‘𝐷)(𝐺‘𝑢))(+g‘𝐷)(𝐺‘𝑣)))
Theorem	lshpkrcl 34721*	The set 𝐺 defined by hyperplane 𝑈 is a linear functional. (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    &   ⊢ 𝐹 = (LFnl‘𝑊)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝐹)
Theorem	lshpkr 34722*	The kernel of functional 𝐺 is the hyperplane defining it. (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))    &   ⊢ 𝐿 = (LKer‘𝑊)    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) = 𝑈)
Theorem	lshpkrex 34723*	There exists a functional whose kernel equals a given hyperplane. Part of Th. 1.27 of Barbu and Precupanu, Convexity and Optimization in Banach Spaces. (Contributed by NM, 17-Jul-2014.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻) → ∃𝑔 ∈ 𝐹 (𝐾‘𝑔) = 𝑈)
Theorem	lshpset2N 34724*	The set of all hyperplanes of a left module or left vector space equals the set of all kernels of nonzero functionals. (Contributed by NM, 17-Jul-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → 𝐻 = {𝑠 ∣ ∃𝑔 ∈ 𝐹 (𝑔 ≠ (𝑉 × { 0 }) ∧ 𝑠 = (𝐾‘𝑔))})
Theorem	islshpkrN 34725*	The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be 𝑈 = (𝐾‘𝑔) or (𝐾‘𝑔) = 𝑈 as in lshpkrex 34723? Both standards seem to be used randomly throughout set.mm; we should decide on a preferred one. (Contributed by NM, 7-Oct-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → (𝑈 ∈ 𝐻 ↔ ∃𝑔 ∈ 𝐹 (𝑔 ≠ (𝑉 × { 0 }) ∧ 𝑈 = (𝐾‘𝑔))))
Theorem	lfl1dim 34726*	Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)} = {𝑔 ∣ ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘}))})
Theorem	lfl1dim2N 34727*	Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim 34726 may be more compatible with lspsn 19050. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐷 = (Scalar‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐷)    &   ⊢ · = (.r‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)} = {𝑔 ∈ 𝐹 ∣ ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘}))})
20.23.8  Opposite rings and dual vector spaces
Syntax	cld 34728	Extend class notation with left dualvector space.
class LDual
Definition	df-ldual 34729*	Define the (left) dual of a left vector space (or module) in which the vectors are functionals. In many texts, this is defined as a right vector space, but by reversing the multiplication we achieve a left vector space, as is done in definition of dual vector space in [Holland95] p. 218. This allows us to reuse our existing collection of left vector space theorems. The restriction on ∘𝑓 (+g‘𝑣) allows it to be a set; see ofmres 7206. Note the operation reversal in the scalar product to allow us to use the original scalar ring instead of the oppr ring, for convenience. (Contributed by NM, 18-Oct-2014.)
⊢ LDual = (𝑣 ∈ V ↦ ({⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓 ∘𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}))
Theorem	ldualset 34730*	Define the (left) dual of a left vector space (or module) in which the vectors are functionals. In many texts, this is defined as a right vector space, but by reversing the multiplication we achieve a left vector space, as is done in definition of dual vector space in [Holland95] p. 218. This allows us to reuse our existing collection of left vector space theorems. Note the operation reversal in the scalar product to allow us to use the original scalar ring instead of the oppr ring, for convenience. (Contributed by NM, 18-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = ( ∘𝑓 + ↾ (𝐹 × 𝐹))    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∙ = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘𝑓 · (𝑉 × {𝑘})))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}))
Theorem	ldualvbase 34731	The vectors of a dual space are functionals of the original space. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑉 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑉 = 𝐹)
Theorem	ldualelvbase 34732	Utility theorem for converting a functional to a vector of the dual space in order to use standard vector theorems. (Contributed by NM, 6-Jan-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑉 = (Base‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝑉)
Theorem	ldualfvadd 34733	Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ ✚ = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ ⨣ = ( ∘𝑓 + ↾ (𝐹 × 𝐹))    ⇒   ⊢ (𝜑 → ✚ = ⨣ )
Theorem	ldualvadd 34734	Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ ✚ = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 ✚ 𝐻) = (𝐺 ∘𝑓 + 𝐻))
Theorem	ldualvaddcl 34735	The value of vector addition in the dual of a vector space is a functional. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 + 𝐻) ∈ 𝐹)
Theorem	ldualvaddval 34736	The value of the value of vector addition in the dual of a vector space. (Contributed by NM, 7-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ ✚ = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐺 ✚ 𝐻)‘𝑋) = ((𝐺‘𝑋) + (𝐻‘𝑋)))
Theorem	ldualsca 34737	The ring of scalars of the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝑂 = (oppr‘𝐹)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑅 = 𝑂)
Theorem	ldualsbase 34738	Base set of scalar ring for the dual of a vector space. (Contributed by NM, 24-Oct-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐿 = (Base‘𝐹)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝐷)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐾 = 𝐿)
Theorem	ldualsaddN 34739	Scalar addition for the dual of a vector space. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝐹)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝐷)    &   ⊢ ✚ = (+g‘𝑅)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ✚ = + )
Theorem	ldualsmul 34740	Scalar multiplication for the dual of a vector space. (Contributed by NM, 19-Oct-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = (.r‘𝐹)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝐷)    &   ⊢ ∙ = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝑋 ∙ 𝑌) = (𝑌 · 𝑋))
Theorem	ldualfvs 34741*	Scalar product operation for the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑌)    &   ⊢ · = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘𝑓 × (𝑉 × {𝑘})))    ⇒   ⊢ (𝜑 → ∙ = · )
Theorem	ldualvs 34742	Scalar product operation value (which is a functional) for the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑋 ∙ 𝐺) = (𝐺 ∘𝑓 × (𝑉 × {𝑋})))
Theorem	ldualvsval 34743	Value of scalar product operation value for the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑋 ∙ 𝐺)‘𝐴) = ((𝐺‘𝐴) × 𝑋))
Theorem	ldualvscl 34744	The scalar product operation value is a functional. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐹)
Theorem	ldualvaddcom 34745	Commutative law for vector (functional) addition. (Contributed by NM, 17-Jan-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	ldualvsass 34746	Associative law for scalar product operation. (Contributed by NM, 20-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝑌 × 𝑋) · 𝐺) = (𝑋 · (𝑌 · 𝐺)))
Theorem	ldualvsass2 34747	Associative law for scalar product operation, using operations from the dual space. (Contributed by NM, 20-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑄 = (Scalar‘𝐷)    &   ⊢ × = (.r‘𝑄)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝑋 × 𝑌) · 𝐺) = (𝑋 · (𝑌 · 𝐺)))
Theorem	ldualvsdi1 34748	Distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑋 · (𝐺 + 𝐻)) = ((𝑋 · 𝐺) + (𝑋 · 𝐻)))
Theorem	ldualvsdi2 34749	Reverse distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ ✚ = (+g‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) · 𝐺) = ((𝑋 · 𝐺) ✚ (𝑌 · 𝐺)))
Theorem	ldualgrplem 34750	Lemma for ldualgrp 34751. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = ∘𝑓 (+g‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ Grp)
Theorem	ldualgrp 34751	The dual of a vector space is a group. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝐷 ∈ Grp)
Theorem	ldual0 34752	The zero scalar of the dual of a vector space. (Contributed by NM, 28-Dec-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐷)    &   ⊢ 𝑂 = (0g‘𝑆)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑂 = 0 )
Theorem	ldual1 34753	The unit scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐷)    &   ⊢ 𝐼 = (1r‘𝑆)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝐼 = 1 )
Theorem	ldualneg 34754	The negative of a scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝑀 = (invg‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝐷)    &   ⊢ 𝑁 = (invg‘𝑆)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑁 = 𝑀)
Theorem	ldual0v 34755	The zero vector of the dual of a vector space. (Contributed by NM, 24-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑂 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑂 = (𝑉 × { 0 }))
Theorem	ldual0vcl 34756	The dual zero vector is a functional. (Contributed by NM, 5-Mar-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 0 ∈ 𝐹)
Theorem	lduallmodlem 34757	Lemma for lduallmod 34758. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = ∘𝑓 (+g‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ LMod)
Theorem	lduallmod 34758	The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝐷 ∈ LMod)
Theorem	lduallvec 34759	The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr 18669; otherwise, the dual would be a right vector space as is sometimes the case in the literature. (Contributed by NM, 22-Oct-2014.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    ⇒   ⊢ (𝜑 → 𝐷 ∈ LVec)
Theorem	ldualvsub 34760	The value of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 − 𝐻) = (𝐺 + ((𝑁‘ 1 ) · 𝐻)))
Theorem	ldualvsubcl 34761	Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺 − 𝐻) ∈ 𝐹)
Theorem	ldualvsubval 34762	The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 34760? (Requires 𝐷 to oppr conversion.) (Contributed by NM, 26-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝑆 = (-g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ − = (-g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐺 − 𝐻)‘𝑋) = ((𝐺‘𝑋)𝑆(𝐻‘𝑋)))
Theorem	ldualssvscl 34763	Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ 𝑆 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑈)
Theorem	ldualssvsubcl 34764	Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015.)
⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ − = (-g‘𝐷)    &   ⊢ 𝑆 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑈)
Theorem	ldual0vs 34765	Scalar zero times a functional is the zero functional. (Contributed by NM, 17-Feb-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ 𝑂 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ( 0 · 𝐺) = 𝑂)
Theorem	lkr0f2 34766	The kernel of the zero functional is the set of all vectors. (Contributed by NM, 4-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) = 𝑉 ↔ 𝐺 = 0 ))
Theorem	lduallkr3 34767	The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ 0 ))
Theorem	lkrpssN 34768	Proper subset relation between kernels. (Contributed by NM, 16-Feb-2015.) (New usage is discouraged.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ⊊ (𝐾‘𝐻) ↔ (𝐺 ≠ 0 ∧ 𝐻 = 0 )))
Theorem	lkrin 34769	Intersection of the kernels of 2 functionals is included in the kernel of their sum. (Contributed by NM, 7-Jan-2015.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ + = (+g‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ∩ (𝐾‘𝐻)) ⊆ (𝐾‘(𝐺 + 𝐻)))
Theorem	eqlkr4 34770*	Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 4-Feb-2015.)
⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐾‘𝐺) = (𝐾‘𝐻))    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ 𝑅 𝐻 = (𝑟 · 𝐺))
Theorem	ldual1dim 34771*	Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑁‘{𝐺}) = {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)})
Theorem	ldualkrsc 34772	The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 28-Dec-2014.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐿‘(𝑋 · 𝐺)) = (𝐿‘𝐺))
Theorem	lkrss 34773	The kernel of a scalar product of a functional includes the kernel of the functional. (Contributed by NM, 27-Jan-2015.)
⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) ⊆ (𝐿‘(𝑋 · 𝐺)))
Theorem	lkrss2N 34774*	Two functionals with kernels in a subset relationship. (Contributed by NM, 17-Feb-2015.) (New usage is discouraged.)
⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐺) ⊆ (𝐾‘𝐻) ↔ ∃𝑟 ∈ 𝑅 𝐻 = (𝑟 · 𝐺)))
Theorem	lkreqN 34775	Proportional functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐾 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑅 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 = (𝐴 · 𝐻))    ⇒   ⊢ (𝜑 → (𝐾‘𝐺) = (𝐾‘𝐻))
Theorem	lkrlspeqN 34776	Condition for colinear functionals to have equal kernels. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
⊢ 𝐹 = (LFnl‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑊)    &   ⊢ 0 = (0g‘𝐷)    &   ⊢ 𝑁 = (LSpan‘𝐷)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ ((𝑁‘{𝐻}) ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) = (𝐿‘𝐻))
20.23.9  Ortholattices and orthomodular lattices
Syntax	cops 34777	Extend class notation with orthoposets.
class OP
Syntax	ccmtN 34778	Extend class notation with the commutes relation.
class cm
Syntax	col 34779	Extend class notation with orthlattices.
class OL
Syntax	coml 34780	Extend class notation with orthomodular lattices.
class OML
Definition	df-oposet 34781*	Define the class of orthoposets, which are bounded posets with an orthocomplementation operation. Note that (Base p ) e. dom ( lub 𝑝) means there is an upper bound 1., and similarly for the 0. element. (Contributed by NM, 20-Oct-2011.) (Revised by NM, 13-Sep-2018.)
⊢ OP = {𝑝 ∈ Poset ∣ (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜‘𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜‘𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎))) ∧ (𝑎(join‘𝑝)(𝑜‘𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜‘𝑎)) = (0.‘𝑝))))}
Definition	df-cmtN 34782*	Define the commutes relation for orthoposets. Definition of commutes in [Kalmbach] p. 20. (Contributed by NM, 6-Nov-2011.)
⊢ cm = (𝑝 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))})
Definition	df-ol 34783	Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.)
⊢ OL = (Lat ∩ OP)
Definition	df-oml 34784*	Define the class of orthomodular lattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.)
⊢ OML = {𝑙 ∈ OL ∣ ∀𝑎 ∈ (Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))}
Theorem	isopos 34785*	The predicate "is an orthoposet." (Contributed by NM, 20-Oct-2011.) (Revised by NM, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 )))
Theorem	opposet 34786	Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.)
⊢ (𝐾 ∈ OP → 𝐾 ∈ Poset)
Theorem	oposlem 34787	Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))
Theorem	op01dm 34788	Conditions necessary for zero and unit elements to exist. (Contributed by NM, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺))
Theorem	op0cl 34789	An orthoposet has a zero element. (h0elch 28240 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → 0 ∈ 𝐵)
Theorem	op1cl 34790	An orthoposet has a unit element. (helch 28228 analog.) (Contributed by NM, 22-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → 1 ∈ 𝐵)
Theorem	op0le 34791	Orthoposet zero is less than or equal to any element. (ch0le 28428 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 0 ≤ 𝑋)
Theorem	ople0 34792	An element less than or equal to zero equals zero. (chle0 28430 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ≤ 0 ↔ 𝑋 = 0 ))
Theorem	opnlen0 34793	An element not less than another is nonzero. TODO: Look for uses of necon3bd 2837 and op0le 34791 to see if this is useful elsewhere. (Contributed by NM, 5-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋 ≤ 𝑌) → 𝑋 ≠ 0 )
Theorem	lub0N 34794	The least upper bound of the empty set is the zero element. (Contributed by NM, 15-Sep-2013.) (New usage is discouraged.)
⊢ 1 = (lub‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → ( 1 ‘∅) = 0 )
Theorem	opltn0 34795	A lattice element greater than zero is nonzero. TODO: is this needed? (Contributed by NM, 1-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ 𝑋 ≠ 0 ))
Theorem	ople1 34796	Any element is less than the orthoposet unit. (chss 28214 analog.) (Contributed by NM, 23-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 1 )
Theorem	op1le 34797	If the orthoposet unit is less than or equal to an element, the element equals the unit. (chle0 28430 analog.) (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( 1 ≤ 𝑋 ↔ 𝑋 = 1 ))
Theorem	glb0N 34798	The greatest lower bound of the empty set is the unit element. (Contributed by NM, 5-Dec-2011.) (New usage is discouraged.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → (𝐺‘∅) = 1 )
Theorem	opoccl 34799	Closure of orthocomplement operation. (choccl 28293 analog.) (Contributed by NM, 20-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)
Theorem	opococ 34800	Double negative law for orthoposets. (ococ 28393 analog.) (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)