P. 373 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37201-37300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	diaintclN 37201	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 37202	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 37203	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 37204*	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 37205	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 37206	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 37207	Lemma for dia2dim 37220. 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 37208	Lemma for dia2dim 37220. 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 37209	Lemma for dia2dim 37220. 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 37210	Lemma for dia2dim 37220. 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 37211	Lemma for dia2dim 37220. 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 37212	Lemma for dia2dim 37220. 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 37213	Lemma for dia2dim 37220. 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 37214	Lemma for dia2dim 37220. 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 37215	Lemma for dia2dim 37220. 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 37216	Lemma for dia2dim 37220. 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 37217	Lemma for dia2dim 37220. 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 37218	Lemma for dia2dim 37220. 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 37219	Lemma for dia2dim 37220. 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 37220	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 37221	Extend class notation with constructed full vector space H.
class DVecH
Definition	df-dvech 37222*	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 37223*	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 37224*	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 37225	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 37226	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 37227*	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 37228*	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 37229	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 37230	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 37231	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 37232*	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 37233*	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 37234*	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 37235	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 37236	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 37237*	The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd 37236 and/or dvhfplusr 37227. (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 37238	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 37239	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 37240	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 37241*	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 37242*	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 37243*	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 37244	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 37245	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 37246	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 37247*	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 37125. (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 37248*	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 37249*	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 37250	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 37251	Lemma for dvhlvec 37252. 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 37252	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 37253	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 37254*	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 37255	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 37259 and dihpN 37479. (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 37256	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 37257*	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 37258*	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 37259*	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 37260*	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 37261*	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 37262	Extend class notation with subspace orthocomplement for DVecA partial vector space.
class ocA
Definition	df-docaN 37263*	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 37264*	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 37265*	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 37266*	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 37267	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 37268	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 37269	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 37270	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 37271	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 37272*	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 37273*	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 37178 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 37274	Extend class notation with subspace join for DVecA partial vector space.
class vA
Definition	df-djaN 37275*	Define (closed) subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.)
|- vA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) , y e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) ) ) )
Theorem	djaffvalN 37276*	Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   =>    |- ( K e. V -> ( vA ` K ) = ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) , y e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( ocA ` K ) ` w ) ` ( ( ( ( ocA ` K ) ` w ) ` x ) i^i ( ( ( ocA ` K ) ` w ) ` y ) ) ) ) ) )
Theorem	djafvalN 37277*	Subspace join for DVecA partial vector space. TODO: take out hypothesis .i, no longer used. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   &    |- J = ( ( vA ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> J = ( x e. ~P T , y e. ~P T |-> ( ._|_ ` ( ( ._|_ ` x ) i^i ( ._|_ ` y ) ) ) ) )
Theorem	djavalN 37278	Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- ._|_ = ( ( ocA ` K ) ` W )   &    |- J = ( ( vA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X J Y ) = ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
Theorem	djaclN 37279	Closure of subspace join for DVecA partial vector space. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- J = ( ( vA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X J Y ) e. ran I )
Theorem	djajN 37280	Transfer lattice join to DVecA partial vector space closed subspace join. Part of Lemma M of [Crawley] p. 120 line 29, with closed subspace join rather than subspace sum. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
|- .\/ = ( join ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoA ` K ) ` W )   &    |- J = ( ( vA ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. dom I /\ Y e. dom I ) ) -> ( I ` ( X .\/ Y ) ) = ( ( I ` X ) J ( I ` Y ) ) )
Syntax	cdib 37281	Extend class notation with isomorphism B.
class DIsoB
Definition	df-dib 37282*	Isomorphism B is isomorphism A extended with an extra dimension set to the zero vector component i.e. the zero endormorphism. Its domain is lattice elements less than or equal to the fiducial co-atom w. (Contributed by NM, 8-Dec-2013.)
|- DIsoB = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. dom ( ( DIsoA ` k ) ` w ) |-> ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } ) ) ) )
Theorem	dibffval 37283*	The partial isomorphism B for a lattice K. (Contributed by NM, 8-Dec-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   =>    |- ( K e. V -> ( DIsoB ` K ) = ( w e. H |-> ( x e. dom ( ( DIsoA ` K ) ` w ) |-> ( ( ( ( DIsoA ` K ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` K ) ` w ) |-> ( _I |` B ) ) } ) ) ) )
Theorem	dibfval 37284*	The partial isomorphism B for a lattice K. (Contributed by NM, 8-Dec-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .0. = ( f e. T |-> ( _I |` B ) )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> I = ( x e. dom J |-> ( ( J ` x ) X. { .0. } ) ) )
Theorem	dibval 37285*	The partial isomorphism B for a lattice K. (Contributed by NM, 8-Dec-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .0. = ( f e. T |-> ( _I |` B ) )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( I ` X ) = ( ( J ` X ) X. { .0. } ) )
Theorem	dibopelvalN 37286*	Member of the partial isomorphism B. (Contributed by NM, 18-Jan-2014.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .0. = ( f e. T |-> ( _I |` B ) )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ X e. dom J ) -> ( <. F , S >. e. ( I ` X ) <-> ( F e. ( J ` X ) /\ S = .0. ) ) )
Theorem	dibval2 37287*	Value of the partial isomorphism B. (Contributed by NM, 18-Jan-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .0. = ( f e. T |-> ( _I |` B ) )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = ( ( J ` X ) X. { .0. } ) )
Theorem	dibopelval2 37288*	Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014.) (Revised by Mario Carneiro, 6-May-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .0. = ( f e. T |-> ( _I |` B ) )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( <. F , S >. e. ( I ` X ) <-> ( F e. ( J ` X ) /\ S = .0. ) ) )
Theorem	dibval3N 37289*	Value of the partial isomorphism B for a lattice K. (Contributed by NM, 24-Feb-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- .0. = ( g e. T |-> ( _I |` B ) )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = ( { f e. T | ( R ` f ) .<_ X } X. { .0. } ) )
Theorem	dibelval3 37290*	Member of the partial isomorphism B. (Contributed by NM, 26-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- .0. = ( g e. T |-> ( _I |` B ) )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( Y e. ( I ` X ) <-> E. f e. T ( Y = <. f , .0. >. /\ ( R ` f ) .<_ X ) ) )
Theorem	dibopelval3 37291*	Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- .0. = ( g e. T |-> ( _I |` B ) )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( <. F , S >. e. ( I ` X ) <-> ( ( F e. T /\ ( R ` F ) .<_ X ) /\ S = .0. ) ) )
Theorem	dibelval1st 37292	Membership in value of the partial isomorphism B for a lattice K. (Contributed by NM, 13-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ Y e. ( I ` X ) ) -> ( 1st ` Y ) e. ( J ` X ) )
Theorem	dibelval1st1 37293	Membership in value of the partial isomorphism B for a lattice K. (Contributed by NM, 13-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ Y e. ( I ` X ) ) -> ( 1st ` Y ) e. T )
Theorem	dibelval1st2N 37294	Membership in value of the partial isomorphism B for a lattice K. (Contributed by NM, 13-Feb-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ Y e. ( I ` X ) ) -> ( R ` ( 1st ` Y ) ) .<_ X )
Theorem	dibelval2nd 37295*	Membership in value of the partial isomorphism B for a lattice K. (Contributed by NM, 13-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- .0. = ( f e. T |-> ( _I |` B ) )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ Y e. ( I ` X ) ) -> ( 2nd ` Y ) = .0. )
Theorem	dibn0 37296	The value of the partial isomorphism B is not empty. (Contributed by NM, 18-Jan-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) =/= (/) )
Theorem	dibfna 37297	Functionality and domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.)
|- H = ( LHyp ` K )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> I Fn dom J )
Theorem	dibdiadm 37298	Domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.)
|- H = ( LHyp ` K )   &    |- J = ( ( DIsoA ` K ) ` W )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> dom I = dom J )
Theorem	dibfnN 37299*	Functionality and domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> I Fn { x e. B | x .<_ W } )
Theorem	dibdmN 37300*	Domain of the partial isomorphism A. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( ( DIsoB ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> dom I = { x e. B | x .<_ W } )