P. 327 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32601-32700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lshpkrcl 32601*	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 32602*	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 32603*	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 32604*	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 32605*	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 32603? 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 32606*	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 32607*	Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim 32606 may be more compatible with lspsn 18213. (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.21.8  Opposite rings and dual vector spaces
Syntax	cld 32608	Extend class notation with left dualvector space.
class LDual
Definition	df-ldual 32609*	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 6800. 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 32610*	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 32611	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 32612	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 32613	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 32614	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 32615	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 32616	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 32617	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 32618	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 32619	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 32620	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 32621*	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 32622	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 32623	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 32624	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 32625	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 32626	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 32627	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 32628	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 32629	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 32630	Lemma for ldualgrp 32631. (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 32631	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 32632	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 32633	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 32634	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 32635	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 32636	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 32637	Lemma for lduallmod 32638. (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 32638	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 32639	The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr 17839; 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 32640	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 32641	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 32642	The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 32640? (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 32643	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 32644	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 32645	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 32646	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 32647	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 32648	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 32649	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 32650*	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 32651*	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 32652	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 32653	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 32654*	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 32655	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 32656	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.21.9  Ortholattices and orthomodular lattices
Syntax	cops 32657	Extend class notation with orthoposets.
class OP
Syntax	ccmtN 32658	Extend class notation with the commutes relation.
class cm
Syntax	col 32659	Extend class notation with orthlattices.
class OL
Syntax	coml 32660	Extend class notation with orthomodular lattices.
class OML
Definition	df-oposet 32661*	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 32662*	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 32663	Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.)
|- OL = ( Lat i^i OP )
Definition	df-oml 32664*	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 32665*	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 32666	Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.)
|- ( K e. OP -> K e. Poset )
Theorem	oposlem 32667	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 32668	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 32669	An orthoposet has a zero element. (h0elch 26894 analog.) (Contributed by NM, 12-Oct-2011.)
|- B = ( Base ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( K e. OP -> .0. e. B )
Theorem	op1cl 32670	An orthoposet has a unit element. (helch 26882 analog.) (Contributed by NM, 22-Oct-2011.)
|- B = ( Base ` K )   &    |- .1. = ( 1. ` K )   =>    |- ( K e. OP -> .1. e. B )
Theorem	op0le 32671	Orthoposet zero is less than or equal to any element. (ch0le 27080 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 32672	An element less than or equal to zero equals zero. (chle0 27082 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 32673	An element not less than another is nonzero. TODO: Look for uses of necon3bd 2636 and op0le 32671 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 32674	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 32675	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 32676	Any element is less than the orthoposet unit. (chss 26868 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 32677	If the orthoposet unit is less than or equal to an element, the element equals the unit. (chle0 27082 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 32678	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 32679	Closure of orthocomplement operation. (choccl 26945 analog.) (Contributed by NM, 20-Oct-2011.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )
Theorem	opococ 32680	Double negative law for orthoposets. (ococ 27045 analog.) (Contributed by NM, 13-Sep-2011.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
Theorem	opcon3b 32681	Contraposition law for orthoposets. (chcon3i 27105 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 32682	Orthocomplement contraposition law. (negcon2 9928 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 32683	Orthocomplement contraposition law. (negcon1 9927 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 32684	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 32685	Contraposition law for orthoposets. (chsscon3 27139 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 ) ) )
Theorem	oplecon1b 32686	Contraposition law for strict ordering in orthoposets. (chsscon1 27140 analog.) (Contributed by NM, 6-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) .<_ Y <-> ( ._|_ ` Y ) .<_ X ) )
Theorem	opoc1 32687	Orthocomplement of orthoposet unit. (Contributed by NM, 24-Jan-2012.)
|- .0. = ( 0. ` K )   &    |- .1. = ( 1. ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( K e. OP -> ( ._|_ ` .1. ) = .0. )
Theorem	opoc0 32688	Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012.)
|- .0. = ( 0. ` K )   &    |- .1. = ( 1. ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( K e. OP -> ( ._|_ ` .0. ) = .1. )
Theorem	opltcon3b 32689	Contraposition law for strict ordering in orthoposets. (chpsscon3 27142 analog.) (Contributed by NM, 4-Nov-2011.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( ._|_ ` Y ) .< ( ._|_ ` X ) ) )
Theorem	opltcon1b 32690	Contraposition law for strict ordering in orthoposets. (chpsscon1 27143 analog.) (Contributed by NM, 5-Nov-2011.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) .< Y <-> ( ._|_ ` Y ) .< X ) )
Theorem	opltcon2b 32691	Contraposition law for strict ordering in orthoposets. (chsscon2 27141 analog.) (Contributed by NM, 5-Nov-2011.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .< ( ._|_ ` Y ) <-> Y .< ( ._|_ ` X ) ) )
Theorem	opexmid 32692	Law of excluded middle for orthoposets. (chjo 27154 analog.) (Contributed by NM, 13-Sep-2011.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   &    |- .\/ = ( join ` K )   &    |- .1. = ( 1. ` K )   =>    |- ( ( K e. OP /\ X e. B ) -> ( X .\/ ( ._|_ ` X ) ) = .1. )
Theorem	opnoncon 32693	Law of contradiction for orthoposets. (chocin 27134 analog.) (Contributed by NM, 13-Sep-2011.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( ( K e. OP /\ X e. B ) -> ( X ./\ ( ._|_ ` X ) ) = .0. )
Theorem	riotaocN 32694*	The orthocomplement of the unique poset element such that ps. (riotaneg 10587 analog.) (Contributed by NM, 16-Jan-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   &    |- ( x = ( ._|_ ` y ) -> ( ph <-> ps ) )   =>    |- ( ( K e. OP /\ E! x e. B ph ) -> ( iota_ x e. B ph ) = ( ._|_ ` ( iota_ y e. B ps ) ) )
Theorem	cmtfvalN 32695*	Value of commutes relation. (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- C = ( cm ` K )   =>    |- ( K e. A -> C = { <. x , y >. | ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } )
Theorem	cmtvalN 32696	Equivalence for commutes relation. Definition of commutes in [Kalmbach] p. 20. (cmbr 27223 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- C = ( cm ` K )   =>    |- ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) )
Theorem	isolat 32697	The predicate "is an ortholattice." (Contributed by NM, 18-Sep-2011.)
|- ( K e. OL <-> ( K e. Lat /\ K e. OP ) )
Theorem	ollat 32698	An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.)
|- ( K e. OL -> K e. Lat )
Theorem	olop 32699	An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.)
|- ( K e. OL -> K e. OP )
Theorem	olposN 32700	An ortholattice is a poset. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.)
|- ( K e. OL -> K e. Poset )