P. 347 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	diaelval 34601	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 34602*	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 34603*	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 34604	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 34605	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 34606	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 34607	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 34608	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 34609	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 34610	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 34611	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 34612	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 34613	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 34614	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 34615	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 34616	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 34617	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 34618	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 34619	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 34620	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 34621	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 34622	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 34623*	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 34624	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 34625	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 34626	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 34627	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 34628	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 34629*	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 34630	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 34631	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 34632	Lemma for dia2dim 34645. 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 34633	Lemma for dia2dim 34645. 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 34634	Lemma for dia2dim 34645. 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 34635	Lemma for dia2dim 34645. 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 34636	Lemma for dia2dim 34645. 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 34637	Lemma for dia2dim 34645. 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 34638	Lemma for dia2dim 34645. 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 34639	Lemma for dia2dim 34645. 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 34640	Lemma for dia2dim 34645. 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 34641	Lemma for dia2dim 34645. 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 34642	Lemma for dia2dim 34645. 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 34643	Lemma for dia2dim 34645. 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 34644	Lemma for dia2dim 34645. 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 34645	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 34646	Extend class notation with constructed full vector space H.
class DVecH
Definition	df-dvech 34647*	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 34648*	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 34649*	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 34650	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 34651	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 34652*	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 34653*	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 34654	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 34655	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 34656	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 34657*	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 34658*	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 34659*	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 34660	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 34661	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 34662*	The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd 34661 and/or dvhfplusr 34652. (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 34663	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 34664	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 34665	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 34666*	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 34667*	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 34668*	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 34669	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 34670	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 34671	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 34672*	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 34550. (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 34673*	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 34674*	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 34675	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 34676	Lemma for dvhlvec 34677. 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 34677	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 34678	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 34679*	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 34680	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 34684 and dihpN 34904. (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 34681	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 34682*	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 34683*	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 34684*	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 34685*	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 34686*	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 34687	Extend class notation with subspace orthocomplement for DVecA partial vector space.
class ocA
Definition	df-docaN 34688*	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 34689*	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 34690*	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 34691*	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 34692	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 34693	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 34694	Double orthocomplement of partial isomorphism A. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ._|_ ` ( ._|_ ` ( I ` X ) ) ) = ( I ` X ) )
Theorem	doca3N 34695	Double orthocomplement of partial isomorphism A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
Theorem	dvadiaN 34696	Any closed subspace is a member of the range of partial isomorphism A, showing the isomorphism maps onto the set of closed subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecA ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   &    |- S = ( LSubSp ` U )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. S /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) -> X e. ran I )
Theorem	diarnN 34697*	Partial isomorphism A maps onto the set of all closed subspaces of partial vector space A. Part of Lemma M of [Crawley] p. 121 line 12, with closed subspaces rather than subspaces. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecA ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   &    |- S = ( LSubSp ` U )   =>    |- ( ( K e. HL /\ W e. H ) -> ran I = { x e. S | ( ._|_ ` ( ._|_ ` x ) ) = x } )
Theorem	diaf1oN 34698*	The partial isomorphism A for a lattice K is a one-to-one, onto function. Part of Lemma M of [Crawley] p. 121 line 12, with closed subspaces rather than subspaces. See diadm 34603 for the domain. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecA ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   &    |- S = ( LSubSp ` U )   =>    |- ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> { x e. S | ( ._|_ ` ( ._|_ ` x ) ) = x } )
Syntax	cdjaN 34699	Extend class notation with subspace join for DVecA partial vector space.
class vA
Definition	df-djaN 34700*	Define (closed) subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.)
|- vA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) , y e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) ) ) )