P. 359 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35801-35900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	diarnN 35801*	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 35802*	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 35707 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 35803	Extend class notation with subspace join for DVecA partial vector space.
class vA
Definition	df-djaN 35804*	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 35805*	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 35806*	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 35807	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 35808	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 35809	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 35810	Extend class notation with isomorphism B.
class DIsoB
Definition	df-dib 35811*	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 35812*	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 35813*	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 35814*	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 35815*	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 35816*	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 35817*	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 35818*	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 35819*	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 35820*	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 35821	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 35822	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 35823	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 35824*	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 35825	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 35826	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 35827	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 35828*	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 35829*	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 35830	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 35831	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 35832	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 35833	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 35834	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 35835	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 35836	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 35837*	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 35838*	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 35839	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 35840*	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 35841	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 35842	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 35843*	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 35844	Extend class notation with isomorphism C.
class DIsoC
Definition	df-dic 35845*	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 35846*	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 35847*	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 35848*	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 35849*	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 35850*	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 35851*	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 35852*	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 35853*	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 35854*	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 35855*	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 35856*	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 35857	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 35858	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 35859*	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 35860	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 35861	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 35862	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 35863	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 35864	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 35865	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 35866*	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 35867*	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 35868*	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 35869*	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 35870*	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 35871*	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 35872*	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 35873	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 35874*	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 35875*	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 35876*	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 35877*	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 35878	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 35879*	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 35880*	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 35881*	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 35882*	Part of proof of Lemma N of [Crawley] p. 121 line 37. TODO: combine cdlemn11a 35879, cdlemn11b 35880, cdlemn11c 35881, 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 35883	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 35884	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 35885*	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 35886*	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 35887*	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 35888	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 35889	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 35890	Part of proof after Lemma N of [Crawley] p. 122. Forward ordering property. TODO: change ( Q .\/ ( X ./\ W ) ) = X to Q .<_ X using lhpmcvr3 34696, 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 35891	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 35892	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 35893*	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 35894*	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 35895*	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 35896*	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 35897*	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 35898*	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 35899	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 35900	Extend class notation with isomorphism H.
class DIsoH