P. 351 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35001-35100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dia11N 35001	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 35002	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 35003	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 35004	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 35005	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 35006	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 35007	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 35008*	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 35009	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 35010	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 35011	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 35012	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 35013	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 35014*	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 35015	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 35016	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 35017	Lemma for dia2dim 35030. 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 35018	Lemma for dia2dim 35030. 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 35019	Lemma for dia2dim 35030. 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 35020	Lemma for dia2dim 35030. 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 35021	Lemma for dia2dim 35030. 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 35022	Lemma for dia2dim 35030. 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 35023	Lemma for dia2dim 35030. 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 35024	Lemma for dia2dim 35030. 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 35025	Lemma for dia2dim 35030. 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 35026	Lemma for dia2dim 35030. 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 35027	Lemma for dia2dim 35030. 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 35028	Lemma for dia2dim 35030. 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 35029	Lemma for dia2dim 35030. 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 35030	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 35031	Extend class notation with constructed full vector space H.
class DVecH
Definition	df-dvech 35032*	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 35033*	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 35034*	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 35035	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 35036	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 35037*	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 35038*	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 35039	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 35040	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 35041	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 35042*	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 35043*	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 35044*	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 35045	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 35046	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 35047*	The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd 35046 and/or dvhfplusr 35037. (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 35048	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 35049	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 35050	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 35051*	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 35052*	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 35053*	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 35054	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 35055	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 35056	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 35057*	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 34935. (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 35058*	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 35059*	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 35060	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 35061	Lemma for dvhlvec 35062. 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 35062	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 35063	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 35064*	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 35065	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 35069 and dihpN 35289. (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 35066	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 35067*	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 35068*	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 35069*	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 35070*	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 35071*	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 35072	Extend class notation with subspace orthocomplement for DVecA partial vector space.
class ocA
Definition	df-docaN 35073*	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 35074*	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 35075*	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 35076*	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 35077	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 35078	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 35079	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 35080	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 35081	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 35082*	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 35083*	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 34988 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 35084	Extend class notation with subspace join for DVecA partial vector space.
class vA
Definition	df-djaN 35085*	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 35086*	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 35087*	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 35088	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 35089	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 35090	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 35091	Extend class notation with isomorphism B.
class DIsoB
Definition	df-dib 35092*	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 35093*	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 35094*	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 35095*	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 35096*	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 35097*	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 35098*	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 35099*	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 35100*	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 ) ) )