HomeHome Metamath Proof Explorer
Theorem List (p. 305 of 315)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-21490)
  Hilbert Space Explorer  Hilbert Space Explorer
(21491-23013)
  Users' Mathboxes  Users' Mathboxes
(23014-31421)
 

Theorem List for Metamath Proof Explorer - 30401-30500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdlemk11tc 30401* Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119.  G,  I stand for g, h. TODO: fix comment. (Contributed by NM, 21-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( b  e.  T  /\  (
 b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  G ) ) 
 /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  I ) ) ) )  ->  ( [_ G  /  g ]_ X `  P ) 
 .<_  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `
  ( I  o.  `' G ) ) ) )
 
Theoremcdlemk11t 30402* Part of proof of Lemma K of [Crawley] p. 118. Eq. 5, line 36, p. 119.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 21-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) ) )  ->  ( [_ G  /  g ]_ X `  P ) 
 .<_  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `
  ( I  o.  `' G ) ) ) )
 
Theoremcdlemk45 30403* Part of proof of Lemma K of [Crawley] p. 118. Line 37, p. 119.  G,  I stand for g, h.  X represents tau. They do not explicitly mention the requirement  ( G  o.  I
)  =/=  (  _I  |  `  B ). (Contributed by NM, 22-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( G  o.  I )  =/=  (  _I  |`  B ) ) )  ->  ( [_ ( G  o.  I
 )  /  g ]_ X `  P )  .<_  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `  G ) ) )
 
Theoremcdlemk46 30404* Part of proof of Lemma K of [Crawley] p. 118. Line 38 (last line), p. 119.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 22-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( G  o.  I )  =/=  (  _I  |`  B ) ) )  ->  ( [_ ( G  o.  I
 )  /  g ]_ X `  P )  .<_  ( ( [_ G  /  g ]_ X `  P )  .\/  ( R `  I ) ) )
 
Theoremcdlemk47 30405* Part of proof of Lemma K of [Crawley] p. 118. Line 2, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 22-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( R `  G )  =/=  ( R `  I ) ) )  ->  ( [_ ( G  o.  I
 )  /  g ]_ X `  P )  =  ( ( ( [_ G  /  g ]_ X `  P )  .\/  ( R `  I ) ) 
 ./\  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `  G ) ) ) )
 
Theoremcdlemk48 30406* Part of proof of Lemma K of [Crawley] p. 118. Line 4, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 22-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) ) )  ->  (
 ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) `
  P )  .<_  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `  [_ G  /  g ]_ X ) ) )
 
Theoremcdlemk49 30407* Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 23-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) ) )  ->  (
 ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) `
  P )  .<_  ( ( [_ G  /  g ]_ X `  P )  .\/  ( R `  [_ I  /  g ]_ X ) ) )
 
Theoremcdlemk50 30408* Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120.  G,  I stand for g, h.  X represents tau. TODO: Combine into cdlemk52 30410? (Contributed by NM, 23-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) ) )  ->  (
 ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) `
  P )  .<_  ( ( ( [_ G  /  g ]_ X `  P )  .\/  ( R `
  [_ I  /  g ]_ X ) )  ./\  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `
  [_ G  /  g ]_ X ) ) ) )
 
Theoremcdlemk51 30409* Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120.  G,  I stand for g, h.  X represents tau. TODO: Combine into cdlemk52 30410? (Contributed by NM, 23-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) ) )  ->  (
 ( ( [_ G  /  g ]_ X `  P )  .\/  ( R `
  [_ I  /  g ]_ X ) )  ./\  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `
  [_ G  /  g ]_ X ) ) ) 
 .<_  ( ( ( [_ G  /  g ]_ X `  P )  .\/  ( R `  I ) ) 
 ./\  ( ( [_ I  /  g ]_ X `  P )  .\/  ( R `  G ) ) ) )
 
Theoremcdlemk52 30410* Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 23-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( R `  G )  =/=  ( R `  I ) ) )  ->  ( ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) `
  P )  =  ( [_ ( G  o.  I )  /  g ]_ X `  P ) )
 
Theoremcdlemk53a 30411* Lemma for cdlemk53 30413. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  F  =/=  (  _I  |`  B ) )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) ) 
 /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( R `  G )  =/=  ( R `  I ) ) )  ->  [_ ( G  o.  I )  /  g ]_ X  =  (
 [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) )
 
Theoremcdlemk53b 30412* Lemma for cdlemk53 30413. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( I  e.  T  /\  I  =/=  (  _I  |`  B ) 
 /\  ( R `  G )  =/=  ( R `  I ) ) )  ->  [_ ( G  o.  I )  /  g ]_ X  =  (
 [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) )
 
Theoremcdlemk53 30413* Part of proof of Lemma K of [Crawley] p. 118. Line 7, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( I  e.  T  /\  ( R `  G )  =/=  ( R `  I
 ) ) )  ->  [_ ( G  o.  I
 )  /  g ]_ X  =  ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) )
 
Theoremcdlemk54 30414* Part of proof of Lemma K of [Crawley] p. 118. Line 10, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( ( I  e.  T  /\  ( R `  G )  =  ( R `  I ) )  /\  j  e.  T  /\  ( j  =/=  (  _I  |`  B )  /\  ( R `  j )  =/=  ( R `  G )  /\  ( R `
  j )  =/=  ( R `  ( G  o.  I ) ) ) ) )  ->  ( [_ ( G  o.  I )  /  g ]_ X  o.  [_ j  /  g ]_ X )  =  ( ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X )  o.  [_ j  /  g ]_ X ) )
 
Theoremcdlemk55a 30415* Lemma for cdlemk55 30417. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( ( I  e.  T  /\  ( R `  G )  =  ( R `  I ) )  /\  j  e.  T  /\  ( j  =/=  (  _I  |`  B )  /\  ( R `  j )  =/=  ( R `  G )  /\  ( R `
  j )  =/=  ( R `  ( G  o.  I ) ) ) ) )  ->  [_ ( G  o.  I
 )  /  g ]_ X  =  ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) )
 
Theoremcdlemk55b 30416* Lemma for cdlemk55 30417. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( I  e.  T  /\  ( R `  G )  =  ( R `  I
 ) ) )  ->  [_ ( G  o.  I
 )  /  g ]_ X  =  ( [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) )
 
Theoremcdlemk55 30417* Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 26-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B )  /\  N  e.  T )  /\  G  e.  T  /\  I  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  [_ ( G  o.  I )  /  g ]_ X  =  (
 [_ G  /  g ]_ X  o.  [_ I  /  g ]_ X ) )
 
TheoremcdlemkyyN 30418* Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up  ( b Y G ) stuff. (Contributed by NM, 21-Jul-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T ( i `
  P )  =  ( ( P  .\/  ( R `  f ) )  ./\  ( ( N `  P )  .\/  ( R `  ( f  o.  `' F ) ) ) ) ) )   &    |-  V  =  ( d  e.  T ,  e  e.  T  |->  ( iota_ j  e.  T ( j `
  P )  =  ( ( P  .\/  ( R `  e ) )  ./\  ( (
 ( S `  d
 ) `  P )  .\/  ( R `  (
 e  o.  `' d
 ) ) ) ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H  /\  ( R `
  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  F  =/=  (  _I  |`  B ) 
 /\  N  e.  T )  /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  (
 b  e.  T  /\  ( b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `
  b )  =/=  ( R `  G ) ) ) ) 
 ->  ( [_ G  /  g ]_ X `  P )  =  ( (
 b V G ) `
  P ) )
 
Theoremcdlemk43N 30419* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 31-Jul-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  e.  T  /\  N  e.  T  /\  F  =/=  N ) 
 /\  ( G  e.  T  /\  G  =/=  (  _I  |`  B ) ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  (
 b  e.  T  /\  ( b  =/=  (  _I  |`  B )  /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `
  b )  =/=  ( R `  G ) ) ) ) 
 ->  ( ( U `  G ) `  P )  =  [_ G  /  g ]_ Y )
 
Theoremcdlemk35u 30420* Substitution version of cdlemk35 30368. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  e.  T  /\  N  e.  T  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( U `  G )  e.  T )
 
Theoremcdlemk55u1 30421* Lemma for cdlemk55u 30422. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  N  e.  T )  /\  ( ( ( R `
  F )  =  ( R `  N )  /\  F  =/=  N )  /\  G  e.  T  /\  I  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( U `  ( G  o.  I ) )  =  ( ( U `  G )  o.  ( U `  I ) ) )
 
Theoremcdlemk55u 30422* Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120.  G,  I stand for g, h.  X represents tau. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  N  e.  T )  /\  ( ( R `  F )  =  ( R `  N )  /\  G  e.  T  /\  I  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( U `  ( G  o.  I
 ) )  =  ( ( U `  G )  o.  ( U `  I ) ) )
 
Theoremcdlemk39u1 30423* Lemma for cdlemk39u 30424. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  N  e.  T )  /\  ( ( R `  F )  =  ( R `  N )  /\  F  =/=  N  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) 
 ->  ( R `  ( U `  G ) ) 
 .<_  ( R `  G ) )
 
Theoremcdlemk39u 30424* Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. Trace-preserving property of the value of tau, represented by  ( U `  G ). (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  N  e.  T )  /\  ( ( R `  F )  =  ( R `  N )  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  ( U `  G ) )  .<_  ( R `
  G ) )
 
Theoremcdlemk19u1 30425* cdlemk19 30325 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  e.  T  /\  F  =/=  N  /\  N  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( U `  F ) `  P )  =  ( N `  P ) )
 
Theoremcdlemk19u 30426* Part of Lemma K of [Crawley] p. 118. Line 12, p. 120, "f (exponent) tau = k". We represent f, k, tau with  F,  N,  U. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  e.  T  /\  N  e.  T ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( U `  F )  =  N )
 
Theoremcdlemk56 30427* Part of Lemma K of [Crawley] p. 118. Line 11, p. 120, "tau is in Delta" i.e.  U is a trace-preserving endormorphism. (Contributed by NM, 31-Jul-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   &    |-  E  =  ( (
 TEndo `  K ) `  W )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  N  e.  T )  /\  ( R `  F )  =  ( R `  N )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) 
 ->  U  e.  E )
 
Theoremcdlemk19w 30428* Use a fixed element to eliminate  P in cdlemk19u 30426. (Contributed by NM, 1-Aug-2013.)
 |-  B  =  ( Base `  K )   &    |-  .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  ._|_  =  ( oc `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  P  =  (  ._|_  `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) ) 
 ./\  ( Z  .\/  ( R `  ( g  o.  `' b ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  N  e.  T )  /\  ( R `  F )  =  ( R `  N ) )  ->  ( U `  F )  =  N )
 
Theoremcdlemk56w 30429* Use a fixed element to eliminate  P in cdlemk56 30427. (Contributed by NM, 1-Aug-2013.)
 |-  B  =  ( Base `  K )   &    |-  .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  ._|_  =  ( oc `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  (
 LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  P  =  (  ._|_  `  W )   &    |-  Z  =  ( ( P  .\/  ( R `  b ) )  ./\  ( ( N `  P )  .\/  ( R `
  ( b  o.  `' F ) ) ) )   &    |-  Y  =  ( ( P  .\/  ( R `  g ) ) 
 ./\  ( Z  .\/  ( R `  ( g  o.  `' b ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  F )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  P )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if ( F  =  N ,  g ,  X )
 )   &    |-  E  =  ( (
 TEndo `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  N  e.  T )  /\  ( R `  F )  =  ( R `  N ) )  ->  ( U  e.  E  /\  ( U `  F )  =  N )
 )
 
Theoremcdlemk 30430* Lemma K of [Crawley] p. 118. Final result, lines 11 and 12 on p. 120: given two translations f and k with the same trace, there exists a trace-preserving endomorphism tau whose value at f is k. We use  F,  N, and  u to represent f, k, and tau. (Contributed by NM, 1-Aug-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  N  e.  T ) 
 /\  ( R `  F )  =  ( R `  N ) ) 
 ->  E. u  e.  E  ( u `  F )  =  N )
 
Theoremtendoex 30431* Generalization of Lemma K of [Crawley] p. 118, cdlemk 30430. TODO: can this be used to shorten uses of cdlemk 30430? (Contributed by NM, 15-Oct-2013.)
 |-  .<_  =  ( le `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  N  e.  T ) 
 /\  ( R `  N )  .<_  ( R `
  F ) ) 
 ->  E. u  e.  E  ( u `  F )  =  N )
 
Theoremcdleml1N 30432 Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( U  e.  E  /\  V  e.  E  /\  f  e.  T )  /\  ( f  =/=  (  _I  |`  B )  /\  ( U `  f )  =/=  (  _I  |`  B ) 
 /\  ( V `  f )  =/=  (  _I  |`  B ) ) )  ->  ( R `  ( U `  f
 ) )  =  ( R `  ( V `
  f ) ) )
 
Theoremcdleml2N 30433* Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( U  e.  E  /\  V  e.  E  /\  f  e.  T )  /\  ( f  =/=  (  _I  |`  B )  /\  ( U `  f )  =/=  (  _I  |`  B ) 
 /\  ( V `  f )  =/=  (  _I  |`  B ) ) )  ->  E. s  e.  E  ( s `  ( U `  f ) )  =  ( V `
  f ) )
 
Theoremcdleml3N 30434* Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  .0.  =  ( g  e.  T  |->  (  _I  |`  B )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( U  e.  E  /\  V  e.  E  /\  f  e.  T )  /\  ( f  =/=  (  _I  |`  B )  /\  U  =/=  .0.  /\  V  =/=  .0.  ) )  ->  E. s  e.  E  ( s  o.  U )  =  V )
 
Theoremcdleml4N 30435* Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  .0.  =  ( g  e.  T  |->  (  _I  |`  B )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( U  e.  E  /\  V  e.  E )  /\  ( U  =/=  .0.  /\  V  =/=  .0.  )
 )  ->  E. s  e.  E  ( s  o.  U )  =  V )
 
Theoremcdleml5N 30436* Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  .0.  =  ( g  e.  T  |->  (  _I  |`  B )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( U  e.  E  /\  V  e.  E )  /\  U  =/=  .0.  )  ->  E. s  e.  E  ( s  o.  U )  =  V )
 
Theoremcdleml6 30437* Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.)
 |-  B  =  ( Base `  K )   &    |-  .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Q  =  ( ( oc `  K ) `  W )   &    |-  Z  =  ( ( Q  .\/  ( R `  b ) )  ./\  ( ( h `  Q )  .\/  ( R `
  ( b  o.  `' ( s `  h ) ) ) ) )   &    |-  Y  =  ( ( Q  .\/  ( R `  g ) ) 
 ./\  ( Z  .\/  ( R `  ( g  o.  `' b ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  ( s `  h ) )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  Q )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if (
 ( s `  h )  =  h ,  g ,  X )
 )   &    |-  E  =  ( (
 TEndo `  K ) `  W )   &    |-  .0.  =  ( f  e.  T  |->  (  _I  |`  B )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  h  e.  T  /\  ( s  e.  E  /\  s  =/=  .0.  ) )  ->  ( U  e.  E  /\  ( U `  (
 s `  h )
 )  =  h ) )
 
Theoremcdleml7 30438* Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.)
 |-  B  =  ( Base `  K )   &    |-  .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Q  =  ( ( oc `  K ) `  W )   &    |-  Z  =  ( ( Q  .\/  ( R `  b ) )  ./\  ( ( h `  Q )  .\/  ( R `
  ( b  o.  `' ( s `  h ) ) ) ) )   &    |-  Y  =  ( ( Q  .\/  ( R `  g ) ) 
 ./\  ( Z  .\/  ( R `  ( g  o.  `' b ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  ( s `  h ) )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  Q )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if (
 ( s `  h )  =  h ,  g ,  X )
 )   &    |-  E  =  ( (
 TEndo `  K ) `  W )   &    |-  .0.  =  ( f  e.  T  |->  (  _I  |`  B )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  h  e.  T  /\  ( s  e.  E  /\  s  =/=  .0.  ) )  ->  ( ( U  o.  s ) `  h )  =  ( (  _I  |`  T ) `  h ) )
 
Theoremcdleml8 30439* Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.)
 |-  B  =  ( Base `  K )   &    |-  .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Q  =  ( ( oc `  K ) `  W )   &    |-  Z  =  ( ( Q  .\/  ( R `  b ) )  ./\  ( ( h `  Q )  .\/  ( R `
  ( b  o.  `' ( s `  h ) ) ) ) )   &    |-  Y  =  ( ( Q  .\/  ( R `  g ) ) 
 ./\  ( Z  .\/  ( R `  ( g  o.  `' b ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  ( s `  h ) )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  Q )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if (
 ( s `  h )  =  h ,  g ,  X )
 )   &    |-  E  =  ( (
 TEndo `  K ) `  W )   &    |-  .0.  =  ( f  e.  T  |->  (  _I  |`  B )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( h  e.  T  /\  h  =/=  (  _I  |`  B ) )  /\  ( s  e.  E  /\  s  =/=  .0.  ) )  ->  ( U  o.  s
 )  =  (  _I  |`  T ) )
 
Theoremcdleml9 30440* Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.)
 |-  B  =  ( Base `  K )   &    |-  .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Q  =  ( ( oc `  K ) `  W )   &    |-  Z  =  ( ( Q  .\/  ( R `  b ) )  ./\  ( ( h `  Q )  .\/  ( R `
  ( b  o.  `' ( s `  h ) ) ) ) )   &    |-  Y  =  ( ( Q  .\/  ( R `  g ) ) 
 ./\  ( Z  .\/  ( R `  ( g  o.  `' b ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  ( s `  h ) )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  Q )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if (
 ( s `  h )  =  h ,  g ,  X )
 )   &    |-  E  =  ( (
 TEndo `  K ) `  W )   &    |-  .0.  =  ( f  e.  T  |->  (  _I  |`  B )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( h  e.  T  /\  h  =/=  (  _I  |`  B ) )  /\  ( s  e.  E  /\  s  =/=  .0.  ) )  ->  U  =/=  .0.  )
 
Theoremdva1dim 30441* Two expressions for the 1-dimensional subspaces of partial vector space A. Remark in [Crawley] p. 120 line 21, but using a non-identity translation (nonzero vector) 
F whose trace is  P rather than  P itself;  F exists by cdlemf 30019. 
E is the division ring base by erngdv 30449, and  s `  F is the scalar product by dvavsca 30473. 
F must be a non-identity translation for the expression to be a 1-dimensional subspace, although the theorem doesn't require it. (Contributed by NM, 14-Oct-2013.)
 |-  .<_  =  ( le `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T ) 
 ->  { g  |  E. s  e.  E  g  =  ( s `  F ) }  =  {
 g  e.  T  |  ( R `  g ) 
 .<_  ( R `  F ) } )
 
Theoremdvhb1dimN 30442* Two expressions for the 1-dimensional subspaces of vector space H, in the isomorphism B case where the 2nd vector component is zero. (Contributed by NM, 23-Feb-2014.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  .0.  =  ( h  e.  T  |->  (  _I  |`  B )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T )  ->  { g  e.  ( T  X.  E )  |  E. s  e.  E  g  =  <. ( s `  F ) ,  .0.  >. }  =  { g  e.  ( T  X.  E )  |  ( ( R `  ( 1st `  g )
 )  .<_  ( R `  F )  /\  ( 2nd `  g )  =  .0.  ) } )
 
Theoremerng1lem 30443 Value of the endomorphism division ring unit. (Contributed by NM, 12-Oct-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  D  =  ( ( EDRing `  K ) `  W )   &    |-  (
 ( K  e.  HL  /\  W  e.  H ) 
 ->  D  e.  Ring )   =>    |-  (
 ( K  e.  HL  /\  W  e.  H ) 
 ->  ( 1r `  D )  =  (  _I  |`  T ) )
 
Theoremerngdvlem1 30444* Lemma for erngrng 30448. (Contributed by NM, 4-Aug-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing `  K ) `  W )   &    |-  B  =  ( Base `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  P  =  ( a  e.  E ,  b  e.  E  |->  ( f  e.  T  |->  ( ( a `  f )  o.  (
 b `  f )
 ) ) )   &    |-  .0.  =  ( f  e.  T  |->  (  _I  |`  B )
 )   &    |-  I  =  ( a  e.  E  |->  ( f  e.  T  |->  `' (
 a `  f )
 ) )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e.  Grp )
 
Theoremerngdvlem2N 30445* Lemma for erngrng 30448. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing `  K ) `  W )   &    |-  B  =  ( Base `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  P  =  ( a  e.  E ,  b  e.  E  |->  ( f  e.  T  |->  ( ( a `  f )  o.  (
 b `  f )
 ) ) )   &    |-  .0.  =  ( f  e.  T  |->  (  _I  |`  B )
 )   &    |-  I  =  ( a  e.  E  |->  ( f  e.  T  |->  `' (
 a `  f )
 ) )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e.  Abel )
 
Theoremerngdvlem3 30446* Lemma for erngrng 30448. (Contributed by NM, 6-Aug-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing `  K ) `  W )   &    |-  B  =  ( Base `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  P  =  ( a  e.  E ,  b  e.  E  |->  ( f  e.  T  |->  ( ( a `  f )  o.  (
 b `  f )
 ) ) )   &    |-  .0.  =  ( f  e.  T  |->  (  _I  |`  B )
 )   &    |-  I  =  ( a  e.  E  |->  ( f  e.  T  |->  `' (
 a `  f )
 ) )   &    |-  .+  =  (
 a  e.  E ,  b  e.  E  |->  ( a  o.  b ) )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e.  Ring )
 
Theoremerngdvlem4 30447* Lemma for erngdv 30449. (Contributed by NM, 11-Aug-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing `  K ) `  W )   &    |-  B  =  ( Base `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  P  =  ( a  e.  E ,  b  e.  E  |->  ( f  e.  T  |->  ( ( a `  f )  o.  (
 b `  f )
 ) ) )   &    |-  .0.  =  ( f  e.  T  |->  (  _I  |`  B )
 )   &    |-  I  =  ( a  e.  E  |->  ( f  e.  T  |->  `' (
 a `  f )
 ) )   &    |-  .+  =  (
 a  e.  E ,  b  e.  E  |->  ( a  o.  b ) )   &    |-  .\/ 
 =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Q  =  ( ( oc `  K ) `  W )   &    |-  Z  =  ( ( Q  .\/  ( R `  b ) )  ./\  ( ( h `  Q )  .\/  ( R `  ( b  o.  `' ( s `
  h ) ) ) ) )   &    |-  Y  =  ( ( Q  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  ( s `  h ) )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  Q )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if (
 ( s `  h )  =  h ,  g ,  X )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( h  e.  T  /\  h  =/=  (  _I  |`  B ) ) )  ->  D  e. 
 DivRing )
 
Theoremerngrng 30448 An endomorphism ring is a ring. Todo: fix comment. (Contributed by NM, 4-Aug-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing `  K ) `  W )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e.  Ring )
 
Theoremerngdv 30449 An endomorphism ring is a division ring. Todo: fix comment. (Contributed by NM, 11-Aug-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing `  K ) `  W )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e. 
 DivRing )
 
Theoremerng0g 30450* The division ring zero of an endomorphism ring. (Contributed by NM, 5-Nov-2013.) (Revised by Mario Carneiro, 23-Jun-2014.)
 |-  B  =  ( Base `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  D  =  ( ( EDRing `  K ) `  W )   &    |-  O  =  ( f  e.  T  |->  (  _I  |`  B )
 )   &    |- 
 .0.  =  ( 0g `  D )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  .0.  =  O )
 
Theoremerng1r 30451 The division ring unit of an endomorphism ring. (Contributed by NM, 5-Nov-2013.) (Revised by Mario Carneiro, 23-Jun-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  D  =  ( ( EDRing `  K ) `  W )   &    |-  .1.  =  ( 1r `  D )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  .1.  =  (  _I  |`  T ) )
 
Theoremerngdvlem1-rN 30452* Lemma for erngrng 30448. (Contributed by NM, 4-Aug-2013.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing R `  K ) `  W )   &    |-  B  =  ( Base `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  P  =  ( a  e.  E ,  b  e.  E  |->  ( f  e.  T  |->  ( ( a `  f )  o.  ( b `  f ) ) ) )   &    |-  O  =  ( f  e.  T  |->  (  _I  |`  B )
 )   &    |-  I  =  ( a  e.  E  |->  ( f  e.  T  |->  `' (
 a `  f )
 ) )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e.  Grp )
 
Theoremerngdvlem2-rN 30453* Lemma for erngrng 30448. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing R `  K ) `  W )   &    |-  B  =  ( Base `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  P  =  ( a  e.  E ,  b  e.  E  |->  ( f  e.  T  |->  ( ( a `  f )  o.  ( b `  f ) ) ) )   &    |-  O  =  ( f  e.  T  |->  (  _I  |`  B )
 )   &    |-  I  =  ( a  e.  E  |->  ( f  e.  T  |->  `' (
 a `  f )
 ) )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e.  Abel )
 
Theoremerngdvlem3-rN 30454* Lemma for erngrng 30448. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing R `  K ) `  W )   &    |-  B  =  ( Base `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  P  =  ( a  e.  E ,  b  e.  E  |->  ( f  e.  T  |->  ( ( a `  f )  o.  ( b `  f ) ) ) )   &    |-  O  =  ( f  e.  T  |->  (  _I  |`  B )
 )   &    |-  I  =  ( a  e.  E  |->  ( f  e.  T  |->  `' (
 a `  f )
 ) )   &    |-  M  =  ( a  e.  E ,  b  e.  E  |->  ( b  o.  a ) )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e.  Ring )
 
Theoremerngdvlem4-rN 30455* Lemma for erngdv 30449. (Contributed by NM, 11-Aug-2013.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing R `  K ) `  W )   &    |-  B  =  ( Base `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  P  =  ( a  e.  E ,  b  e.  E  |->  ( f  e.  T  |->  ( ( a `  f )  o.  ( b `  f ) ) ) )   &    |-  O  =  ( f  e.  T  |->  (  _I  |`  B )
 )   &    |-  I  =  ( a  e.  E  |->  ( f  e.  T  |->  `' (
 a `  f )
 ) )   &    |-  M  =  ( a  e.  E ,  b  e.  E  |->  ( b  o.  a ) )   &    |-  .\/ 
 =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  R  =  ( ( trL `  K ) `  W )   &    |-  Q  =  ( ( oc `  K ) `  W )   &    |-  Z  =  ( ( Q  .\/  ( R `  b ) )  ./\  ( ( h `  Q )  .\/  ( R `  ( b  o.  `' ( s `
  h ) ) ) ) )   &    |-  Y  =  ( ( Q  .\/  ( R `  g ) )  ./\  ( Z  .\/  ( R `  (
 g  o.  `' b
 ) ) ) )   &    |-  X  =  ( iota_ z  e.  T A. b  e.  T  ( ( b  =/=  (  _I  |`  B ) 
 /\  ( R `  b )  =/=  ( R `  ( s `  h ) )  /\  ( R `  b )  =/=  ( R `  g ) )  ->  ( z `  Q )  =  Y )
 )   &    |-  U  =  ( g  e.  T  |->  if (
 ( s `  h )  =  h ,  g ,  X )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( h  e.  T  /\  h  =/=  (  _I  |`  B ) ) )  ->  D  e. 
 DivRing )
 
Theoremerngrng-rN 30456 An endomorphism ring is a ring. Todo: fix comment. (Contributed by NM, 4-Aug-2013.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing R `  K ) `  W )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e.  Ring )
 
Theoremerngdv-rN 30457 An endomorphism ring is a division ring. Todo: fix comment. (Contributed by NM, 11-Aug-2013.) (New usage is discouraged.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing R `  K ) `  W )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e.  DivRing )
 
Syntaxcdveca 30458 Extend class notation with constructed vector space A.
 class  DVecA
 
Definitiondf-dveca 30459* Define constructed partial vector space A. (Contributed by NM, 8-Oct-2013.)
 |-  DVecA  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( { <. ( Base `  ndx ) ,  ( ( LTrn `  k
 ) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
 ) `  w ) ,  g  e.  (
 ( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
 >. ,  <. (Scalar `  ndx ) ,  ( ( EDRing `  k
 ) `  w ) >. }  u.  { <. ( .s `  ndx ) ,  ( s  e.  (
 ( TEndo `  k ) `  w ) ,  f  e.  ( ( LTrn `  k
 ) `  w )  |->  ( s `  f
 ) ) >. } )
 ) )
 
Theoremdvafset 30460* The constructed partial vector space A for a lattice  K. (Contributed by NM, 8-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
 |-  H  =  ( LHyp `  K )   =>    |-  ( K  e.  V  ->  (
 DVecA `  K )  =  ( w  e.  H  |->  ( { <. ( Base `  ndx ) ,  ( ( LTrn `  K ) `  w ) >. ,  <. (
 +g  `  ndx ) ,  ( f  e.  (
 ( LTrn `  K ) `  w ) ,  g  e.  ( ( LTrn `  K ) `  w )  |->  ( f  o.  g ) ) >. ,  <. (Scalar `  ndx ) ,  ( ( EDRing `
  K ) `  w ) >. }  u.  {
 <. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  K ) `  w ) ,  f  e.  ( (
 LTrn `  K ) `  w )  |->  ( s `
  f ) )
 >. } ) ) )
 
Theoremdvaset 30461* The constructed partial vector space A for a lattice  K. (Contributed by NM, 8-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  =  ( ( DVecA `  K ) `  W )   =>    |-  ( ( K  e.  X  /\  W  e.  H )  ->  U  =  ( { <. ( Base ` 
 ndx ) ,  T >. ,  <. ( +g  `  ndx ) ,  ( f  e.  T ,  g  e.  T  |->  ( f  o.  g ) ) >. , 
 <. (Scalar `  ndx ) ,  D >. }  u.  { <. ( .s `  ndx ) ,  ( s  e.  E ,  f  e.  T  |->  ( s `  f ) ) >. } ) )
 
Theoremdvasca 30462 The ring base set of the constructed partial vector space A are all translation group endomorphisms (for a fiducial co-atom  W). (Contributed by NM, 22-Jun-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  D  =  ( ( EDRing `  K ) `  W )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  F  =  (Scalar `  U )   =>    |-  (
 ( K  e.  X  /\  W  e.  H ) 
 ->  F  =  D )
 
Theoremdvabase 30463 The ring base set of the constructed partial vector space A are all translation group endomorphisms (for a fiducial co-atom  W). (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  F  =  (Scalar `  U )   &    |-  C  =  ( Base `  F )   =>    |-  (
 ( K  e.  X  /\  W  e.  H ) 
 ->  C  =  E )
 
Theoremdvafplusg 30464* Ring addition operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  F  =  (Scalar `  U )   &    |-  .+  =  ( +g  `  F )   =>    |-  (
 ( K  e.  V  /\  W  e.  H ) 
 ->  .+  =  ( s  e.  E ,  t  e.  E  |->  ( f  e.  T  |->  ( ( s `
  f )  o.  ( t `  f
 ) ) ) ) )
 
Theoremdvaplusg 30465* Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  F  =  (Scalar `  U )   &    |-  .+  =  ( +g  `  F )   =>    |-  (
 ( ( K  e.  V  /\  W  e.  H )  /\  ( R  e.  E  /\  S  e.  E ) )  ->  ( R 
 .+  S )  =  ( f  e.  T  |->  ( ( R `  f )  o.  ( S `  f ) ) ) )
 
Theoremdvaplusgv 30466 Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  F  =  (Scalar `  U )   &    |-  .+  =  ( +g  `  F )   =>    |-  (
 ( ( K  e.  V  /\  W  e.  H )  /\  ( R  e.  E  /\  S  e.  E  /\  G  e.  T ) )  ->  ( ( R  .+  S ) `  G )  =  (
 ( R `  G )  o.  ( S `  G ) ) )
 
Theoremdvafmulr 30467* Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  F  =  (Scalar `  U )   &    |-  .x.  =  ( .r `  F )   =>    |-  ( ( K  e.  V  /\  W  e.  H )  ->  .x.  =  (
 s  e.  E ,  t  e.  E  |->  ( s  o.  t ) ) )
 
Theoremdvamulr 30468 Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  U  =  ( ( DVecA `  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 ) )
 
Theoremdvavbase 30469 The vectors (vector base set) of the constructed partial vector space A are all translations (for a fiducial co-atom  W). (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  V  =  ( Base `  U )   =>    |-  (
 ( K  e.  X  /\  W  e.  H ) 
 ->  V  =  T )
 
Theoremdvafvadd 30470* The vector sum operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  .+  =  ( +g  `  U )   =>    |-  (
 ( K  e.  X  /\  W  e.  H ) 
 ->  .+  =  ( f  e.  T ,  g  e.  T  |->  ( f  o.  g ) ) )
 
Theoremdvavadd 30471 Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  .+  =  ( +g  `  U )   =>    |-  (
 ( ( K  e.  V  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T ) )  ->  ( F 
 .+  G )  =  ( F  o.  G ) )
 
Theoremdvafvsca 30472* Ring addition operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  .x.  =  ( .s `  U )   =>    |-  ( ( K  e.  V  /\  W  e.  H )  ->  .x.  =  (
 s  e.  E ,  f  e.  T  |->  ( s `
  f ) ) )
 
Theoremdvavsca 30473 Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  .x.  =  ( .s `  U )   =>    |-  ( ( ( K  e.  V  /\  W  e.  H )  /\  ( R  e.  E  /\  F  e.  T )
 )  ->  ( R  .x.  F )  =  ( R `  F ) )
 
Theoremtendospid 30474 Identity property of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
 |-  ( F  e.  T  ->  ( (  _I  |`  T ) `
  F )  =  F )
 
Theoremtendospcl 30475 Closure of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   =>    |-  ( ( ( K  e.  V  /\  W  e.  H )  /\  U  e.  E  /\  F  e.  T )  ->  ( U `  F )  e.  T )
 
Theoremtendospass 30476 Associative law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   =>    |-  ( ( ( K  e.  X  /\  W  e.  H )  /\  ( U  e.  E  /\  V  e.  E  /\  F  e.  T )
 )  ->  ( ( U  o.  V ) `  F )  =  ( U `  ( V `  F ) ) )
 
Theoremtendospdi1 30477 Forward distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   =>    |-  ( ( ( K  e.  V  /\  W  e.  H )  /\  ( U  e.  E  /\  F  e.  T  /\  G  e.  T )
 )  ->  ( U `  ( F  o.  G ) )  =  (
 ( U `  F )  o.  ( U `  G ) ) )
 
Theoremtendocnv 30478 Converse of a trace-preserving endomorphism value. (Contributed by NM, 7-Apr-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  S  e.  E  /\  F  e.  T )  ->  `' ( S `  F )  =  ( S `  `' F ) )
 
Theoremtendospdi2 30479* Reverse distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
 |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  P  =  ( s  e.  E ,  t  e.  E  |->  ( f  e.  T  |->  ( ( s `  f )  o.  (
 t `  f )
 ) ) )   =>    |-  ( ( U  e.  E  /\  V  e.  E  /\  F  e.  T )  ->  ( ( U P V ) `
  F )  =  ( ( U `  F )  o.  ( V `  F ) ) )
 
TheoremtendospcanN 30480* Cancellation law for trace-perserving endomorphism values (used as scalar product). (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  O  =  ( f  e.  T  |->  (  _I  |`  B )
 )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  e.  E  /\  S  =/=  O )  /\  ( F  e.  T  /\  G  e.  T ) )  ->  ( ( S `  F )  =  ( S `  G ) 
 <->  F  =  G ) )
 
Theoremdvaabl 30481 The constructed partial vector space A for a lattice  K is an abelian group. (Contributed by NM, 11-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecA `  K ) `  W )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  U  e.  Abel )
 
Theoremdvalveclem 30482 Lemma for dvalvec 30483. (Contributed by NM, 11-Oct-2013.) (Proof shortened by Mario Carneiro, 22-Jun-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  .+  =  ( +g  `  U )   &    |-  E  =  ( ( TEndo `  K ) `  W )   &    |-  D  =  (Scalar `  U )   &    |-  B  =  ( Base `  K )   &    |-  .+^  =  (
 +g  `  D )   &    |-  .X.  =  ( .r `  D )   &    |-  .x. 
 =  ( .s `  U )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  U  e.  LVec )
 
Theoremdvalvec 30483 The constructed partial vector space A for a lattice  K is a left vector space. (Contributed by NM, 11-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
 |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( DVecA `  K ) `  W )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  U  e.  LVec )
 
Theoremdva0g 30484 The zero vector of partial vector space A. (Contributed by NM, 9-Sep-2014.)
 |-  B  =  ( Base `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K ) `  W )   &    |-  U  =  ( ( DVecA `  K ) `  W )   &    |-  .0.  =  ( 0g `  U )   =>    |-  ( ( K  e.  HL  /\  W  e.  H )  ->  .0.  =  (  _I  |`  B ) )
 
Syntaxcdia 30485 Extend class notation with partial isomorphism A.
 class  DIsoA
 
Definitiondf-disoa 30486* Define partial isomorphism A. (Contributed by NM, 15-Oct-2013.)
 |-  DIsoA  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  { y  e.  ( Base `  k )  |  y ( le `  k
 ) w }  |->  { f  e.  ( (
 LTrn `  k ) `  w )  |  (
 ( ( trL `  k
 ) `  w ) `  f ) ( le `  k ) x }
 ) ) )
 
Theoremdiaffval 30487* The partial isomorphism A for a lattice  K. (Contributed by NM, 15-Oct-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  ( K  e.  V  ->  ( DIsoA `  K )  =  ( w  e.  H  |->  ( x  e.  { y  e.  B  |  y  .<_  w }  |->  { f  e.  (
 ( LTrn `  K ) `  w )  |  ( ( ( trL `  K ) `  w ) `  f )  .<_  x }
 ) ) )
 
Theoremdiafval 30488* The partial isomorphism A for a lattice  K. (Contributed by NM, 15-Oct-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  T  =  ( ( LTrn `  K