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	eqlkr3 34701	Two functionals with the same kernel are equal if they are equal at any nonzero value. (Contributed by NM, 2-Jan-2015.)
|- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` S )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   &    |- ( ph -> ( K ` G ) = ( K ` H ) )   &    |- ( ph -> ( G ` X ) = ( H ` X ) )   &    |- ( ph -> ( G ` X ) =/= .0. )   =>    |- ( ph -> G = H )
Theorem	lkrlsp 34702	The subspace sum of a kernel and the span of a vector not in the kernel (by ellkr 34689) is the whole vector space. (Contributed by NM, 19-Apr-2014.)
|- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) = V )
Theorem	lkrlsp2 34703	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.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) = V )
Theorem	lkrlsp3 34704	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.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( N ` ( ( K ` G ) u. { X } ) ) = V )
Theorem	lkrshp 34705	The kernel of a nonzero functional is a hyperplane. (Contributed by NM, 29-Jun-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( K ` G ) e. H )
Theorem	lkrshp3 34706	The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 17-Jul-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( K ` G ) e. H <-> G =/= ( V X. { .0. } ) ) )
Theorem	lkrshpor 34707	The kernel of a functional is either a hyperplane or the full vector space. (Contributed by NM, 7-Oct-2014.)
|- V = ( Base ` W )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( K ` G ) e. H \/ ( K ` G ) = V ) )
Theorem	lkrshp4 34708	A kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014.)
|- V = ( Base ` W )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( K ` G ) =/= V <-> ( K ` G ) e. H ) )
Theorem	lshpsmreu 34709*	Lemma for lshpkrex 34718. Show uniqueness of ring multiplier k when a vector X is broken down into components, one in a hyperplane and the other outside of it . TODO: do we need the cbvrexv 3071 for a to c? (Contributed by NM, 4-Jan-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   =>    |- ( ph -> E! k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) )
Theorem	lshpkrlem1 34710*	Lemma for lshpkrex 34718. The value of tentative functional G is zero iff its argument belongs to hyperplane U. (Contributed by NM, 14-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ph -> ( X e. U <-> ( G ` X ) = .0. ) )
Theorem	lshpkrlem2 34711*	Lemma for lshpkrex 34718. The value of tentative functional G is a scalar. (Contributed by NM, 16-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ph -> ( G ` X ) e. K )
Theorem	lshpkrlem3 34712*	Lemma for lshpkrex 34718. Defining property of G ` X. (Contributed by NM, 15-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ph -> E. z e. U X = ( z .+ ( ( G ` X ) .x. Z ) ) )
Theorem	lshpkrlem4 34713*	Lemma for lshpkrex 34718. Part of showing linearity of G. (Contributed by NM, 16-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) ) ) -> ( ( l .x. u ) .+ v ) = ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) ) )
Theorem	lshpkrlem5 34714*	Lemma for lshpkrex 34718. Part of showing linearity of G. (Contributed by NM, 16-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( G ` ( ( l .x. u ) .+ v ) ) = ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) )
Theorem	lshpkrlem6 34715*	Lemma for lshpkrex 34718. Show linearlity of G. (Contributed by NM, 17-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` D )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   =>    |- ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> ( G ` ( ( l .x. u ) .+ v ) ) = ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) )
Theorem	lshpkrcl 34716*	The set G defined by hyperplane U is a linear functional. (Contributed by NM, 17-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   &    |- F = (LFnl ` W )   =>    |- ( ph -> G e. F )
Theorem	lshpkr 34717*	The kernel of functional G is the hyperplane defining it. (Contributed by NM, 17-Jul-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> Z e. V )   &    |- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )   &    |- D = (Scalar ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .s ` W )   &    |- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )   &    |- L = (LKer ` W )   =>    |- ( ph -> ( L ` G ) = U )
Theorem	lshpkrex 34718*	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.)
|- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( ( W e. LVec /\ U e. H ) -> E. g e. F ( K ` g ) = U )
Theorem	lshpset2N 34719*	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.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( W e. LVec -> H = { s | E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) } )
Theorem	islshpkrN 34720*	The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be U = ( K ` g ) or ( K ` g ) = U as in lshpkrex 34718? 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.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- .0. = ( 0g ` D )   &    |- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   =>    |- ( W e. LVec -> ( U e. H <-> E. g e. F ( g =/= ( V X. { .0. } ) /\ U = ( K ` g ) ) ) )
Theorem	lfl1dim 34721*	Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> { g e. F | ( L ` G ) C_ ( L ` g ) } = { g | E. k e. K g = ( G oF .x. ( V X. { k } ) ) } )
Theorem	lfl1dim2N 34722*	Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim 34721 may be more compatible with lspsn 17627. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- D = (Scalar ` W )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   &    |- K = ( Base ` D )   &    |- .x. = ( .r ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> { g e. F | ( L ` G ) C_ ( L ` g ) } = { g e. F | E. k e. K g = ( G oF .x. ( V X. { k } ) ) } )
21.30.5  Opposite rings and dual vector spaces
Syntax	cld 34723	Extend class notation with left dualvector space.
class LDual
Definition	df-ldual 34724*	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 oF ( +g ` v ) allows it to be a set; see ofmres 6781. 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 e. _V |-> ( { <. ( Base ` ndx ) , (LFnl ` v ) >. , <. ( +g ` ndx ) , ( oF ( +g ` (Scalar ` v ) ) |` ( (LFnl ` v ) X. (LFnl ` v ) ) ) >. , <. (Scalar ` ndx ) , (oppr ` (Scalar ` v ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` (Scalar ` v ) ) , f e. (LFnl ` v ) |-> ( f oF ( .r ` (Scalar ` v ) ) ( ( Base ` v ) X. { k } ) ) ) >. } ) )
Theorem	ldualset 34725*	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.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` R )   &    |- .+b = ( oF .+ |` ( F X. F ) )   &    |- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- O = (oppr ` R )   &    |- .xb = ( k e. K , f e. F |-> ( f oF .x. ( V X. { k } ) ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> D = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. (Scalar ` ndx ) , O >. } u. { <. ( .s ` ndx ) , .xb >. } ) )
Theorem	ldualvbase 34726	The vectors of a dual space are functionals of the original space. (Contributed by NM, 18-Oct-2014.)
|- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- V = ( Base ` D )   &    |- ( ph -> W e. X )   =>    |- ( ph -> V = F )
Theorem	ldualelvbase 34727	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.)
|- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- V = ( Base ` D )   &    |- ( ph -> W e. X )   &    |- ( ph -> G e. F )   =>    |- ( ph -> G e. V )
Theorem	ldualfvadd 34728	Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.)
|- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- .+ = ( +g ` R )   &    |- D = (LDual ` W )   &    |- .+b = ( +g ` D )   &    |- ( ph -> W e. X )   &    |- .+^ = ( oF .+ |` ( F X. F ) )   =>    |- ( ph -> .+b = .+^ )
Theorem	ldualvadd 34729	Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.)
|- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- .+ = ( +g ` R )   &    |- D = (LDual ` W )   &    |- .+b = ( +g ` D )   &    |- ( ph -> W e. X )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( G .+b H ) = ( G oF .+ H ) )
Theorem	ldualvaddcl 34730	The value of vector addition in the dual of a vector space is a functional. (Contributed by NM, 21-Oct-2014.)
|- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- .+ = ( +g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( G .+ H ) e. F )
Theorem	ldualvaddval 34731	The value of the value of vector addition in the dual of a vector space. (Contributed by NM, 7-Jan-2015.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- .+ = ( +g ` R )   &    |- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- .+b = ( +g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( G .+b H ) ` X ) = ( ( G ` X ) .+ ( H ` X ) ) )
Theorem	ldualsca 34732	The ring of scalars of the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
|- F = (Scalar ` W )   &    |- O = (oppr ` F )   &    |- D = (LDual ` W )   &    |- R = (Scalar ` D )   &    |- ( ph -> W e. X )   =>    |- ( ph -> R = O )
Theorem	ldualsbase 34733	Base set of scalar ring for the dual of a vector space. (Contributed by NM, 24-Oct-2014.)
|- F = (Scalar ` W )   &    |- L = ( Base ` F )   &    |- D = (LDual ` W )   &    |- R = (Scalar ` D )   &    |- K = ( Base ` R )   &    |- ( ph -> W e. V )   =>    |- ( ph -> K = L )
Theorem	ldualsaddN 34734	Scalar addition for the dual of a vector space. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.)
|- F = (Scalar ` W )   &    |- .+ = ( +g ` F )   &    |- D = (LDual ` W )   &    |- R = (Scalar ` D )   &    |- .+b = ( +g ` R )   &    |- ( ph -> W e. V )   =>    |- ( ph -> .+b = .+ )
Theorem	ldualsmul 34735	Scalar multiplication for the dual of a vector space. (Contributed by NM, 19-Oct-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .r ` F )   &    |- D = (LDual ` W )   &    |- R = (Scalar ` D )   &    |- .xb = ( .r ` R )   &    |- ( ph -> W e. V )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. K )   =>    |- ( ph -> ( X .xb Y ) = ( Y .x. X ) )
Theorem	ldualfvs 34736*	Scalar product operation for the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
|- F = (LFnl ` W )   &    |- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- D = (LDual ` W )   &    |- .xb = ( .s ` D )   &    |- ( ph -> W e. Y )   &    |- .x. = ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) )   =>    |- ( ph -> .xb = .x. )
Theorem	ldualvs 34737	Scalar product operation value (which is a functional) for the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
|- F = (LFnl ` W )   &    |- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- D = (LDual ` W )   &    |- .xb = ( .s ` D )   &    |- ( ph -> W e. Y )   &    |- ( ph -> X e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( X .xb G ) = ( G oF .X. ( V X. { X } ) ) )
Theorem	ldualvsval 34738	Value of scalar product operation value for the dual of a vector space. (Contributed by NM, 18-Oct-2014.)
|- F = (LFnl ` W )   &    |- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- D = (LDual ` W )   &    |- .xb = ( .s ` D )   &    |- ( ph -> W e. Y )   &    |- ( ph -> X e. K )   &    |- ( ph -> G e. F )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( ( X .xb G ) ` A ) = ( ( G ` A ) .X. X ) )
Theorem	ldualvscl 34739	The scalar product operation value is a functional. (Contributed by NM, 18-Oct-2014.)
|- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- D = (LDual ` W )   &    |- .x. = ( .s ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( X .x. G ) e. F )
Theorem	ldualvaddcom 34740	Commutative law for vector (functional) addition. (Contributed by NM, 17-Jan-2015.)
|- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- .+ = ( +g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. F )   &    |- ( ph -> Y e. F )   =>    |- ( ph -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	ldualvsass 34741	Associative law for scalar product operation. (Contributed by NM, 20-Oct-2014.)
|- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- D = (LDual ` W )   &    |- .x. = ( .s ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( Y .X. X ) .x. G ) = ( X .x. ( Y .x. G ) ) )
Theorem	ldualvsass2 34742	Associative law for scalar product operation, using operations from the dual space. (Contributed by NM, 20-Oct-2014.)
|- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- D = (LDual ` W )   &    |- Q = (Scalar ` D )   &    |- .X. = ( .r ` Q )   &    |- .x. = ( .s ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( X .X. Y ) .x. G ) = ( X .x. ( Y .x. G ) ) )
Theorem	ldualvsdi1 34743	Distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014.)
|- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- D = (LDual ` W )   &    |- .+ = ( +g ` D )   &    |- .x. = ( .s ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( X .x. ( G .+ H ) ) = ( ( X .x. G ) .+ ( X .x. H ) ) )
Theorem	ldualvsdi2 34744	Reverse distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014.)
|- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- .+ = ( +g ` R )   &    |- K = ( Base ` R )   &    |- D = (LDual ` W )   &    |- .+b = ( +g ` D )   &    |- .x. = ( .s ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. K )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( X .+ Y ) .x. G ) = ( ( X .x. G ) .+b ( Y .x. G ) ) )
Theorem	ldualgrplem 34745	Lemma for ldualgrp 34746. (Contributed by NM, 22-Oct-2014.)
|- D = (LDual ` W )   &    |- ( ph -> W e. LMod )   &    |- V = ( Base ` W )   &    |- .+ = oF ( +g ` W )   &    |- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- O = (oppr ` R )   &    |- .x. = ( .s ` D )   =>    |- ( ph -> D e. Grp )
Theorem	ldualgrp 34746	The dual of a vector space is a group. (Contributed by NM, 21-Oct-2014.)
|- D = (LDual ` W )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> D e. Grp )
Theorem	ldual0 34747	The zero scalar of the dual of a vector space. (Contributed by NM, 28-Dec-2014.)
|- R = (Scalar ` W )   &    |- .0. = ( 0g ` R )   &    |- D = (LDual ` W )   &    |- S = (Scalar ` D )   &    |- O = ( 0g ` S )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> O = .0. )
Theorem	ldual1 34748	The unit scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015.)
|- R = (Scalar ` W )   &    |- .1. = ( 1r ` R )   &    |- D = (LDual ` W )   &    |- S = (Scalar ` D )   &    |- I = ( 1r ` S )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> I = .1. )
Theorem	ldualneg 34749	The negative of a scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015.)
|- R = (Scalar ` W )   &    |- M = ( invg ` R )   &    |- D = (LDual ` W )   &    |- S = (Scalar ` D )   &    |- N = ( invg ` S )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> N = M )
Theorem	ldual0v 34750	The zero vector of the dual of a vector space. (Contributed by NM, 24-Oct-2014.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- .0. = ( 0g ` R )   &    |- D = (LDual ` W )   &    |- O = ( 0g ` D )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> O = ( V X. { .0. } ) )
Theorem	ldual0vcl 34751	The dual zero vector is a functional. (Contributed by NM, 5-Mar-2015.)
|- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- .0. = ( 0g ` D )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> .0. e. F )
Theorem	lduallmodlem 34752	Lemma for lduallmod 34753. (Contributed by NM, 22-Oct-2014.)
|- D = (LDual ` W )   &    |- ( ph -> W e. LMod )   &    |- V = ( Base ` W )   &    |- .+ = oF ( +g ` W )   &    |- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- O = (oppr ` R )   &    |- .x. = ( .s ` D )   =>    |- ( ph -> D e. LMod )
Theorem	lduallmod 34753	The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014.)
|- D = (LDual ` W )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> D e. LMod )
Theorem	lduallvec 34754	The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr 17251; otherwise, the dual would be a right vector space as is sometimes the case in the literature. (Contributed by NM, 22-Oct-2014.)
|- D = (LDual ` W )   &    |- ( ph -> W e. LVec )   =>    |- ( ph -> D e. LVec )
Theorem	ldualvsub 34755	The value of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.)
|- R = (Scalar ` W )   &    |- N = ( invg ` R )   &    |- .1. = ( 1r ` R )   &    |- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- .+ = ( +g ` D )   &    |- .x. = ( .s ` D )   &    |- .- = ( -g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( G .- H ) = ( G .+ ( ( N ` .1. ) .x. H ) ) )
Theorem	ldualvsubcl 34756	Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.)
|- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- .- = ( -g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( G .- H ) e. F )
Theorem	ldualvsubval 34757	The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 34755? (Requires D to oppr conversion.) (Contributed by NM, 26-Feb-2015.)
|- V = ( Base ` W )   &    |- R = (Scalar ` W )   &    |- S = ( -g ` R )   &    |- F = (LFnl ` W )   &    |- D = (LDual ` W )   &    |- .- = ( -g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( G .- H ) ` X ) = ( ( G ` X ) S ( H ` X ) ) )
Theorem	ldualssvscl 34758	Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015.)
|- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- D = (LDual ` W )   &    |- .x. = ( .s ` D )   &    |- S = ( LSubSp ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. U )   =>    |- ( ph -> ( X .x. Y ) e. U )
Theorem	ldualssvsubcl 34759	Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015.)
|- D = (LDual ` W )   &    |- .- = ( -g ` D )   &    |- S = ( LSubSp ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   =>    |- ( ph -> ( X .- Y ) e. U )
Theorem	ldual0vs 34760	Scalar zero times a functional is the zero functional. (Contributed by NM, 17-Feb-2015.)
|- F = (LFnl ` W )   &    |- R = (Scalar ` W )   &    |- .0. = ( 0g ` R )   &    |- D = (LDual ` W )   &    |- .x. = ( .s ` D )   &    |- O = ( 0g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( .0. .x. G ) = O )
Theorem	lkr0f2 34761	The kernel of the zero functional is the set of all vectors. (Contributed by NM, 4-Feb-2015.)
|- V = ( Base ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- D = (LDual ` W )   &    |- .0. = ( 0g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( K ` G ) = V <-> G = .0. ) )
Theorem	lduallkr3 34762	The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.)
|- H = (LSHyp ` W )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- D = (LDual ` W )   &    |- .0. = ( 0g ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( ( K ` G ) e. H <-> G =/= .0. ) )
Theorem	lkrpssN 34763	Proper subset relation between kernels. (Contributed by NM, 16-Feb-2015.) (New usage is discouraged.)
|- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- D = (LDual ` W )   &    |- .0. = ( 0g ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( ( K ` G ) C. ( K ` H ) <-> ( G =/= .0. /\ H = .0. ) ) )
Theorem	lkrin 34764	Intersection of the kernels of 2 functionals is included in the kernel of their sum. (Contributed by NM, 7-Jan-2015.)
|- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- D = (LDual ` W )   &    |- .+ = ( +g ` D )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( ( K ` G ) i^i ( K ` H ) ) C_ ( K ` ( G .+ H ) ) )
Theorem	eqlkr4 34765*	Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 4-Feb-2015.)
|- S = (Scalar ` W )   &    |- R = ( Base ` S )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- D = (LDual ` W )   &    |- .x. = ( .s ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   &    |- ( ph -> ( K ` G ) = ( K ` H ) )   =>    |- ( ph -> E. r e. R H = ( r .x. G ) )
Theorem	ldual1dim 34766*	Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.)
|- F = (LFnl ` W )   &    |- L = (LKer ` W )   &    |- D = (LDual ` W )   &    |- N = ( LSpan ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   =>    |- ( ph -> ( N ` { G } ) = { g e. F | ( L ` G ) C_ ( L ` g ) } )
Theorem	ldualkrsc 34767	The kernel of a non-zero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 28-Dec-2014.)
|- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   &    |- D = (LDual ` W )   &    |- .x. = ( .s ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. K )   &    |- ( ph -> X =/= .0. )   =>    |- ( ph -> ( L ` ( X .x. G ) ) = ( L ` G ) )
Theorem	lkrss 34768	The kernel of a scalar product of a functional includes the kernel of the functional. (Contributed by NM, 27-Jan-2015.)
|- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- F = (LFnl ` W )   &    |- L = (LKer ` W )   &    |- D = (LDual ` W )   &    |- .x. = ( .s ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   &    |- ( ph -> X e. K )   =>    |- ( ph -> ( L ` G ) C_ ( L ` ( X .x. G ) ) )
Theorem	lkrss2N 34769*	Two functionals with kernels in a subset relationship. (Contributed by NM, 17-Feb-2015.) (New usage is discouraged.)
|- S = (Scalar ` W )   &    |- R = ( Base ` S )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- D = (LDual ` W )   &    |- .x. = ( .s ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> G e. F )   &    |- ( ph -> H e. F )   =>    |- ( ph -> ( ( K ` G ) C_ ( K ` H ) <-> E. r e. R H = ( r .x. G ) ) )
Theorem	lkreqN 34770	Proportional functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
|- S = (Scalar ` W )   &    |- R = ( Base ` S )   &    |- .0. = ( 0g ` S )   &    |- F = (LFnl ` W )   &    |- K = (LKer ` W )   &    |- D = (LDual ` W )   &    |- .x. = ( .s ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> A e. ( R \ { .0. } ) )   &    |- ( ph -> H e. F )   &    |- ( ph -> G = ( A .x. H ) )   =>    |- ( ph -> ( K ` G ) = ( K ` H ) )
Theorem	lkrlspeqN 34771	Condition for colinear functionals to have equal kernels. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
|- F = (LFnl ` W )   &    |- L = (LKer ` W )   &    |- D = (LDual ` W )   &    |- .0. = ( 0g ` D )   &    |- N = ( LSpan ` D )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> H e. F )   &    |- ( ph -> G e. ( ( N ` { H } ) \ { .0. } ) )   =>    |- ( ph -> ( L ` G ) = ( L ` H ) )
21.30.6  Ortholattices and orthomodular lattices
Syntax	cops 34772	Extend class notation with orthoposets.
class OP
Syntax	ccmtN 34773	Extend class notation with the commutes relation.
class cm
Syntax	col 34774	Extend class notation with orthlattices.
class OL
Syntax	coml 34775	Extend class notation with orthomodular lattices.
class OML
Definition	df-oposet 34776*	Define the class of orthoposets, which are bounded posets with an orthocomplementation operation. Note that ( Base p ) e. dom ( lub p ) 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 = { p e. Poset | ( ( ( Base ` p ) e. dom ( lub ` p ) /\ ( Base ` p ) e. dom ( glb ` p ) ) /\ E. o ( o = ( oc ` p ) /\ A. a e. ( Base ` p ) A. b e. ( Base ` p ) ( ( ( o ` a ) e. ( Base ` p ) /\ ( o ` ( o ` a ) ) = a /\ ( a ( le ` p ) b -> ( o ` b ) ( le ` p ) ( o ` a ) ) ) /\ ( a ( join ` p ) ( o ` a ) ) = ( 1. ` p ) /\ ( a ( meet ` p ) ( o ` a ) ) = ( 0. ` p ) ) ) ) }
Definition	df-cmtN 34777*	Define the commutes relation for orthoposets. Definition of commutes in [Kalmbach] p. 20. (Contributed by NM, 6-Nov-2011.)
|- cm = ( p e. _V |-> { <. x , y >. | ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) ) } )
Definition	df-ol 34778	Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.)
|- OL = ( Lat i^i OP )
Definition	df-oml 34779*	Define the class of orthomodular lattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.)
|- OML = { l e. OL | A. a e. ( Base ` l ) A. b e. ( Base ` l ) ( a ( le ` l ) b -> b = ( a ( join ` l ) ( b ( meet ` l ) ( ( oc ` l ) ` a ) ) ) ) }
Theorem	isopos 34780*	The predicate "is an orthoposet." (Contributed by NM, 20-Oct-2011.) (Revised by NM, 14-Sep-2018.)
|- B = ( Base ` K )   &    |- U = ( lub ` K )   &    |- G = ( glb ` K )   &    |- .<_ = ( le ` K )   &    |- ._|_ = ( oc ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- .1. = ( 1. ` K )   =>    |- ( K e. OP <-> ( ( K e. Poset /\ B e. dom U /\ B e. dom G ) /\ A. x e. B A. y e. B ( ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) /\ ( x .\/ ( ._|_ ` x ) ) = .1. /\ ( x ./\ ( ._|_ ` x ) ) = .0. ) ) )
Theorem	opposet 34781	Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.)
|- ( K e. OP -> K e. Poset )
Theorem	oposlem 34782	Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- ._|_ = ( oc ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- .1. = ( 1. ` K )   =>    |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X .<_ Y -> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) ) /\ ( X .\/ ( ._|_ ` X ) ) = .1. /\ ( X ./\ ( ._|_ ` X ) ) = .0. ) )
Theorem	op01dm 34783	Conditions necessary for zero and unit elements to exist. (Contributed by NM, 14-Sep-2018.)
|- B = ( Base ` K )   &    |- U = ( lub ` K )   &    |- G = ( glb ` K )   =>    |- ( K e. OP -> ( B e. dom U /\ B e. dom G ) )
Theorem	op0cl 34784	An orthoposet has a zero element. (h0elch 26151 analog.) (Contributed by NM, 12-Oct-2011.)
|- B = ( Base ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( K e. OP -> .0. e. B )
Theorem	op1cl 34785	An orthoposet has a unit element. (helch 26139 analog.) (Contributed by NM, 22-Oct-2011.)
|- B = ( Base ` K )   &    |- .1. = ( 1. ` K )   =>    |- ( K e. OP -> .1. e. B )
Theorem	op0le 34786	Orthoposet zero is less than or equal to any element. (ch0le 26337 analog.) (Contributed by NM, 12-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( ( K e. OP /\ X e. B ) -> .0. .<_ X )
Theorem	ople0 34787	An element less than or equal to zero equals zero. (chle0 26339 analog.) (Contributed by NM, 21-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( ( K e. OP /\ X e. B ) -> ( X .<_ .0. <-> X = .0. ) )
Theorem	opnlen0 34788	An element not less than another is nonzero. TODO: Look for uses of necon3bd 2655 and op0le 34786 to see if this is useful elsewhere. (Contributed by NM, 5-May-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( ( ( K e. OP /\ X e. B /\ Y e. B ) /\ -. X .<_ Y ) -> X =/= .0. )
Theorem	lub0N 34789	The least upper bound of the empty set is the zero element. (Contributed by NM, 15-Sep-2013.) (New usage is discouraged.)
|- .1. = ( lub ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( K e. OP -> ( .1. ` (/) ) = .0. )
Theorem	opltn0 34790	A lattice element greater than zero is nonzero. TODO: is this needed? (Contributed by NM, 1-Jun-2012.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( ( K e. OP /\ X e. B ) -> ( .0. .< X <-> X =/= .0. ) )
Theorem	ople1 34791	Any element is less than the orthoposet unit. (chss 26125 analog.) (Contributed by NM, 23-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .1. = ( 1. ` K )   =>    |- ( ( K e. OP /\ X e. B ) -> X .<_ .1. )
Theorem	op1le 34792	If the orthoposet unit is less than or equal to an element, the element equals the unit. (chle0 26339 analog.) (Contributed by NM, 5-Dec-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .1. = ( 1. ` K )   =>    |- ( ( K e. OP /\ X e. B ) -> ( .1. .<_ X <-> X = .1. ) )
Theorem	glb0N 34793	The greatest lower bound of the empty set is the unit element. (Contributed by NM, 5-Dec-2011.) (New usage is discouraged.)
|- G = ( glb ` K )   &    |- .1. = ( 1. ` K )   =>    |- ( K e. OP -> ( G ` (/) ) = .1. )
Theorem	opoccl 34794	Closure of orthocomplement operation. (choccl 26202 analog.) (Contributed by NM, 20-Oct-2011.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )
Theorem	opococ 34795	Double negative law for orthoposets. (ococ 26302 analog.) (Contributed by NM, 13-Sep-2011.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
Theorem	opcon3b 34796	Contraposition law for orthoposets. (chcon3i 26362 analog.) (Contributed by NM, 8-Nov-2011.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X = Y <-> ( ._|_ ` Y ) = ( ._|_ ` X ) ) )
Theorem	opcon2b 34797	Orthocomplement contraposition law. (negcon2 9877 analog.) (Contributed by NM, 16-Jan-2012.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X = ( ._|_ ` Y ) <-> Y = ( ._|_ ` X ) ) )
Theorem	opcon1b 34798	Orthocomplement contraposition law. (negcon1 9876 analog.) (Contributed by NM, 24-Jan-2012.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) = Y <-> ( ._|_ ` Y ) = X ) )
Theorem	oplecon3 34799	Contraposition law for orthoposets. (Contributed by NM, 13-Sep-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) )
Theorem	oplecon3b 34800	Contraposition law for orthoposets. (chsscon3 26396 analog.) (Contributed by NM, 4-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) )