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	djaffvalN 34701*	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 34702*	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 34703	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 34704	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 34705	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 34706	Extend class notation with isomorphism B.
class DIsoB
Definition	df-dib 34707*	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 34708*	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 34709*	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 34710*	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 34711*	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 34712*	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 34713*	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 34714*	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 34715*	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 34716*	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 34717	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 34718	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 34719	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 34720*	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 34721	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 34722	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 34723	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 34724*	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 34725*	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 34726	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 34727	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 34728	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 34729	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 34730	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 34731	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 34732	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 34733*	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 34734*	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 34735	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 34736*	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 34737	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 34738	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 34739*	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 34740	Extend class notation with isomorphism C.
class DIsoC
Definition	df-dic 34741*	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 34742*	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 34743*	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 34744*	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 34745*	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 34746*	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 34747*	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 34748*	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 34749*	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 34750*	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 34751*	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 34752*	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 34753	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 34754	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 34755*	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 34756	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 34757	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 34758	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 34759	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 34760	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 34761	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 34762*	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 34763*	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 34764*	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 34765*	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 34766*	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 34767*	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 34768*	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 34769	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 34770*	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 34771*	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 34772*	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 34773*	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 34774	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 34775*	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 ) )
Theorem	cdlemn11b 34776*	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 ` Q ) .(+) ( I ` X ) ) )
Theorem	cdlemn11c 34777*	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 ) ) ) -> E. y e. ( J ` Q ) E. z e. ( I ` X ) <. G , ( _I |` T ) >. = ( y .+ z ) )
Theorem	cdlemn11pre 34778*	Part of proof of Lemma N of [Crawley] p. 121 line 37. TODO: combine cdlemn11a 34775, cdlemn11b 34776, cdlemn11c 34777, cdlemn11pre into one? (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 ) ) ) -> N .<_ ( Q .\/ X ) )
Theorem	cdlemn11 34779	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 )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ ( J ` R ) C_ ( ( J ` Q ) .(+) ( I ` X ) ) ) -> R .<_ ( Q .\/ X ) )
Theorem	cdlemn 34780	Lemma N of [Crawley] p. 121 line 27. (Contributed by NM, 27-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( ( 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	dihordlem6 34781*	Part of proof of Lemma N of [Crawley] p. 122 line 35. (Contributed by NM, 3-Mar-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 )   &    |- 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 ) ) -> ( <. ( s ` G ) , s >. .+ <. g , O >. ) = <. ( ( s ` G ) o. g ) , s >. )
Theorem	dihordlem7 34782*	Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-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 )   &    |- 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 /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> ( f = ( ( s ` G ) o. g ) /\ O = s ) )
Theorem	dihordlem7b 34783*	Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-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 )   &    |- 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 /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> ( f = g /\ O = s ) )
Theorem	dihjustlem 34784	Part of proof after Lemma N of [Crawley] p. 122 line 4, "the definition of phi(x) is independent of the atom q." (Contributed by NM, 2-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ X e. B ) /\ ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) -> ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` R ) .(+) ( I ` ( X ./\ W ) ) ) )
Theorem	dihjust 34785	Part of proof after Lemma N of [Crawley] p. 122 line 4, "the definition of phi(x) is independent of the atom q." (Contributed by NM, 2-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ X e. B ) /\ ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) -> ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) = ( ( J ` R ) .(+) ( I ` ( X ./\ W ) ) ) )
Theorem	dihord1 34786	Part of proof after Lemma N of [Crawley] p. 122. Forward ordering property. TODO: change ( Q .\/ ( X ./\ W ) ) = X to Q .<_ X using lhpmcvr3 33590, here and all theorems below. (Contributed by NM, 2-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( Q .\/ ( X ./\ W ) ) = X /\ ( R .\/ ( Y ./\ W ) ) = Y /\ X .<_ Y ) ) -> ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` R ) .(+) ( I ` ( Y ./\ W ) ) ) )
Theorem	dihord2a 34787	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( Q .\/ ( X ./\ W ) ) = X /\ ( R .\/ ( Y ./\ W ) ) = Y /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` R ) .(+) ( I ` ( Y ./\ W ) ) ) ) ) -> Q .<_ ( R .\/ ( Y ./\ W ) ) )
Theorem	dihord2b 34788	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` R ) .(+) ( I ` ( Y ./\ W ) ) ) ) -> ( I ` ( X ./\ W ) ) C_ ( ( J ` R ) .(+) ( I ` ( Y ./\ W ) ) ) )
Theorem	dihord2cN 34789*	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. TODO: needed? shorten other proof with it? (Contributed by NM, 3-Mar-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> <. f , O >. e. ( I ` ( X ./\ W ) ) )
Theorem	dihord11b 34790*	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- P = ( ( oc ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- 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 /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> <. f , O >. e. ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) )
Theorem	dihord10 34791*	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- P = ( ( oc ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- G = ( iota_ h e. T ( h ` P ) = N )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ ( ( s e. E /\ g e. T ) /\ ( R ` g ) .<_ ( Y ./\ W ) /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> ( R ` f ) .<_ ( Y ./\ W ) )
Theorem	dihord11c 34792*	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- P = ( ( oc ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- 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 /\ Y e. B ) /\ ( ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) /\ f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> E. y e. ( J ` N ) E. z e. ( I ` ( Y ./\ W ) ) <. f , O >. = ( y .+ z ) )
Theorem	dihord2pre 34793*	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- P = ( ( oc ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- 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 /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) -> ( X ./\ W ) .<_ ( Y ./\ W ) )
Theorem	dihord2pre2 34794*	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 4-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- P = ( ( oc ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- 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 /\ Y e. B ) /\ ( ( Q .\/ ( X ./\ W ) ) = X /\ ( N .\/ ( Y ./\ W ) ) = Y /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) ) -> ( Q .\/ ( X ./\ W ) ) .<_ ( N .\/ ( Y ./\ W ) ) )
Theorem	dihord2 34795	Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. TODO: do we need -. X .<_ W and -. Y .<_ W? (Contributed by NM, 4-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   &    |- J = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( Q .\/ ( X ./\ W ) ) = X /\ ( N .\/ ( Y ./\ W ) ) = Y /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) ) -> X .<_ Y )
Syntax	cdih 34796	Extend class notation with isomorphism H.
class DIsoH
Definition	df-dih 34797*	Define isomorphism H. (Contributed by NM, 28-Jan-2014.)
|- DIsoH = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ( Base ` k ) |-> if ( x ( le ` k ) w , ( ( ( DIsoB ` k ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) ) ) ) ) )
Theorem	dihffval 34798*	The isomorphism H for a lattice K. Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 28-Jan-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( K e. V -> ( DIsoH ` K ) = ( w e. H |-> ( x e. B |-> if ( x .<_ w , ( ( ( DIsoB ` K ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) A. q e. A ( ( -. q .<_ w /\ ( q .\/ ( x ./\ w ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) ) ) ) ) ) )
Theorem	dihfval 34799*	Isomorphism H for a lattice K. Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 28-Jan-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoH ` K ) ` W )   &    |- D = ( ( DIsoB ` K ) ` W )   &    |- C = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( K e. V /\ W e. H ) -> I = ( x e. B |-> if ( x .<_ W , ( D ` x ) , ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( x ./\ W ) ) = x ) -> u = ( ( C ` q ) .(+) ( D ` ( x ./\ W ) ) ) ) ) ) ) )
Theorem	dihval 34800*	Value of isomorphism H for a lattice K. Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 3-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoH ` K ) ` W )   &    |- D = ( ( DIsoB ` K ) ` W )   &    |- C = ( ( DIsoC ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( ( K e. V /\ W e. H ) /\ X e. B ) -> ( I ` X ) = if ( X .<_ W , ( D ` X ) , ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) ) )