P. 347 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34601-34700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvhlveclem 34601	Lemma for dvhlvec 34602. TODO: proof substituting inner part first shorter/longer than substituting outer part first? TODO: break up into smaller lemmas? TODO: does ph -> method shorten proof? (Contributed by NM, 22-Oct-2013.) (Proof shortened by Mario Carneiro, 24-Jun-2014.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (Scalar ` U )   &    |- .+^ = ( +g ` D )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` D )   &    |- I = ( invg ` D )   &    |- .X. = ( .r ` D )   &    |- .x. = ( .s ` U )   =>    |- ( ( K e. HL /\ W e. H ) -> U e. LVec )
Theorem	dvhlvec 34602	The full vector space U constructed from a Hilbert lattice K (given a fiducial hyperplane W) is a left module. (Contributed by NM, 23-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> U e. LVec )
Theorem	dvhlmod 34603	The full vector space U constructed from a Hilbert lattice K (given a fiducial hyperplane W) is a left module. (Contributed by NM, 23-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> U e. LMod )
Theorem	dvh0g 34604*	The zero vector of vector space H has the zero translation as its first member and the zero trace-preserving endomorphism as the second. (Contributed by NM, 9-Mar-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .0. = ( 0g ` U )   &    |- O = ( f e. T |-> ( _I |` B ) )   =>    |- ( ( K e. HL /\ W e. H ) -> .0. = <. ( _I |` B ) , O >. )
Theorem	dvheveccl 34605	Properties of a unit vector that we will use later as a convenient reference vector. This vector is called "e" in the remark after Lemma M of [Crawley] p. 121. line 17. See also dvhopN 34609 and dihpN 34829. (Contributed by NM, 27-Mar-2015.)
|- H = ( LHyp ` K )   &    |- B = ( Base ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- E = <. ( _I |` B ) , ( _I |` T ) >.   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> E e. ( V \ { .0. } ) )
Theorem	dvhopclN 34606	Closure of a DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.)
|- ( ( F e. T /\ U e. E ) -> <. F , U >. e. ( T X. E ) )
Theorem	dvhopaddN 34607*	Sum of DVecH vectors expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.)
|- A = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) P ( 2nd ` g ) ) >. )   =>    |- ( ( ( F e. T /\ U e. E ) /\ ( G e. T /\ V e. E ) ) -> ( <. F , U >. A <. G , V >. ) = <. ( F o. G ) , ( U P V ) >. )
Theorem	dvhopspN 34608*	Scalar product of DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.)
|- S = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )   =>    |- ( ( R e. E /\ ( F e. T /\ U e. E ) ) -> ( R S <. F , U >. ) = <. ( R ` F ) , ( R o. U ) >. )
Theorem	dvhopN 34609*	Decompose a DVecH vector expressed as an ordered pair into the sum of two components, the first from the translation group vector base of DVecA and the other from the one-dimensional vector subspace E. Part of Lemma M of [Crawley] p. 121, line 18. We represent their e, sigma, f by <. ( _I |` B ) , ( _I |` T ) >., U, <. F , O >.. We swapped the order of vector sum (their juxtaposition i.e. composition) to show <. F , O >. first. Note that O and ( _I |` T ) are the zero and one of the division ring E, and ( _I |` B ) is the zero of the translation group. S is the scalar product. (Contributed by NM, 21-Nov-2013.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- P = ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) )   &    |- A = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) P ( 2nd ` g ) ) >. )   &    |- S = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )   &    |- O = ( c e. T |-> ( _I |` B ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> <. F , U >. = ( <. F , O >. A ( U S <. ( _I |` B ) , ( _I |` T ) >. ) ) )
Theorem	dvhopellsm 34610*	Ordered pair membership in a subspace sum. (Contributed by NM, 12-Mar-2014.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- S = ( LSubSp ` U )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( <. F , T >. e. ( X .(+) Y ) <-> E. x E. y E. z E. w ( ( <. x , y >. e. X /\ <. z , w >. e. Y ) /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )
Theorem	cdlemm10N 34611*	The image of the map G is the entire one-dimensional subspace ( I ` V ). Remark after Lemma M of [Crawley] p. 121 line 23. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- C = { r e. A | ( r .<_ ( P .\/ V ) /\ -. r .<_ W ) }   &    |- F = ( iota_ f e. T ( f ` P ) = s )   &    |- G = ( q e. C |-> ( iota_ f e. T ( f ` P ) = q ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ran G = ( I ` V ) )
Syntax	cocaN 34612	Extend class notation with subspace orthocomplement for DVecA partial vector space.
class ocA
Definition	df-docaN 34613*	Define subspace orthocomplement for DVecA partial vector space. Temporarily, we are using the range of the isomorphism instead of the set of closed subspaces. Later, when inner product is introduced, we will show that these are the same. (Contributed by NM, 6-Dec-2013.)
|- ocA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( DIsoA ` k ) ` w ) ` ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w ) ) ) ) )
Theorem	docaffvalN 34614*	Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- H = ( LHyp ` K )   =>    |- ( K e. V -> ( ocA ` K ) = ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( DIsoA ` K ) ` w ) ` ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) ) ) ) )
Theorem	docafvalN 34615*	Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- N = ( ( ocA ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> N = ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) ) )
Theorem	docavalN 34616*	Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- N = ( ( ocA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( N ` X ) = ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) )
Theorem	docaclN 34617	Closure of subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ._|_ ` X ) e. ran I )
Theorem	diaocN 34618	Value of partial isomorphism A at lattice orthocomplement (using a Sasaki projection to get orthocomplement relative to the fiducial co-atom W). (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- N = ( ( ocA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` ( ( ( ._|_ ` X ) .\/ ( ._|_ ` W ) ) ./\ W ) ) = ( N ` ( I ` X ) ) )
Theorem	doca2N 34619	Double orthocomplement of partial isomorphism A. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ._|_ ` ( ._|_ ` ( I ` X ) ) ) = ( I ` X ) )
Theorem	doca3N 34620	Double orthocomplement of partial isomorphism A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
Theorem	dvadiaN 34621	Any closed subspace is a member of the range of partial isomorphism A, showing the isomorphism maps onto the set of closed subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecA ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   &    |- S = ( LSubSp ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. S /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) -> X e. ran I )
Theorem	diarnN 34622*	Partial isomorphism A maps onto the set of all closed subspaces of partial vector space A. Part of Lemma M of [Crawley] p. 121 line 12, with closed subspaces rather than subspaces. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecA ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   &    |- S = ( LSubSp ` U )   =>    |- ( ( K e. HL /\ W e. H ) -> ran I = { x e. S | ( ._|_ ` ( ._|_ ` x ) ) = x } )
Theorem	diaf1oN 34623*	The partial isomorphism A for a lattice K is a one-to-one, onto function. Part of Lemma M of [Crawley] p. 121 line 12, with closed subspaces rather than subspaces. See diadm 34528 for the domain. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecA ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   &    |- S = ( LSubSp ` U )   =>    |- ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> { x e. S | ( ._|_ ` ( ._|_ ` x ) ) = x } )
Syntax	cdjaN 34624	Extend class notation with subspace join for DVecA partial vector space.
class vA
Definition	df-djaN 34625*	Define (closed) subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.)
|- vA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) , y e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) ) ) )
Theorem	djaffvalN 34626*	Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   =>    |- ( K e. V -> ( vA ` K ) = ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) , y e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( ocA ` K ) ` w ) ` ( ( ( ( ocA ` K ) ` w ) ` x ) i^i ( ( ( ocA ` K ) ` w ) ` y ) ) ) ) ) )
Theorem	djafvalN 34627*	Subspace join for DVecA partial vector space. TODO: take out hypothesis .i, no longer used. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   &    |- J = ( ( vA ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> J = ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) )
Theorem	djavalN 34628	Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   &    |- J = ( ( vA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X J Y ) = ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
Theorem	djaclN 34629	Closure of subspace join for DVecA partial vector space. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- J = ( ( vA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X J Y ) e. ran I )
Theorem	djajN 34630	Transfer lattice join to DVecA partial vector space closed subspace join. Part of Lemma M of [Crawley] p. 120 line 29, with closed subspace join rather than subspace sum. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
|- .\/ = ( join ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- J = ( ( vA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` ( X .\/ Y ) ) = ( ( I ` X ) J ( I ` Y ) ) )
Syntax	cdib 34631	Extend class notation with isomorphism B.
class DIsoB
Definition	df-dib 34632*	Isomorphism B is isomorphism A extended with an extra dimension set to the zero vector component i.e. the zero endormorphism. Its domain is lattice elements less than or equal to the fiducial co-atom w. (Contributed by NM, 8-Dec-2013.)
|- DIsoB = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. dom ( ( DIsoA ` k ) ` w ) |-> ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } ) ) ) )
Theorem	dibffval 34633*	The partial isomorphism B for a lattice K. (Contributed by NM, 8-Dec-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   =>    |- ( K e. V -> ( DIsoB ` K ) = ( w e. H |-> ( x e. dom ( ( DIsoA ` K ) ` w ) |-> ( ( ( ( DIsoA ` K ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` K ) ` w ) |-> ( _I |` B ) ) } ) ) ) )
Theorem	dibfval 34634*	The partial isomorphism B for a lattice K. (Contributed by NM, 8-Dec-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .0. = ( f e. T |-> ( _I |` B ) )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> I = ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) )
Theorem	dibval 34635*	The partial isomorphism B for a lattice K. (Contributed by NM, 8-Dec-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .0. = ( f e. T |-> ( _I |` B ) )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( I ` X ) = ( ( J ` X ) X. { .0. } ) )
Theorem	dibopelvalN 34636*	Member of the partial isomorphism B. (Contributed by NM, 18-Jan-2014.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .0. = ( f e. T |-> ( _I |` B ) )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( <. F , S >. e. ( I ` X ) <-> ( F e. ( J ` X ) /\ S = .0. ) ) )
Theorem	dibval2 34637*	Value of the partial isomorphism B. (Contributed by NM, 18-Jan-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .0. = ( f e. T |-> ( _I |` B ) )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = ( ( J ` X ) X. { .0. } ) )
Theorem	dibopelval2 34638*	Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014.) (Revised by Mario Carneiro, 6-May-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .0. = ( f e. T |-> ( _I |` B ) )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( <. F , S >. e. ( I ` X ) <-> ( F e. ( J ` X ) /\ S = .0. ) ) )
Theorem	dibval3N 34639*	Value of the partial isomorphism B for a lattice K. (Contributed by NM, 24-Feb-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- .0. = ( g e. T |-> ( _I |` B ) )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = ( { f e. T | ( R ` f ) .<_ X } X. { .0. } ) )
Theorem	dibelval3 34640*	Member of the partial isomorphism B. (Contributed by NM, 26-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- .0. = ( g e. T |-> ( _I |` B ) )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( Y e. ( I ` X ) <-> E. f e. T ( Y = <. f , .0. >. /\ ( R ` f ) .<_ X ) ) )
Theorem	dibopelval3 34641*	Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- .0. = ( g e. T |-> ( _I |` B ) )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( <. F , S >. e. ( I ` X ) <-> ( ( F e. T /\ ( R ` F ) .<_ X ) /\ S = .0. ) ) )
Theorem	dibelval1st 34642	Membership in value of the partial isomorphism B for a lattice K. (Contributed by NM, 13-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ Y e. ( I ` X ) ) -> ( 1st ` Y ) e. ( J ` X ) )
Theorem	dibelval1st1 34643	Membership in value of the partial isomorphism B for a lattice K. (Contributed by NM, 13-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ Y e. ( I ` X ) ) -> ( 1st ` Y ) e. T )
Theorem	dibelval1st2N 34644	Membership in value of the partial isomorphism B for a lattice K. (Contributed by NM, 13-Feb-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ Y e. ( I ` X ) ) -> ( R ` ( 1st ` Y ) ) .<_ X )
Theorem	dibelval2nd 34645*	Membership in value of the partial isomorphism B for a lattice K. (Contributed by NM, 13-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .0. = ( f e. T |-> ( _I |` B ) )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ Y e. ( I ` X ) ) -> ( 2nd ` Y ) = .0. )
Theorem	dibn0 34646	The value of the partial isomorphism B is not empty. (Contributed by NM, 18-Jan-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) =/= (/) )
Theorem	dibfna 34647	Functionality and domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.)
|- H = ( LHyp ` K )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> I Fn dom J )
Theorem	dibdiadm 34648	Domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.)
|- H = ( LHyp ` K )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> dom I = dom J )
Theorem	dibfnN 34649*	Functionality and domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> I Fn { x e. B | x .<_ W } )
Theorem	dibdmN 34650*	Domain of the partial isomorphism A. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> dom I = { x e. B | x .<_ W } )
Theorem	dibeldmN 34651	Member of domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> ( X e. dom I <-> ( X e. B /\ X .<_ W ) ) )
Theorem	dibord 34652	The isomorphism B for a lattice K is order-preserving in the region under co-atom W. (Contributed by NM, 24-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )
Theorem	dib11N 34653	The isomorphism B for a lattice K is one-to-one in the region under co-atom W. (Contributed by NM, 24-Feb-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( I ` X ) = ( I ` Y ) <-> X = Y ) )
Theorem	dibf11N 34654	The partial isomorphism A for a lattice K is a one-to-one function. Part of Lemma M of [Crawley] p. 120 line 27. (Contributed by NM, 4-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I )
Theorem	dibclN 34655	Closure of partial isomorphism B for a lattice K. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) e. ran I )
Theorem	dibvalrel 34656	The value of partial isomorphism B is a relation. (Contributed by NM, 8-Mar-2014.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> Rel ( I ` X ) )
Theorem	dib0 34657	The value of partial isomorphism B at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 27-Mar-2014.)
|- .0. = ( 0. ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- O = ( 0g ` U )   =>    |- ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = { O } )
Theorem	dib1dim 34658*	Two expressions for the 1-dimensional subspaces of vector space H. (Contributed by NM, 24-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g e. ( T X. E ) | E. s e. E g = <. ( s ` F ) , O >. } )
Theorem	dibglbN 34659*	Partial isomorphism B of a lattice glb. (Contributed by NM, 9-Mar-2014.) (New usage is discouraged.)
|- G = ( glb ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) )
Theorem	dibintclN 34660	The intersection of partial isomorphism B closed subspaces is a closed subspace. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^| S e. ran I )
Theorem	dib1dim2 34661*	Two expressions for a 1-dimensional subspace of vector space H (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 24-Feb-2014.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- N = ( LSpan ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( N ` { <. F , O >. } ) )
Theorem	dibss 34662	The partial isomorphism B maps to a set of vectors in full vector space H. (Contributed by NM, 1-Jan-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) C_ V )
Theorem	diblss 34663	The value of partial isomorphism B is a subspace of partial vector space H. TODO: use dib* specific theorems instead of dia* ones to shorten proof? (Contributed by NM, 11-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- S = ( LSubSp ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) e. S )
Theorem	diblsmopel 34664*	Membership in subspace sum for partial isomorphism B. (Contributed by NM, 21-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- O = ( f e. T |-> ( _I |` B ) )   &    |- V = ( ( DVecA ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` V )   &    |- .+b = ( LSSum ` U )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( X e. B /\ X .<_ W ) )   &    |- ( ph -> ( Y e. B /\ Y .<_ W ) )   =>    |- ( ph -> ( <. F , S >. e. ( ( I ` X ) .+b ( I ` Y ) ) <-> ( F e. ( ( J ` X ) .(+) ( J ` Y ) ) /\ S = O ) ) )
Syntax	cdic 34665	Extend class notation with isomorphism C.
class DIsoC
Definition	df-dic 34666*	Isomorphism C has domain of lattice atoms that are not less than or equal to the fiducial co-atom w. The value is a one-dimensional subspace generated by the pair consisting of the iota_ vector below and the endomorphism ring unit. Definition of phi(q) in [Crawley] p. 121. Note that we use the fixed atom ( ( oc k ) w ) to represent the p in their "Choose an atom p..." on line 21. (Contributed by NM, 15-Dec-2013.)
|- DIsoC = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( q e. { r e. ( Atoms ` k ) | -. r ( le ` k ) w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) ) } ) ) )
Theorem	dicffval 34667*	The partial isomorphism C for a lattice K. (Contributed by NM, 15-Dec-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( K e. V -> ( DIsoC ` K ) = ( w e. H |-> ( q e. { r e. A | -. r .<_ w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` w ) ) } ) ) )
Theorem	dicfval 34668*	The partial isomorphism C for a lattice K. (Contributed by NM, 15-Dec-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> I = ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } ) )
Theorem	dicval 34669*	The partial isomorphism C for a lattice K. (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) } )
Theorem	dicopelval 34670*	Membership in value of the partial isomorphism C for a lattice K. (Contributed by NM, 15-Feb-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   &    |- F e. _V   &    |- S e. _V   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. F , S >. e. ( I ` Q ) <-> ( F = ( S ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ S e. E ) ) )
Theorem	dicelvalN 34671*	Membership in value of the partial isomorphism C for a lattice K. (Contributed by NM, 25-Feb-2014.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Y e. ( I ` Q ) <-> ( Y e. ( _V X. _V ) /\ ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ ( 2nd ` Y ) e. E ) ) ) )
Theorem	dicval2 34672*	The partial isomorphism C for a lattice K. (Contributed by NM, 20-Feb-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   &    |- G = ( iota_ g e. T ( g ` P ) = Q )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { <. f , s >. | ( f = ( s ` G ) /\ s e. E ) } )
Theorem	dicelval3 34673*	Member of the partial isomorphism C. (Contributed by NM, 26-Feb-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   &    |- G = ( iota_ g e. T ( g ` P ) = Q )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Y e. ( I ` Q ) <-> E. s e. E Y = <. ( s ` G ) , s >. ) )
Theorem	dicopelval2 34674*	Membership in value of the partial isomorphism C for a lattice K. (Contributed by NM, 20-Feb-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   &    |- G = ( iota_ g e. T ( g ` P ) = Q )   &    |- F e. _V   &    |- S e. _V   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. F , S >. e. ( I ` Q ) <-> ( F = ( S ` G ) /\ S e. E ) ) )
Theorem	dicelval2N 34675*	Membership in value of the partial isomorphism C for a lattice K. (Contributed by NM, 25-Feb-2014.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   &    |- G = ( iota_ g e. T ( g ` P ) = Q )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Y e. ( I ` Q ) <-> ( Y e. ( _V X. _V ) /\ ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` G ) /\ ( 2nd ` Y ) e. E ) ) ) )
Theorem	dicfnN 34676*	Functionality and domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoC ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> I Fn { p e. A | -. p .<_ W } )
Theorem	dicdmN 34677*	Domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoC ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> dom I = { p e. A | -. p .<_ W } )
Theorem	dicvalrelN 34678	The value of partial isomorphism C is a relation. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoC ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> Rel ( I ` X ) )
Theorem	dicssdvh 34679	The partial isomorphism C maps to a set of vectors in full vector space H. (Contributed by NM, 19-Jan-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ V )
Theorem	dicelval1sta 34680*	Membership in value of the partial isomorphism C for a lattice K. (Contributed by NM, 16-Feb-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) )
Theorem	dicelval1stN 34681	Membership in value of the partial isomorphism C for a lattice K. (Contributed by NM, 16-Feb-2014.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 1st ` Y ) e. T )
Theorem	dicelval2nd 34682	Membership in value of the partial isomorphism C for a lattice K. (Contributed by NM, 16-Feb-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 2nd ` Y ) e. E )
Theorem	dicvaddcl 34683	Membership in value of the partial isomorphism C is closed under vector sum. (Contributed by NM, 16-Feb-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   &    |- .+ = ( +g ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( X .+ Y ) e. ( I ` Q ) )
Theorem	dicvscacl 34684	Membership in value of the partial isomorphism C is closed under scalar product. (Contributed by NM, 16-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   &    |- .x. = ( .s ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( X .x. Y ) e. ( I ` Q ) )
Theorem	dicn0 34685	The value of the partial isomorphism C is not empty. (Contributed by NM, 15-Feb-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoC ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) =/= (/) )
Theorem	diclss 34686	The value of partial isomorphism C is a subspace of partial vector space H. (Contributed by NM, 16-Feb-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   &    |- S = ( LSubSp ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) e. S )
Theorem	diclspsn 34687*	The value of isomorphism C is spanned by vector F. Part of proof of Lemma N of [Crawley] p. 121 line 29. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- N = ( LSpan ` U )   &    |- F = ( iota_ f e. T ( f ` P ) = Q )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( N ` { <. F , ( _I |` T ) >. } ) )
Theorem	cdlemn2 34688*	Part of proof of Lemma N of [Crawley] p. 121 line 30. (Contributed by NM, 21-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- F = ( iota_ h e. T ( h ` Q ) = S )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( R ` F ) .<_ X )
Theorem	cdlemn2a 34689*	Part of proof of Lemma N of [Crawley] p. 121. (Contributed by NM, 24-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- O = ( f e. T |-> ( _I |` B ) )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- N = ( LSpan ` U )   &    |- F = ( iota_ h e. T ( h ` Q ) = S )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ S .<_ ( Q .\/ X ) ) -> ( N ` { <. F , O >. } ) C_ ( I ` X ) )
Theorem	cdlemn3 34690*	Part of proof of Lemma N of [Crawley] p. 121 line 31. (Contributed by NM, 21-Feb-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- F = ( iota_ h e. T ( h ` P ) = Q )   &    |- G = ( iota_ h e. T ( h ` P ) = R )   &    |- J = ( iota_ h e. T ( h ` Q ) = R )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( J o. F ) = G )
Theorem	cdlemn4 34691*	Part of proof of Lemma N of [Crawley] p. 121 line 31. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = ( iota_ h e. T ( h ` P ) = Q )   &    |- G = ( iota_ h e. T ( h ` P ) = R )   &    |- J = ( iota_ h e. T ( h ` Q ) = R )   &    |- .+ = ( +g ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> <. G , ( _I |` T ) >. = ( <. F , ( _I |` T ) >. .+ <. J , O >. ) )
Theorem	cdlemn4a 34692*	Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 24-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = ( iota_ h e. T ( h ` P ) = Q )   &    |- G = ( iota_ h e. T ( h ` P ) = R )   &    |- J = ( iota_ h e. T ( h ` Q ) = R )   &    |- N = ( LSpan ` U )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( N ` { <. G , ( _I |` T ) >. } ) C_ ( ( N ` { <. F , ( _I |` T ) >. } ) .(+) ( N ` { <. J , O >. } ) ) )
Theorem	cdlemn5pre 34693*	Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- P = ( ( oc ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- N = ( LSpan ` U )   &    |- F = ( iota_ h e. T ( h ` P ) = Q )   &    |- G = ( iota_ h e. T ( h ` P ) = R )   &    |- M = ( iota_ h e. T ( h ` Q ) = R )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ R .<_ ( Q .\/ X ) ) -> ( J ` R ) C_ ( ( J ` Q ) .(+) ( I ` X ) ) )
Theorem	cdlemn5 34694	Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ R .<_ ( Q .\/ X ) ) -> ( J ` R ) C_ ( ( J ` Q ) .(+) ( I ` X ) ) )
Theorem	cdlemn6 34695*	Part of proof of Lemma N of [Crawley] p. 121 line 35. (Contributed by NM, 26-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = ( iota_ h e. T ( h ` P ) = Q )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T ) ) -> ( <. ( s ` F ) , s >. .+ <. g , O >. ) = <. ( ( s ` F ) o. g ) , s >. )
Theorem	cdlemn7 34696*	Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = ( iota_ h e. T ( h ` P ) = Q )   &    |- G = ( iota_ h e. T ( h ` P ) = R )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> ( G = ( ( s ` F ) o. g ) /\ ( _I |` T ) = s ) )
Theorem	cdlemn8 34697*	Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = ( iota_ h e. T ( h ` P ) = Q )   &    |- G = ( iota_ h e. T ( h ` P ) = R )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> g = ( G o. `' F ) )
Theorem	cdlemn9 34698*	Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- F = ( iota_ h e. T ( h ` P ) = Q )   &    |- G = ( iota_ h e. T ( h ` P ) = R )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> ( g ` Q ) = R )
Theorem	cdlemn10 34699	Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( g e. T /\ ( g ` Q ) = S /\ ( R ` g ) .<_ X ) ) -> S .<_ ( Q .\/ X ) )
Theorem	cdlemn11a 34700*	Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- .(+) = ( LSSum ` U )   &    |- F = ( iota_ h e. T ( h ` P ) = Q )   &    |- G = ( iota_ h e. T ( h ` P ) = N )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( J ` N ) C_ ( ( J ` Q ) .(+) ( I ` X ) ) ) -> <. G , ( _I |` T ) >. e. ( J ` N ) )