P. 344 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34301-34400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tendocnv 34301	Converse of a trace-preserving endomorphism value. (Contributed by NM, 7-Apr-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> `' ( S ` F ) = ( S ` `' F ) )
Theorem	tendospdi2 34302*	Reverse distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
|- T = ( ( LTrn ` K ) ` W )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   =>    |- ( ( U e. E /\ V e. E /\ F e. T ) -> ( ( U P V ) ` F ) = ( ( U ` F ) o. ( V ` F ) ) )
Theorem	tendospcanN 34303*	Cancellation law for trace-perserving endomorphism values (used as scalar product). (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- O = ( f e. T |-> ( _I |` B ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ S =/= O ) /\ ( F e. T /\ G e. T ) ) -> ( ( S ` F ) = ( S ` G ) <-> F = G ) )
Theorem	dvaabl 34304	The constructed partial vector space A for a lattice K is an abelian group. (Contributed by NM, 11-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecA ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> U e. Abel )
Theorem	dvalveclem 34305	Lemma for dvalvec 34306. (Contributed by NM, 11-Oct-2013.) (Proof shortened by Mario Carneiro, 22-Jun-2014.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecA ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .+ = ( +g ` U )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = (Scalar ` U )   &    |- B = ( Base ` K )   &    |- .+^ = ( +g ` D )   &    |- .X. = ( .r ` D )   &    |- .x. = ( .s ` U )   =>    |- ( ( K e. HL /\ W e. H ) -> U e. LVec )
Theorem	dvalvec 34306	The constructed partial vector space A for a lattice K is a left vector space. (Contributed by NM, 11-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecA ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> U e. LVec )
Theorem	dva0g 34307	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 34308	Extend class notation with partial isomorphism A.
class DIsoA
Definition	df-disoa 34309*	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 34310*	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 34311*	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 34312*	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 34313	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 34314*	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 34315*	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 34316	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 34317	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 34318	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 34319	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 34320	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 34321	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 34322	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 34323	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 34324	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 34325	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 34326	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 34327	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 34328	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 34329	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 34330	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 34331	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 34332	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 34333	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 34334	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 34335*	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 34336	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 34337	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 34338	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 34339	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 34340	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 34341*	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 34342	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 34343	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 34344	Lemma for dia2dim 34357. 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 34345	Lemma for dia2dim 34357. 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 34346	Lemma for dia2dim 34357. 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 34347	Lemma for dia2dim 34357. 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 34348	Lemma for dia2dim 34357. 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 34349	Lemma for dia2dim 34357. 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 34350	Lemma for dia2dim 34357. 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 34351	Lemma for dia2dim 34357. 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 34352	Lemma for dia2dim 34357. 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 34353	Lemma for dia2dim 34357. 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 34354	Lemma for dia2dim 34357. 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 34355	Lemma for dia2dim 34357. 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 34356	Lemma for dia2dim 34357. 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 34357	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 34358	Extend class notation with constructed full vector space H.
class DVecH
Definition	df-dvech 34359*	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 34360*	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 34361*	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 34362	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 34363	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 34364*	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 34365*	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 34366	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 34367	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 34368	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 34369*	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 34370*	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 34371*	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 34372	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 34373	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 34374*	The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd 34373 and/or dvhfplusr 34364. (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 34375	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 34376	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 34377	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 34378*	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 34379*	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 34380*	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 34381	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 34382	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 34383	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 34384*	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 34262. (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 34385*	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 34386*	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 34387	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 34388	Lemma for dvhlvec 34389. 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 34389	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 34390	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 34391*	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 34392	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 34396 and dihpN 34616. (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 34393	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 34394*	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 34395*	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 34396*	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 34397*	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 34398*	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 34399	Extend class notation with subspace orthocomplement for DVecA partial vector space.
class ocA
Definition	df-docaN 34400*	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 ) ) ) ) )