Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lsat0cv Structured version   Unicode version

Theorem lsat0cv 34231
Description: A subspace is an atom iff it covers the zero subspace. This could serve as an alternate definition of an atom. TODO: this is a quick-and-dirty proof that could probably be more efficient. (Contributed by NM, 14-Mar-2015.)
Hypotheses
Ref Expression
lsat0cv.o  |-  .0.  =  ( 0g `  W )
lsat0cv.s  |-  S  =  ( LSubSp `  W )
lsat0cv.a  |-  A  =  (LSAtoms `  W )
lsat0cv.c  |-  C  =  (  <oLL  `  W )
lsat0cv.w  |-  ( ph  ->  W  e.  LVec )
lsat0cv.u  |-  ( ph  ->  U  e.  S )
Assertion
Ref Expression
lsat0cv  |-  ( ph  ->  ( U  e.  A  <->  {  .0.  } C U ) )

Proof of Theorem lsat0cv
Dummy variables  x  s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lsat0cv.o . . 3  |-  .0.  =  ( 0g `  W )
2 lsat0cv.a . . 3  |-  A  =  (LSAtoms `  W )
3 lsat0cv.c . . 3  |-  C  =  (  <oLL  `  W )
4 lsat0cv.w . . . 4  |-  ( ph  ->  W  e.  LVec )
54adantr 465 . . 3  |-  ( (
ph  /\  U  e.  A )  ->  W  e.  LVec )
6 simpr 461 . . 3  |-  ( (
ph  /\  U  e.  A )  ->  U  e.  A )
71, 2, 3, 5, 6lsatcv0 34229 . 2  |-  ( (
ph  /\  U  e.  A )  ->  {  .0.  } C U )
8 lsat0cv.s . . . . . . 7  |-  S  =  ( LSubSp `  W )
9 lveclmod 17623 . . . . . . . . 9  |-  ( W  e.  LVec  ->  W  e. 
LMod )
104, 9syl 16 . . . . . . . 8  |-  ( ph  ->  W  e.  LMod )
1110adantr 465 . . . . . . 7  |-  ( (
ph  /\  {  .0.  } C U )  ->  W  e.  LMod )
121, 8lsssn0 17465 . . . . . . . . 9  |-  ( W  e.  LMod  ->  {  .0.  }  e.  S )
1310, 12syl 16 . . . . . . . 8  |-  ( ph  ->  {  .0.  }  e.  S )
1413adantr 465 . . . . . . 7  |-  ( (
ph  /\  {  .0.  } C U )  ->  {  .0.  }  e.  S
)
15 lsat0cv.u . . . . . . . 8  |-  ( ph  ->  U  e.  S )
1615adantr 465 . . . . . . 7  |-  ( (
ph  /\  {  .0.  } C U )  ->  U  e.  S )
17 simpr 461 . . . . . . 7  |-  ( (
ph  /\  {  .0.  } C U )  ->  {  .0.  } C U )
188, 3, 11, 14, 16, 17lcvpss 34222 . . . . . 6  |-  ( (
ph  /\  {  .0.  } C U )  ->  {  .0.  }  C.  U
)
19 pssnel 3898 . . . . . 6  |-  ( {  .0.  }  C.  U  ->  E. x ( x  e.  U  /\  -.  x  e.  {  .0.  } ) )
2018, 19syl 16 . . . . 5  |-  ( (
ph  /\  {  .0.  } C U )  ->  E. x ( x  e.  U  /\  -.  x  e.  {  .0.  } ) )
2115ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  {  .0.  } C U )  /\  ( x  e.  U  /\  -.  x  e.  {  .0.  } ) )  ->  U  e.  S )
22 simprl 755 . . . . . . . . . . 11  |-  ( ( ( ph  /\  {  .0.  } C U )  /\  ( x  e.  U  /\  -.  x  e.  {  .0.  } ) )  ->  x  e.  U )
23 eqid 2467 . . . . . . . . . . . 12  |-  ( Base `  W )  =  (
Base `  W )
2423, 8lssel 17455 . . . . . . . . . . 11  |-  ( ( U  e.  S  /\  x  e.  U )  ->  x  e.  ( Base `  W ) )
2521, 22, 24syl2anc 661 . . . . . . . . . 10  |-  ( ( ( ph  /\  {  .0.  } C U )  /\  ( x  e.  U  /\  -.  x  e.  {  .0.  } ) )  ->  x  e.  ( Base `  W )
)
26 elsn 4047 . . . . . . . . . . . . . 14  |-  ( x  e.  {  .0.  }  <->  x  =  .0.  )
2726biimpri 206 . . . . . . . . . . . . 13  |-  ( x  =  .0.  ->  x  e.  {  .0.  } )
2827necon3bi 2696 . . . . . . . . . . . 12  |-  ( -.  x  e.  {  .0.  }  ->  x  =/=  .0.  )
2928adantl 466 . . . . . . . . . . 11  |-  ( ( x  e.  U  /\  -.  x  e.  {  .0.  } )  ->  x  =/=  .0.  )
3029adantl 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  {  .0.  } C U )  /\  ( x  e.  U  /\  -.  x  e.  {  .0.  } ) )  ->  x  =/=  .0.  )
31 eldifsn 4158 . . . . . . . . . 10  |-  ( x  e.  ( ( Base `  W )  \  {  .0.  } )  <->  ( x  e.  ( Base `  W
)  /\  x  =/=  .0.  ) )
3225, 30, 31sylanbrc 664 . . . . . . . . 9  |-  ( ( ( ph  /\  {  .0.  } C U )  /\  ( x  e.  U  /\  -.  x  e.  {  .0.  } ) )  ->  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )
3332, 22jca 532 . . . . . . . 8  |-  ( ( ( ph  /\  {  .0.  } C U )  /\  ( x  e.  U  /\  -.  x  e.  {  .0.  } ) )  ->  ( x  e.  ( ( Base `  W
)  \  {  .0.  } )  /\  x  e.  U ) )
3433ex 434 . . . . . . 7  |-  ( (
ph  /\  {  .0.  } C U )  -> 
( ( x  e.  U  /\  -.  x  e.  {  .0.  } )  ->  ( x  e.  ( ( Base `  W
)  \  {  .0.  } )  /\  x  e.  U ) ) )
3534eximdv 1686 . . . . . 6  |-  ( (
ph  /\  {  .0.  } C U )  -> 
( E. x ( x  e.  U  /\  -.  x  e.  {  .0.  } )  ->  E. x
( x  e.  ( ( Base `  W
)  \  {  .0.  } )  /\  x  e.  U ) ) )
36 df-rex 2823 . . . . . 6  |-  ( E. x  e.  ( (
Base `  W )  \  {  .0.  } ) x  e.  U  <->  E. x
( x  e.  ( ( Base `  W
)  \  {  .0.  } )  /\  x  e.  U ) )
3735, 36syl6ibr 227 . . . . 5  |-  ( (
ph  /\  {  .0.  } C U )  -> 
( E. x ( x  e.  U  /\  -.  x  e.  {  .0.  } )  ->  E. x  e.  ( ( Base `  W
)  \  {  .0.  } ) x  e.  U
) )
3820, 37mpd 15 . . . 4  |-  ( (
ph  /\  {  .0.  } C U )  ->  E. x  e.  (
( Base `  W )  \  {  .0.  } ) x  e.  U )
39 simpllr 758 . . . . . . . 8  |-  ( ( ( ( ph  /\  {  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  ->  {  .0.  } C U )
408, 3, 4, 13, 15lcvbr2 34220 . . . . . . . . . . 11  |-  ( ph  ->  ( {  .0.  } C U  <->  ( {  .0.  } 
C.  U  /\  A. s  e.  S  (
( {  .0.  }  C.  s  /\  s  C_  U )  ->  s  =  U ) ) ) )
4140adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  {  .0.  } C U )  -> 
( {  .0.  } C U  <->  ( {  .0.  } 
C.  U  /\  A. s  e.  S  (
( {  .0.  }  C.  s  /\  s  C_  U )  ->  s  =  U ) ) ) )
4241ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ( ph  /\  {  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  ->  ( {  .0.  } C U  <-> 
( {  .0.  }  C.  U  /\  A. s  e.  S  ( ( {  .0.  }  C.  s  /\  s  C_  U )  ->  s  =  U ) ) ) )
4310ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  {  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  ->  W  e.  LMod )
4443ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  W  e.  LMod )
45 eldifi 3631 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( Base `  W )  \  {  .0.  } )  ->  x  e.  ( Base `  W
) )
4645adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  {  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  ->  x  e.  ( Base `  W
) )
4746ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  x  e.  ( Base `  W ) )
48 eqid 2467 . . . . . . . . . . . . . . . 16  |-  ( LSpan `  W )  =  (
LSpan `  W )
4923, 8, 48lspsncl 17494 . . . . . . . . . . . . . . 15  |-  ( ( W  e.  LMod  /\  x  e.  ( Base `  W
) )  ->  (
( LSpan `  W ) `  { x } )  e.  S )
5044, 47, 49syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  ( ( LSpan `  W
) `  { x } )  e.  S
)
511, 8lss0ss 17466 . . . . . . . . . . . . . 14  |-  ( ( W  e.  LMod  /\  (
( LSpan `  W ) `  { x } )  e.  S )  ->  {  .0.  }  C_  (
( LSpan `  W ) `  { x } ) )
5244, 50, 51syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  {  .0.  }  C_  ( ( LSpan `  W
) `  { x } ) )
53 eldifsni 4159 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( Base `  W )  \  {  .0.  } )  ->  x  =/=  .0.  )
5453adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  {  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  ->  x  =/=  .0.  )
5554ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  x  =/=  .0.  )
5623, 1, 48lspsneq0 17529 . . . . . . . . . . . . . . . . 17  |-  ( ( W  e.  LMod  /\  x  e.  ( Base `  W
) )  ->  (
( ( LSpan `  W
) `  { x } )  =  {  .0.  }  <->  x  =  .0.  ) )
5744, 47, 56syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  ( ( ( LSpan `  W ) `  {
x } )  =  {  .0.  }  <->  x  =  .0.  ) )
5857necon3bid 2725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  ( ( ( LSpan `  W ) `  {
x } )  =/= 
{  .0.  }  <->  x  =/=  .0.  ) )
5955, 58mpbird 232 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  ( ( LSpan `  W
) `  { x } )  =/=  {  .0.  } )
6059necomd 2738 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  {  .0.  }  =/=  ( ( LSpan `  W
) `  { x } ) )
61 df-pss 3497 . . . . . . . . . . . . 13  |-  ( {  .0.  }  C.  (
( LSpan `  W ) `  { x } )  <-> 
( {  .0.  }  C_  ( ( LSpan `  W
) `  { x } )  /\  {  .0.  }  =/=  ( (
LSpan `  W ) `  { x } ) ) )
6252, 60, 61sylanbrc 664 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  {  .0.  }  C.  ( ( LSpan `  W
) `  { x } ) )
6315ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  {  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  ->  U  e.  S )
6463ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  U  e.  S )
65 simplr 754 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  x  e.  U )
668, 48, 44, 64, 65lspsnel5a 17513 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  ( ( LSpan `  W
) `  { x } )  C_  U
)
6762, 66jca 532 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  ( {  .0.  }  C.  ( ( LSpan `  W
) `  { x } )  /\  (
( LSpan `  W ) `  { x } ) 
C_  U ) )
68 psseq2 3597 . . . . . . . . . . . . . . 15  |-  ( s  =  ( ( LSpan `  W ) `  {
x } )  -> 
( {  .0.  }  C.  s  <->  {  .0.  }  C.  ( ( LSpan `  W
) `  { x } ) ) )
69 sseq1 3530 . . . . . . . . . . . . . . 15  |-  ( s  =  ( ( LSpan `  W ) `  {
x } )  -> 
( s  C_  U  <->  ( ( LSpan `  W ) `  { x } ) 
C_  U ) )
7068, 69anbi12d 710 . . . . . . . . . . . . . 14  |-  ( s  =  ( ( LSpan `  W ) `  {
x } )  -> 
( ( {  .0.  } 
C.  s  /\  s  C_  U )  <->  ( {  .0.  }  C.  ( ( LSpan `  W ) `  { x } )  /\  ( ( LSpan `  W ) `  {
x } )  C_  U ) ) )
71 eqeq1 2471 . . . . . . . . . . . . . 14  |-  ( s  =  ( ( LSpan `  W ) `  {
x } )  -> 
( s  =  U  <-> 
( ( LSpan `  W
) `  { x } )  =  U ) )
7270, 71imbi12d 320 . . . . . . . . . . . . 13  |-  ( s  =  ( ( LSpan `  W ) `  {
x } )  -> 
( ( ( {  .0.  }  C.  s  /\  s  C_  U )  ->  s  =  U )  <->  ( ( {  .0.  }  C.  (
( LSpan `  W ) `  { x } )  /\  ( ( LSpan `  W ) `  {
x } )  C_  U )  ->  (
( LSpan `  W ) `  { x } )  =  U ) ) )
7372rspcv 3215 . . . . . . . . . . . 12  |-  ( ( ( LSpan `  W ) `  { x } )  e.  S  ->  ( A. s  e.  S  ( ( {  .0.  } 
C.  s  /\  s  C_  U )  ->  s  =  U )  ->  (
( {  .0.  }  C.  ( ( LSpan `  W
) `  { x } )  /\  (
( LSpan `  W ) `  { x } ) 
C_  U )  -> 
( ( LSpan `  W
) `  { x } )  =  U ) ) )
7450, 73syl 16 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  ( A. s  e.  S  ( ( {  .0.  }  C.  s  /\  s  C_  U )  ->  s  =  U )  ->  ( ( {  .0.  }  C.  (
( LSpan `  W ) `  { x } )  /\  ( ( LSpan `  W ) `  {
x } )  C_  U )  ->  (
( LSpan `  W ) `  { x } )  =  U ) ) )
7567, 74mpid 41 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\ 
{  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  /\  {  .0.  }  C.  U )  ->  ( A. s  e.  S  ( ( {  .0.  }  C.  s  /\  s  C_  U )  ->  s  =  U )  ->  ( ( LSpan `  W ) `  { x } )  =  U ) )
7675expimpd 603 . . . . . . . . 9  |-  ( ( ( ( ph  /\  {  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  ->  (
( {  .0.  }  C.  U  /\  A. s  e.  S  ( ( {  .0.  }  C.  s  /\  s  C_  U )  ->  s  =  U ) )  ->  (
( LSpan `  W ) `  { x } )  =  U ) )
7742, 76sylbid 215 . . . . . . . 8  |-  ( ( ( ( ph  /\  {  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  ->  ( {  .0.  } C U  ->  ( ( LSpan `  W ) `  {
x } )  =  U ) )
7839, 77mpd 15 . . . . . . 7  |-  ( ( ( ( ph  /\  {  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  ->  (
( LSpan `  W ) `  { x } )  =  U )
7978eqcomd 2475 . . . . . 6  |-  ( ( ( ( ph  /\  {  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  /\  x  e.  U )  ->  U  =  ( ( LSpan `  W ) `  {
x } ) )
8079ex 434 . . . . 5  |-  ( ( ( ph  /\  {  .0.  } C U )  /\  x  e.  ( ( Base `  W
)  \  {  .0.  } ) )  ->  (
x  e.  U  ->  U  =  ( ( LSpan `  W ) `  { x } ) ) )
8180reximdva 2942 . . . 4  |-  ( (
ph  /\  {  .0.  } C U )  -> 
( E. x  e.  ( ( Base `  W
)  \  {  .0.  } ) x  e.  U  ->  E. x  e.  ( ( Base `  W
)  \  {  .0.  } ) U  =  ( ( LSpan `  W ) `  { x } ) ) )
8238, 81mpd 15 . . 3  |-  ( (
ph  /\  {  .0.  } C U )  ->  E. x  e.  (
( Base `  W )  \  {  .0.  } ) U  =  ( (
LSpan `  W ) `  { x } ) )
834adantr 465 . . . 4  |-  ( (
ph  /\  {  .0.  } C U )  ->  W  e.  LVec )
8423, 48, 1, 2islsat 34189 . . . 4  |-  ( W  e.  LVec  ->  ( U  e.  A  <->  E. x  e.  ( ( Base `  W
)  \  {  .0.  } ) U  =  ( ( LSpan `  W ) `  { x } ) ) )
8583, 84syl 16 . . 3  |-  ( (
ph  /\  {  .0.  } C U )  -> 
( U  e.  A  <->  E. x  e.  ( (
Base `  W )  \  {  .0.  } ) U  =  ( (
LSpan `  W ) `  { x } ) ) )
8682, 85mpbird 232 . 2  |-  ( (
ph  /\  {  .0.  } C U )  ->  U  e.  A )
877, 86impbida 830 1  |-  ( ph  ->  ( U  e.  A  <->  {  .0.  } C U ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379   E.wex 1596    e. wcel 1767    =/= wne 2662   A.wral 2817   E.wrex 2818    \ cdif 3478    C_ wss 3481    C. wpss 3482   {csn 4033   class class class wbr 4453   ` cfv 5594   Basecbs 14507   0gc0g 14712   LModclmod 17383   LSubSpclss 17449   LSpanclspn 17488   LVecclvec 17619  LSAtomsclsa 34172    <oLL clcv 34216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-1st 6795  df-2nd 6796  df-tpos 6967  df-recs 7054  df-rdg 7088  df-er 7323  df-en 7529  df-dom 7530  df-sdom 7531  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-nn 10549  df-2 10606  df-3 10607  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-ress 14514  df-plusg 14585  df-mulr 14586  df-0g 14714  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-grp 15929  df-minusg 15930  df-sbg 15931  df-cmn 16673  df-abl 16674  df-mgp 17014  df-ur 17026  df-ring 17072  df-oppr 17144  df-dvdsr 17162  df-unit 17163  df-invr 17193  df-drng 17269  df-lmod 17385  df-lss 17450  df-lsp 17489  df-lvec 17620  df-lsatoms 34174  df-lcv 34217
This theorem is referenced by:  mapdcnvatN  36864  mapdat  36865
  Copyright terms: Public domain W3C validator