P. 358 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35701-35800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dva0g 35701	The zero vector of partial vector space A. (Contributed by NM, 9-Sep-2014.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- U = ( ( DVecA ` K ) ` W )   &    |- .0. = ( 0g ` U )   =>    |- ( ( K e. HL /\ W e. H ) -> .0. = ( _I |` B ) )
Syntax	cdia 35702	Extend class notation with partial isomorphism A.
class DIsoA
Definition	df-disoa 35703*	Define partial isomorphism A. (Contributed by NM, 15-Oct-2013.)
|- DIsoA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. { y e. ( Base ` k ) | y ( le ` k ) w } |-> { f e. ( ( LTrn ` k ) ` w ) | ( ( ( trL ` k ) ` w ) ` f ) ( le ` k ) x } ) ) )
Theorem	diaffval 35704*	The partial isomorphism A for a lattice K. (Contributed by NM, 15-Oct-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   =>    |- ( K e. V -> ( DIsoA ` K ) = ( w e. H |-> ( x e. { y e. B | y .<_ w } |-> { f e. ( ( LTrn ` K ) ` w ) | ( ( ( trL ` K ) ` w ) ` f ) .<_ x } ) ) )
Theorem	diafval 35705*	The partial isomorphism A for a lattice K. (Contributed by NM, 15-Oct-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> I = ( x e. { y e. B | y .<_ W } |-> { f e. T | ( R ` f ) .<_ x } ) )
Theorem	diaval 35706*	The partial isomorphism A for a lattice K. Definition of isomorphism map in [Crawley] p. 120 line 24. (Contributed by NM, 15-Oct-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = { f e. T | ( R ` f ) .<_ X } )
Theorem	diaelval 35707	Member of the partial isomorphism A for a lattice K. (Contributed by NM, 3-Dec-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( F e. ( I ` X ) <-> ( F e. T /\ ( R ` F ) .<_ X ) ) )
Theorem	diafn 35708*	Functionality and domain of the partial isomorphism A. (Contributed by NM, 26-Nov-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> I Fn { x e. B | x .<_ W } )
Theorem	diadm 35709*	Domain of the partial isomorphism A. (Contributed by NM, 3-Dec-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> dom I = { x e. B | x .<_ W } )
Theorem	diaeldm 35710	Member of domain of the partial isomorphism A. (Contributed by NM, 4-Dec-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> ( X e. dom I <-> ( X e. B /\ X .<_ W ) ) )
Theorem	diadmclN 35711	A member of domain of the partial isomorphism A is a lattice element. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> X e. B )
Theorem	diadmleN 35712	A member of domain of the partial isomorphism A is under the fiducial hyperplane. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> X .<_ W )
Theorem	dian0 35713	The value of the partial isomorphism A is not empty. (Contributed by NM, 17-Jan-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) =/= (/) )
Theorem	dia0eldmN 35714	The lattice zero belongs to the domain of partial isomorphism A. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
|- .0. = ( 0. ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> .0. e. dom I )
Theorem	dia1eldmN 35715	The fiducial hyperplane (the largest allowed lattice element) belongs to the domain of partial isomorphism A. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> W e. dom I )
Theorem	diass 35716	The value of the partial isomorphism A is a set of translations i.e. a set of vectors. (Contributed by NM, 26-Nov-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) C_ T )
Theorem	diael 35717	A member of the value of the partial isomorphism A is a translation i.e. a vector. (Contributed by NM, 17-Jan-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ F e. ( I ` X ) ) -> F e. T )
Theorem	diatrl 35718	Trace of a member of the partial isomorphism A. (Contributed by NM, 17-Jan-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ F e. ( I ` X ) ) -> ( R ` F ) .<_ X )
Theorem	diaelrnN 35719	Any value of the partial isomorphism A is a set of translations i.e. a set of vectors. (Contributed by NM, 26-Nov-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ S e. ran I ) -> S C_ T )
Theorem	dialss 35720	The value of partial isomorphism A is a subspace of partial vector space A. Part of Lemma M of [Crawley] p. 120 line 26. (Contributed by NM, 17-Jan-2014.) (Revised by Mario Carneiro, 23-Jun-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( DVecA ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- S = ( LSubSp ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) e. S )
Theorem	diaord 35721	The partial isomorphism A for a lattice K is order-preserving in the region under co-atom W. Part of Lemma M of [Crawley] p. 120 line 28. (Contributed by NM, 26-Nov-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` 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	dia11N 35722	The partial isomorphism A for a lattice K is one-to-one in the region under co-atom W. Part of Lemma M of [Crawley] p. 120 line 28. (Contributed by NM, 25-Nov-2013.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` 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	diaf11N 35723	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 = ( ( DIsoA ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I )
Theorem	diaclN 35724	Closure of partial isomorphism A for a lattice K. (Contributed by NM, 4-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) e. ran I )
Theorem	diacnvclN 35725	Closure of partial isomorphism A converse. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. dom I )
Theorem	dia0 35726	The value of the partial isomorphism A at the lattice zero is the singleton of the identity translation i.e. the zero subspace. (Contributed by NM, 26-Nov-2013.)
|- B = ( Base ` K )   &    |- .0. = ( 0. ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = { ( _I |` B ) } )
Theorem	dia1N 35727	The value of the partial isomorphism A at the fiducial co-atom is the set of all translations i.e. the entire vector space. (Contributed by NM, 26-Nov-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> ( I ` W ) = T )
Theorem	dia1elN 35728	The largest subspace in the range of partial isomorphism A. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> T e. ran I )
Theorem	diaglbN 35729*	Partial isomorphism A of a lattice glb. (Contributed by NM, 3-Dec-2013.) (New usage is discouraged.)
|- G = ( glb ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) )
Theorem	diameetN 35730	Partial isomorphism A of a lattice meet. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
|- ./\ = ( meet ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` ( X ./\ Y ) ) = ( ( I ` X ) i^i ( I ` Y ) ) )
Theorem	diainN 35731	Inverse partial isomorphism A of an intersection. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- ./\ = ( meet ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> ( X i^i Y ) = ( I ` ( ( `' I ` X ) ./\ ( `' I ` Y ) ) ) )
Theorem	diaintclN 35732	The intersection of partial isomorphism A closed subspaces is a closed subspace. (Contributed by NM, 3-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^| S e. ran I )
Theorem	diasslssN 35733	The partial isomorphism A maps to subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecA ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- S = ( LSubSp ` U )   =>    |- ( ( K e. HL /\ W e. H ) -> ran I C_ S )
Theorem	diassdvaN 35734	The partial isomorphism A maps to a set of vectors in partial vector space A. (Contributed by NM, 1-Jan-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- U = ( ( DVecA ` K ) ` W )   &    |- V = ( Base ` U )   =>    |- ( ( ( K e. Y /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) C_ V )
Theorem	dia1dim 35735*	Two expressions for the 1-dimensional subspaces of partial vector space A (when F is a nonzero vector i.e. non-identity translation). Remark after Lemma L in [Crawley] p. 120 line 21. (Contributed by NM, 15-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g | E. s e. E g = ( s ` F ) } )
Theorem	dia1dim2 35736	Two expressions for a 1-dimensional subspace of partial vector space A (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 15-Jan-2014.) (Revised by Mario Carneiro, 22-Jun-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- U = ( ( DVecA ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- N = ( LSpan ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( N ` { F } ) )
Theorem	dia1dimid 35737	A vector (translation) belongs to the 1-dim subspace it generates. (Contributed by NM, 8-Sep-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. ( I ` ( R ` F ) ) )
Theorem	dia2dimlem1 35738	Lemma for dia2dim 35751. Show properties of the auxiliary atom Q. Part of proof of Lemma M in [Crawley] p. 121 line 3. (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   &    |- ( ph -> ( P e. A /\ -. P .<_ W ) )   &    |- ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )   &    |- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )   &    |- ( ph -> U =/= V )   &    |- ( ph -> ( R ` F ) =/= U )   =>    |- ( ph -> ( Q e. A /\ -. Q .<_ W ) )
Theorem	dia2dimlem2 35739	Lemma for dia2dim 35751. Define a translation G whose trace is atom U. Part of proof of Lemma M in [Crawley] p. 121 line 4. (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   &    |- ( ph -> ( P e. A /\ -. P .<_ W ) )   &    |- ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )   &    |- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )   &    |- ( ph -> ( R ` F ) =/= V )   &    |- ( ph -> G e. T )   &    |- ( ph -> ( G ` P ) = Q )   =>    |- ( ph -> ( R ` G ) = U )
Theorem	dia2dimlem3 35740	Lemma for dia2dim 35751. Define a translation D whose trace is atom V. Part of proof of Lemma M in [Crawley] p. 121 line 5. (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   &    |- ( ph -> ( P e. A /\ -. P .<_ W ) )   &    |- ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )   &    |- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )   &    |- ( ph -> U =/= V )   &    |- ( ph -> ( R ` F ) =/= U )   &    |- ( ph -> ( R ` F ) =/= V )   &    |- ( ph -> D e. T )   &    |- ( ph -> ( D ` Q ) = ( F ` P ) )   =>    |- ( ph -> ( R ` D ) = V )
Theorem	dia2dimlem4 35741	Lemma for dia2dim 35751. Show that the composition (sum) of translations (vectors) G and D equals F. Part of proof of Lemma M in [Crawley] p. 121 line 5. (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( P e. A /\ -. P .<_ W ) )   &    |- ( ph -> F e. T )   &    |- ( ph -> G e. T )   &    |- ( ph -> ( G ` P ) = Q )   &    |- ( ph -> D e. T )   &    |- ( ph -> ( D ` Q ) = ( F ` P ) )   =>    |- ( ph -> ( D o. G ) = F )
Theorem	dia2dimlem5 35742	Lemma for dia2dim 35751. The sum of vectors G and D belongs to the sum of the subspaces generated by them. Thus, F = ( G o. D ) belongs to the subspace sum. Part of proof of Lemma M in [Crawley] p. 121 line 5. (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- Y = ( ( DVecA ` K ) ` W )   &    |- S = ( LSubSp ` Y )   &    |- .(+) = ( LSSum ` Y )   &    |- N = ( LSpan ` Y )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   &    |- ( ph -> ( P e. A /\ -. P .<_ W ) )   &    |- ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )   &    |- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )   &    |- ( ph -> U =/= V )   &    |- ( ph -> ( R ` F ) =/= U )   &    |- ( ph -> ( R ` F ) =/= V )   &    |- ( ph -> G e. T )   &    |- ( ph -> ( G ` P ) = Q )   &    |- ( ph -> D e. T )   &    |- ( ph -> ( D ` Q ) = ( F ` P ) )   =>    |- ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )
Theorem	dia2dimlem6 35743	Lemma for dia2dim 35751. Eliminate auxiliary translations G and D. (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- Y = ( ( DVecA ` K ) ` W )   &    |- S = ( LSubSp ` Y )   &    |- .(+) = ( LSSum ` Y )   &    |- N = ( LSpan ` Y )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   &    |- ( ph -> ( P e. A /\ -. P .<_ W ) )   &    |- ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )   &    |- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )   &    |- ( ph -> U =/= V )   &    |- ( ph -> ( R ` F ) =/= U )   &    |- ( ph -> ( R ` F ) =/= V )   =>    |- ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )
Theorem	dia2dimlem7 35744	Lemma for dia2dim 35751. Eliminate ( F ` P ) =/= P condition. (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- Y = ( ( DVecA ` K ) ` W )   &    |- S = ( LSubSp ` Y )   &    |- .(+) = ( LSSum ` Y )   &    |- N = ( LSpan ` Y )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   &    |- ( ph -> ( P e. A /\ -. P .<_ W ) )   &    |- ( ph -> F e. T )   &    |- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )   &    |- ( ph -> U =/= V )   &    |- ( ph -> ( R ` F ) =/= U )   &    |- ( ph -> ( R ` F ) =/= V )   =>    |- ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )
Theorem	dia2dimlem8 35745	Lemma for dia2dim 35751. Eliminate no-longer used auxiliary atoms P and Q. (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- Y = ( ( DVecA ` K ) ` W )   &    |- S = ( LSubSp ` Y )   &    |- .(+) = ( LSSum ` Y )   &    |- N = ( LSpan ` Y )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   &    |- ( ph -> F e. T )   &    |- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )   &    |- ( ph -> U =/= V )   &    |- ( ph -> ( R ` F ) =/= U )   &    |- ( ph -> ( R ` F ) =/= V )   =>    |- ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )
Theorem	dia2dimlem9 35746	Lemma for dia2dim 35751. Eliminate ( R ` F ) =/= U, V conditions. (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- Y = ( ( DVecA ` K ) ` W )   &    |- S = ( LSubSp ` Y )   &    |- .(+) = ( LSSum ` Y )   &    |- N = ( LSpan ` Y )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   &    |- ( ph -> F e. T )   &    |- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )   &    |- ( ph -> U =/= V )   =>    |- ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )
Theorem	dia2dimlem10 35747	Lemma for dia2dim 35751. Convert membership in closed subspace ( I ` ( U .\/ V ) ) to a lattice ordering. (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- Y = ( ( DVecA ` K ) ` W )   &    |- S = ( LSubSp ` Y )   &    |- N = ( LSpan ` Y )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   &    |- ( ph -> F e. T )   &    |- ( ph -> F e. ( I ` ( U .\/ V ) ) )   =>    |- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )
Theorem	dia2dimlem11 35748	Lemma for dia2dim 35751. Convert ordering hypothesis on R ` F to subspace membership F e. ( I ` ( U .\/ V ) ). (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- Y = ( ( DVecA ` K ) ` W )   &    |- S = ( LSubSp ` Y )   &    |- .(+) = ( LSSum ` Y )   &    |- N = ( LSpan ` Y )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   &    |- ( ph -> F e. T )   &    |- ( ph -> U =/= V )   &    |- ( ph -> F e. ( I ` ( U .\/ V ) ) )   =>    |- ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )
Theorem	dia2dimlem12 35749	Lemma for dia2dim 35751. Obtain subset relation. (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- Y = ( ( DVecA ` K ) ` W )   &    |- S = ( LSubSp ` Y )   &    |- .(+) = ( LSSum ` Y )   &    |- N = ( LSpan ` Y )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   &    |- ( ph -> U =/= V )   =>    |- ( ph -> ( I ` ( U .\/ V ) ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )
Theorem	dia2dimlem13 35750	Lemma for dia2dim 35751. Eliminate U =/= V condition. (Contributed by NM, 8-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- Y = ( ( DVecA ` K ) ` W )   &    |- S = ( LSubSp ` Y )   &    |- .(+) = ( LSSum ` Y )   &    |- N = ( LSpan ` Y )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   =>    |- ( ph -> ( I ` ( U .\/ V ) ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )
Theorem	dia2dim 35751	A two-dimensional subspace of partial vector space A is closed, or equivalently, the isomorphism of a join of two atoms is a subset of the subspace sum of the isomorphisms of each atom (and thus they are equal, as shown later for the full vector space H). (Contributed by NM, 9-Sep-2014.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- Y = ( ( DVecA ` K ) ` W )   &    |- .(+) = ( LSSum ` Y )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( U e. A /\ U .<_ W ) )   &    |- ( ph -> ( V e. A /\ V .<_ W ) )   =>    |- ( ph -> ( I ` ( U .\/ V ) ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )
Syntax	cdvh 35752	Extend class notation with constructed full vector space H.
class DVecH
Definition	df-dvech 35753*	Define constructed full vector space H. (Contributed by NM, 17-Oct-2013.)
|- DVecH = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( { <. ( Base ` ndx ) , ( ( ( LTrn ` k ) ` w ) X. ( ( TEndo ` k ) ` w ) ) >. , <. ( +g ` ndx ) , ( f e. ( ( ( LTrn ` k ) ` w ) X. ( ( TEndo ` k ) ` w ) ) , g e. ( ( ( LTrn ` k ) ` w ) X. ( ( TEndo ` k ) ` w ) ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` k ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. (Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( ( LTrn ` k ) ` w ) X. ( ( TEndo ` k ) ` w ) ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) )
Theorem	dvhfset 35754*	The constructed full vector space H for a lattice K. (Contributed by NM, 17-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
|- H = ( LHyp ` K )   =>    |- ( K e. V -> ( DVecH ` K ) = ( w e. H |-> ( { <. ( Base ` ndx ) , ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) >. , <. ( +g ` ndx ) , ( f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) , g e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. (Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) )
Theorem	dvhset 35755*	The constructed full vector space H for a lattice K. (Contributed by NM, 17-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRing ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   =>    |- ( ( K e. X /\ W e. H ) -> U = ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. (Scalar ` ndx ) , D >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) )
Theorem	dvhsca 35756	The ring of scalars of the constructed full vector space H. (Contributed by NM, 22-Jun-2014.)
|- H = ( LHyp ` K )   &    |- D = ( ( EDRing ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   =>    |- ( ( K e. X /\ W e. H ) -> F = D )
Theorem	dvhbase 35757	The ring base set of the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
|- H = ( LHyp ` K )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- C = ( Base ` F )   =>    |- ( ( K e. X /\ W e. H ) -> C = E )
Theorem	dvhfplusr 35758*	Ring addition operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- .+ = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   &    |- .+b = ( +g ` F )   =>    |- ( ( K e. V /\ W e. H ) -> .+b = .+ )
Theorem	dvhfmulr 35759*	Ring multiplication operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- .x. = ( .r ` F )   =>    |- ( ( K e. V /\ W e. H ) -> .x. = ( s e. E , t e. E |-> ( s o. t ) ) )
Theorem	dvhmulr 35760	Ring multiplication operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- .x. = ( .r ` F )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ S e. E ) ) -> ( R .x. S ) = ( R o. S ) )
Theorem	dvhvbase 35761	The vectors (vector base set) of the constructed full vector space H are all translations (for a fiducial co-atom W). (Contributed by NM, 2-Nov-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   =>    |- ( ( K e. X /\ W e. H ) -> V = ( T X. E ) )
Theorem	dvhelvbasei 35762	Vector membership in the constructed full vector space H. (Contributed by NM, 20-Feb-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   =>    |- ( ( ( K e. X /\ W e. H ) /\ ( F e. T /\ S e. E ) ) -> <. F , S >. e. V )
Theorem	dvhvaddcbv 35763*	Change bound variables to isolate them later. (Contributed by NM, 3-Nov-2013.)
|- .+ = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. )   =>    |- .+ = ( h e. ( T X. E ) , i e. ( T X. E ) |-> <. ( ( 1st ` h ) o. ( 1st ` i ) ) , ( ( 2nd ` h ) .+^ ( 2nd ` i ) ) >. )
Theorem	dvhvaddval 35764*	The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.)
|- .+ = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. )   =>    |- ( ( F e. ( T X. E ) /\ G e. ( T X. E ) ) -> ( F .+ G ) = <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. )
Theorem	dvhfvadd 35765*	The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (Scalar ` U )   &    |- .+^ = ( +g ` D )   &    |- .+b = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. )   &    |- .+ = ( +g ` U )   =>    |- ( ( K e. HL /\ W e. H ) -> .+ = .+b )
Theorem	dvhvadd 35766	The vector sum operation for the constructed full vector space H. (Contributed by NM, 11-Feb-2014.) (Revised by Mario Carneiro, 23-Jun-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (Scalar ` U )   &    |- .+ = ( +g ` U )   &    |- .+^ = ( +g ` D )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) = <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. )
Theorem	dvhopvadd 35767	The vector sum operation for the constructed full vector space H. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 6-May-2015.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (Scalar ` U )   &    |- .+ = ( +g ` U )   &    |- .+^ = ( +g ` D )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( <. F , Q >. .+ <. G , R >. ) = <. ( F o. G ) , ( Q .+^ R ) >. )
Theorem	dvhopvadd2 35768*	The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd 35767 and/or dvhfplusr 35758. (Contributed by NM, 26-Sep-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- .+ = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+b = ( +g ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( <. F , Q >. .+b <. G , R >. ) = <. ( F o. G ) , ( Q .+ R ) >. )
Theorem	dvhvaddcl 35769	Closure of the vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (Scalar ` U )   &    |- .+^ = ( +g ` D )   &    |- .+ = ( +g ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) e. ( T X. E ) )
Theorem	dvhvaddcomN 35770	Commutativity of vector sum. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (Scalar ` U )   &    |- .+^ = ( +g ` D )   &    |- .+ = ( +g ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) = ( G .+ F ) )
Theorem	dvhvaddass 35771	Associativity of vector sum. (Contributed by NM, 31-Oct-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (Scalar ` U )   &    |- .+^ = ( +g ` D )   &    |- .+ = ( +g ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( F .+ G ) .+ I ) = ( F .+ ( G .+ I ) ) )
Theorem	dvhvscacbv 35772*	Change bound variables to isolate them later. (Contributed by NM, 20-Nov-2013.)
|- .x. = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )   =>    |- .x. = ( t e. E , g e. ( T X. E ) |-> <. ( t ` ( 1st ` g ) ) , ( t o. ( 2nd ` g ) ) >. )
Theorem	dvhvscaval 35773*	The scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Nov-2013.)
|- .x. = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )   =>    |- ( ( U e. E /\ F e. ( T X. E ) ) -> ( U .x. F ) = <. ( U ` ( 1st ` F ) ) , ( U o. ( 2nd ` F ) ) >. )
Theorem	dvhfvsca 35774*	Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013.) (Revised by Mario Carneiro, 23-Jun-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .x. = ( .s ` U )   =>    |- ( ( K e. V /\ W e. H ) -> .x. = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) )
Theorem	dvhvsca 35775	Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .x. = ( .s ` U )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. ( T X. E ) ) ) -> ( R .x. F ) = <. ( R ` ( 1st ` F ) ) , ( R o. ( 2nd ` F ) ) >. )
Theorem	dvhopvsca 35776	Scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Feb-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .x. = ( .s ` U )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> ( R .x. <. F , X >. ) = <. ( R ` F ) , ( R o. X ) >. )
Theorem	dvhvscacl 35777	Closure of the scalar product operation for the constructed full vector space H. (Contributed by NM, 12-Feb-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .x. = ( .s ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( R e. E /\ F e. ( T X. E ) ) ) -> ( R .x. F ) e. ( T X. E ) )
Theorem	tendoinvcl 35778*	Closure of multiplicative inverse for endomorphism. We use the scalar inverse of the vector space since it is much simpler than the direct inverse of cdleml8 35656. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- N = ( invr ` F )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( ( N ` S ) e. E /\ ( N ` S ) =/= O ) )
Theorem	tendolinv 35779*	Left multiplicative inverse for endomorphism. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- N = ( invr ` F )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( ( N ` S ) o. S ) = ( _I |` T ) )
Theorem	tendorinv 35780*	Right multiplicative inverse for endomorphism. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- O = ( h e. T |-> ( _I |` B ) )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- F = (Scalar ` U )   &    |- N = ( invr ` F )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( S o. ( N ` S ) ) = ( _I |` T ) )
Theorem	dvhgrp 35781	The full vector space U constructed from a Hilbert lattice K (given a fiducial hyperplane W) is a group. (Contributed by NM, 19-Oct-2013.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (Scalar ` U )   &    |- .+^ = ( +g ` D )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` D )   &    |- I = ( invg ` D )   =>    |- ( ( K e. HL /\ W e. H ) -> U e. Grp )
Theorem	dvhlveclem 35782	Lemma for dvhlvec 35783. TODO: proof substituting inner part first shorter/longer than substituting outer part first? TODO: break up into smaller lemmas? TODO: does ph -> method shorten proof? (Contributed by NM, 22-Oct-2013.) (Proof shortened by Mario Carneiro, 24-Jun-2014.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- D = (Scalar ` U )   &    |- .+^ = ( +g ` D )   &    |- .+ = ( +g ` U )   &    |- .0. = ( 0g ` D )   &    |- I = ( invg ` D )   &    |- .X. = ( .r ` D )   &    |- .x. = ( .s ` U )   =>    |- ( ( K e. HL /\ W e. H ) -> U e. LVec )
Theorem	dvhlvec 35783	The full vector space U constructed from a Hilbert lattice K (given a fiducial hyperplane W) is a left module. (Contributed by NM, 23-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> U e. LVec )
Theorem	dvhlmod 35784	The full vector space U constructed from a Hilbert lattice K (given a fiducial hyperplane W) is a left module. (Contributed by NM, 23-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> U e. LMod )
Theorem	dvh0g 35785*	The zero vector of vector space H has the zero translation as its first member and the zero trace-preserving endomorphism as the second. (Contributed by NM, 9-Mar-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .0. = ( 0g ` U )   &    |- O = ( f e. T |-> ( _I |` B ) )   =>    |- ( ( K e. HL /\ W e. H ) -> .0. = <. ( _I |` B ) , O >. )
Theorem	dvheveccl 35786	Properties of a unit vector that we will use later as a convenient reference vector. This vector is called "e" in the remark after Lemma M of [Crawley] p. 121. line 17. See also dvhopN 35790 and dihpN 36010. (Contributed by NM, 27-Mar-2015.)
|- H = ( LHyp ` K )   &    |- B = ( Base ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- E = <. ( _I |` B ) , ( _I |` T ) >.   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> E e. ( V \ { .0. } ) )
Theorem	dvhopclN 35787	Closure of a DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.)
|- ( ( F e. T /\ U e. E ) -> <. F , U >. e. ( T X. E ) )
Theorem	dvhopaddN 35788*	Sum of DVecH vectors expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.)
|- A = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) P ( 2nd ` g ) ) >. )   =>    |- ( ( ( F e. T /\ U e. E ) /\ ( G e. T /\ V e. E ) ) -> ( <. F , U >. A <. G , V >. ) = <. ( F o. G ) , ( U P V ) >. )
Theorem	dvhopspN 35789*	Scalar product of DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.)
|- S = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )   =>    |- ( ( R e. E /\ ( F e. T /\ U e. E ) ) -> ( R S <. F , U >. ) = <. ( R ` F ) , ( R o. U ) >. )
Theorem	dvhopN 35790*	Decompose a DVecH vector expressed as an ordered pair into the sum of two components, the first from the translation group vector base of DVecA and the other from the one-dimensional vector subspace E. Part of Lemma M of [Crawley] p. 121, line 18. We represent their e, sigma, f by <. ( _I |` B ) , ( _I |` T ) >., U, <. F , O >.. We swapped the order of vector sum (their juxtaposition i.e. composition) to show <. F , O >. first. Note that O and ( _I |` T ) are the zero and one of the division ring E, and ( _I |` B ) is the zero of the translation group. S is the scalar product. (Contributed by NM, 21-Nov-2013.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- P = ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) )   &    |- A = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) P ( 2nd ` g ) ) >. )   &    |- S = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )   &    |- O = ( c e. T |-> ( _I |` B ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> <. F , U >. = ( <. F , O >. A ( U S <. ( _I |` B ) , ( _I |` T ) >. ) ) )
Theorem	dvhopellsm 35791*	Ordered pair membership in a subspace sum. (Contributed by NM, 12-Mar-2014.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- S = ( LSubSp ` U )   &    |- .(+) = ( LSSum ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( <. F , T >. e. ( X .(+) Y ) <-> E. x E. y E. z E. w ( ( <. x , y >. e. X /\ <. z , w >. e. Y ) /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )
Theorem	cdlemm10N 35792*	The image of the map G is the entire one-dimensional subspace ( I ` V ). Remark after Lemma M of [Crawley] p. 121 line 23. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- C = { r e. A | ( r .<_ ( P .\/ V ) /\ -. r .<_ W ) }   &    |- F = ( iota_ f e. T ( f ` P ) = s )   &    |- G = ( q e. C |-> ( iota_ f e. T ( f ` P ) = q ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ran G = ( I ` V ) )
Syntax	cocaN 35793	Extend class notation with subspace orthocomplement for DVecA partial vector space.
class ocA
Definition	df-docaN 35794*	Define subspace orthocomplement for DVecA partial vector space. Temporarily, we are using the range of the isomorphism instead of the set of closed subspaces. Later, when inner product is introduced, we will show that these are the same. (Contributed by NM, 6-Dec-2013.)
|- ocA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( DIsoA ` k ) ` w ) ` ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w ) ) ) ) )
Theorem	docaffvalN 35795*	Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- H = ( LHyp ` K )   =>    |- ( K e. V -> ( ocA ` K ) = ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( DIsoA ` K ) ` w ) ` ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) ) ) ) )
Theorem	docafvalN 35796*	Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- N = ( ( ocA ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> N = ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) ) )
Theorem	docavalN 35797*	Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- N = ( ( ocA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( N ` X ) = ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) )
Theorem	docaclN 35798	Closure of subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ._|_ ` X ) e. ran I )
Theorem	diaocN 35799	Value of partial isomorphism A at lattice orthocomplement (using a Sasaki projection to get orthocomplement relative to the fiducial co-atom W). (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- N = ( ( ocA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` ( ( ( ._|_ ` X ) .\/ ( ._|_ ` W ) ) ./\ W ) ) = ( N ` ( I ` X ) ) )
Theorem	doca2N 35800	Double orthocomplement of partial isomorphism A. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ._|_ ` ( ._|_ ` ( I ` X ) ) ) = ( I ` X ) )