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

Theorem hdmap1eulemOLDN 35489
Description: Lemma for hdmap1euOLDN 35491. TODO: combine with hdmap1euOLDN 35491 or at least share some hypotheses. (Contributed by NM, 15-May-2015.) (New usage is discouraged.)
Hypotheses
Ref Expression
hdmap1eulem.h  |-  H  =  ( LHyp `  K
)
hdmap1eulem.u  |-  U  =  ( ( DVecH `  K
) `  W )
hdmap1eulem.v  |-  V  =  ( Base `  U
)
hdmap1eulem.s  |-  .-  =  ( -g `  U )
hdmap1eulem.o  |-  .0.  =  ( 0g `  U )
hdmap1eulem.n  |-  N  =  ( LSpan `  U )
hdmap1eulem.c  |-  C  =  ( (LCDual `  K
) `  W )
hdmap1eulem.d  |-  D  =  ( Base `  C
)
hdmap1eulem.r  |-  R  =  ( -g `  C
)
hdmap1eulem.q  |-  Q  =  ( 0g `  C
)
hdmap1eulem.j  |-  J  =  ( LSpan `  C )
hdmap1eulem.m  |-  M  =  ( (mapd `  K
) `  W )
hdmap1eulem.i  |-  I  =  ( (HDMap1 `  K
) `  W )
hdmap1eulem.k  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
hdmap1eulem.mn  |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )
hdmap1eulem.x  |-  ( ph  ->  X  e.  ( V 
\  {  .0.  }
) )
hdmap1eulem.f  |-  ( ph  ->  F  e.  D )
hdmap1eulem.y  |-  ( ph  ->  T  e.  V )
hdmap1eulem.l  |-  L  =  ( x  e.  _V  |->  if ( ( 2nd `  x
)  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `
 { ( 2nd `  x ) } ) )  =  ( J `
 { h }
)  /\  ( M `  ( N `  {
( ( 1st `  ( 1st `  x ) ) 
.-  ( 2nd `  x
) ) } ) )  =  ( J `
 { ( ( 2nd `  ( 1st `  x ) ) R h ) } ) ) ) ) )
Assertion
Ref Expression
hdmap1eulemOLDN  |-  ( ph  ->  E! y  e.  D  A. z  e.  V  ( -.  z  e.  ( N `  { X ,  T } )  -> 
y  =  ( I `
 <. z ,  ( I `  <. X ,  F ,  z >. ) ,  T >. )
) )
Distinct variable groups:    C, h    x, h, y, z, D   
h, F, x, y, z    h, J, x   
h, L, x, y, z    h, M, x   
h, N, x, y, z    .0. , h, x, y, z    x, Q    R, h, x    .- , h, x    T, h, x, y, z    U, h, z    h, V, y, z    h, X, x, y, z    ph, h, y, z
Allowed substitution hints:    ph( x)    C( x, y, z)    Q( y, z, h)    R( y,
z)    U( x, y)    H( x, y, z, h)    I( x, y, z, h)    J( y, z)    K( x, y, z, h)    M( y,
z)    .- ( y, z)    V( x)    W( x, y, z, h)

Proof of Theorem hdmap1eulemOLDN
StepHypRef Expression
1 hdmap1eulem.h . . 3  |-  H  =  ( LHyp `  K
)
2 hdmap1eulem.u . . 3  |-  U  =  ( ( DVecH `  K
) `  W )
3 hdmap1eulem.v . . 3  |-  V  =  ( Base `  U
)
4 hdmap1eulem.s . . 3  |-  .-  =  ( -g `  U )
5 hdmap1eulem.o . . 3  |-  .0.  =  ( 0g `  U )
6 hdmap1eulem.n . . 3  |-  N  =  ( LSpan `  U )
7 hdmap1eulem.c . . 3  |-  C  =  ( (LCDual `  K
) `  W )
8 hdmap1eulem.d . . 3  |-  D  =  ( Base `  C
)
9 hdmap1eulem.r . . 3  |-  R  =  ( -g `  C
)
10 hdmap1eulem.q . . 3  |-  Q  =  ( 0g `  C
)
11 hdmap1eulem.j . . 3  |-  J  =  ( LSpan `  C )
12 hdmap1eulem.m . . 3  |-  M  =  ( (mapd `  K
) `  W )
13 hdmap1eulem.l . . 3  |-  L  =  ( x  e.  _V  |->  if ( ( 2nd `  x
)  =  .0.  ,  Q ,  ( iota_ h  e.  D  ( ( M `  ( N `
 { ( 2nd `  x ) } ) )  =  ( J `
 { h }
)  /\  ( M `  ( N `  {
( ( 1st `  ( 1st `  x ) ) 
.-  ( 2nd `  x
) ) } ) )  =  ( J `
 { ( ( 2nd `  ( 1st `  x ) ) R h ) } ) ) ) ) )
14 hdmap1eulem.k . . 3  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
15 hdmap1eulem.f . . 3  |-  ( ph  ->  F  e.  D )
16 hdmap1eulem.mn . . 3  |-  ( ph  ->  ( M `  ( N `  { X } ) )  =  ( J `  { F } ) )
17 hdmap1eulem.x . . 3  |-  ( ph  ->  X  e.  ( V 
\  {  .0.  }
) )
18 hdmap1eulem.y . . 3  |-  ( ph  ->  T  e.  V )
191, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18mapdh9aOLDN 35455 . 2  |-  ( ph  ->  E! y  e.  D  A. z  e.  V  ( -.  z  e.  ( N `  { X ,  T } )  -> 
y  =  ( L `
 <. z ,  ( L `  <. X ,  F ,  z >. ) ,  T >. )
) )
20 hdmap1eulem.i . . . . . . . . . 10  |-  I  =  ( (HDMap1 `  K
) `  W )
2114ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
2217ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  ->  X  e.  ( V  \  {  .0.  } ) )
2315ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  ->  F  e.  D )
24 simplr 754 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
z  e.  V )
251, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 20, 21, 22, 23, 24, 13hdmap1valc 35468 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
( I `  <. X ,  F ,  z
>. )  =  ( L `  <. X ,  F ,  z >. ) )
26 oteq2 4084 . . . . . . . . 9  |-  ( ( I `  <. X ,  F ,  z >. )  =  ( L `  <. X ,  F , 
z >. )  ->  <. z ,  ( I `  <. X ,  F , 
z >. ) ,  T >.  =  <. z ,  ( L `  <. X ,  F ,  z >. ) ,  T >. )
2725, 26syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  ->  <. z ,  ( I `
 <. X ,  F ,  z >. ) ,  T >.  =  <. z ,  ( L `  <. X ,  F , 
z >. ) ,  T >. )
2827fveq2d 5710 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
( I `  <. z ,  ( I `  <. X ,  F , 
z >. ) ,  T >. )  =  ( I `
 <. z ,  ( L `  <. X ,  F ,  z >. ) ,  T >. )
)
29 eqid 2443 . . . . . . . . 9  |-  ( LSubSp `  U )  =  (
LSubSp `  U )
301, 2, 14dvhlmod 34774 . . . . . . . . . 10  |-  ( ph  ->  U  e.  LMod )
3130ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  ->  U  e.  LMod )
32 eldifi 3493 . . . . . . . . . . . 12  |-  ( X  e.  ( V  \  {  .0.  } )  ->  X  e.  V )
3317, 32syl 16 . . . . . . . . . . 11  |-  ( ph  ->  X  e.  V )
343, 29, 6, 30, 33, 18lspprcl 17074 . . . . . . . . . 10  |-  ( ph  ->  ( N `  { X ,  T }
)  e.  ( LSubSp `  U ) )
3534ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
( N `  { X ,  T }
)  e.  ( LSubSp `  U ) )
36 simpr 461 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  ->  -.  z  e.  ( N `  { X ,  T } ) )
373, 5, 29, 31, 35, 24, 36lssneln0 17048 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
z  e.  ( V 
\  {  .0.  }
) )
3816ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
( M `  ( N `  { X } ) )  =  ( J `  { F } ) )
391, 2, 14dvhlvec 34773 . . . . . . . . . . . . 13  |-  ( ph  ->  U  e.  LVec )
4039ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  ->  U  e.  LVec )
4133ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  ->  X  e.  V )
4218ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  ->  T  e.  V )
433, 6, 40, 24, 41, 42, 36lspindpi 17228 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
( ( N `  { z } )  =/=  ( N `  { X } )  /\  ( N `  { z } )  =/=  ( N `  { T } ) ) )
4443simpld 459 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
( N `  {
z } )  =/=  ( N `  { X } ) )
4544necomd 2710 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
( N `  { X } )  =/=  ( N `  { z } ) )
4610, 13, 1, 12, 2, 3, 4, 5, 6, 7, 8, 9, 11, 21, 23, 38, 22, 24, 45mapdhcl 35391 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
( L `  <. X ,  F ,  z
>. )  e.  D
)
471, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 20, 21, 37, 46, 42, 13hdmap1valc 35468 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
( I `  <. z ,  ( L `  <. X ,  F , 
z >. ) ,  T >. )  =  ( L `
 <. z ,  ( L `  <. X ,  F ,  z >. ) ,  T >. )
)
4828, 47eqtrd 2475 . . . . . 6  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
( I `  <. z ,  ( I `  <. X ,  F , 
z >. ) ,  T >. )  =  ( L `
 <. z ,  ( L `  <. X ,  F ,  z >. ) ,  T >. )
)
4948eqeq2d 2454 . . . . 5  |-  ( ( ( ph  /\  z  e.  V )  /\  -.  z  e.  ( N `  { X ,  T } ) )  -> 
( y  =  ( I `  <. z ,  ( I `  <. X ,  F , 
z >. ) ,  T >. )  <->  y  =  ( L `  <. z ,  ( L `  <. X ,  F , 
z >. ) ,  T >. ) ) )
5049pm5.74da 687 . . . 4  |-  ( (
ph  /\  z  e.  V )  ->  (
( -.  z  e.  ( N `  { X ,  T }
)  ->  y  =  ( I `  <. z ,  ( I `  <. X ,  F , 
z >. ) ,  T >. ) )  <->  ( -.  z  e.  ( N `  { X ,  T } )  ->  y  =  ( L `  <. z ,  ( L `
 <. X ,  F ,  z >. ) ,  T >. ) ) ) )
5150ralbidva 2746 . . 3  |-  ( ph  ->  ( A. z  e.  V  ( -.  z  e.  ( N `  { X ,  T }
)  ->  y  =  ( I `  <. z ,  ( I `  <. X ,  F , 
z >. ) ,  T >. ) )  <->  A. z  e.  V  ( -.  z  e.  ( N `  { X ,  T } )  ->  y  =  ( L `  <. z ,  ( L `
 <. X ,  F ,  z >. ) ,  T >. ) ) ) )
5251reubidv 2920 . 2  |-  ( ph  ->  ( E! y  e.  D  A. z  e.  V  ( -.  z  e.  ( N `  { X ,  T }
)  ->  y  =  ( I `  <. z ,  ( I `  <. X ,  F , 
z >. ) ,  T >. ) )  <->  E! y  e.  D  A. z  e.  V  ( -.  z  e.  ( N `  { X ,  T } )  ->  y  =  ( L `  <. z ,  ( L `
 <. X ,  F ,  z >. ) ,  T >. ) ) ) )
5319, 52mpbird 232 1  |-  ( ph  ->  E! y  e.  D  A. z  e.  V  ( -.  z  e.  ( N `  { X ,  T } )  -> 
y  =  ( I `
 <. z ,  ( I `  <. X ,  F ,  z >. ) ,  T >. )
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756    =/= wne 2620   A.wral 2730   E!wreu 2732   _Vcvv 2987    \ cdif 3340   ifcif 3806   {csn 3892   {cpr 3894   <.cotp 3900    e. cmpt 4365   ` cfv 5433   iota_crio 6066  (class class class)co 6106   1stc1st 6590   2ndc2nd 6591   Basecbs 14189   0gc0g 14393   -gcsg 15428   LModclmod 16963   LSubSpclss 17028   LSpanclspn 17067   LVecclvec 17198   HLchlt 33014   LHypclh 33647   DVecHcdvh 34742  LCDualclcd 35250  mapdcmpd 35288  HDMap1chdma1 35456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-cnex 9353  ax-resscn 9354  ax-1cn 9355  ax-icn 9356  ax-addcl 9357  ax-addrcl 9358  ax-mulcl 9359  ax-mulrcl 9360  ax-mulcom 9361  ax-addass 9362  ax-mulass 9363  ax-distr 9364  ax-i2m1 9365  ax-1ne0 9366  ax-1rid 9367  ax-rnegex 9368  ax-rrecex 9369  ax-cnre 9370  ax-pre-lttri 9371  ax-pre-lttrn 9372  ax-pre-ltadd 9373  ax-pre-mulgt0 9374  ax-riotaBAD 32623
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-pss 3359  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-tp 3897  df-op 3899  df-ot 3901  df-uni 4107  df-int 4144  df-iun 4188  df-iin 4189  df-br 4308  df-opab 4366  df-mpt 4367  df-tr 4401  df-eprel 4647  df-id 4651  df-po 4656  df-so 4657  df-fr 4694  df-we 4696  df-ord 4737  df-on 4738  df-lim 4739  df-suc 4740  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-of 6335  df-om 6492  df-1st 6592  df-2nd 6593  df-tpos 6760  df-undef 6807  df-recs 6847  df-rdg 6881  df-1o 6935  df-oadd 6939  df-er 7116  df-map 7231  df-en 7326  df-dom 7327  df-sdom 7328  df-fin 7329  df-pnf 9435  df-mnf 9436  df-xr 9437  df-ltxr 9438  df-le 9439  df-sub 9612  df-neg 9613  df-nn 10338  df-2 10395  df-3 10396  df-4 10397  df-5 10398  df-6 10399  df-n0 10595  df-z 10662  df-uz 10877  df-fz 11453  df-struct 14191  df-ndx 14192  df-slot 14193  df-base 14194  df-sets 14195  df-ress 14196  df-plusg 14266  df-mulr 14267  df-sca 14269  df-vsca 14270  df-0g 14395  df-mre 14539  df-mrc 14540  df-acs 14542  df-poset 15131  df-plt 15143  df-lub 15159  df-glb 15160  df-join 15161  df-meet 15162  df-p0 15224  df-p1 15225  df-lat 15231  df-clat 15293  df-mnd 15430  df-submnd 15480  df-grp 15560  df-minusg 15561  df-sbg 15562  df-subg 15693  df-cntz 15850  df-oppg 15876  df-lsm 16150  df-cmn 16294  df-abl 16295  df-mgp 16607  df-ur 16619  df-rng 16662  df-oppr 16730  df-dvdsr 16748  df-unit 16749  df-invr 16779  df-dvr 16790  df-drng 16849  df-lmod 16965  df-lss 17029  df-lsp 17068  df-lvec 17199  df-lsatoms 32640  df-lshyp 32641  df-lcv 32683  df-lfl 32722  df-lkr 32750  df-ldual 32788  df-oposet 32840  df-ol 32842  df-oml 32843  df-covers 32930  df-ats 32931  df-atl 32962  df-cvlat 32986  df-hlat 33015  df-llines 33161  df-lplanes 33162  df-lvols 33163  df-lines 33164  df-psubsp 33166  df-pmap 33167  df-padd 33459  df-lhyp 33651  df-laut 33652  df-ldil 33767  df-ltrn 33768  df-trl 33822  df-tgrp 34406  df-tendo 34418  df-edring 34420  df-dveca 34666  df-disoa 34693  df-dvech 34743  df-dib 34803  df-dic 34837  df-dih 34893  df-doch 35012  df-djh 35059  df-lcdual 35251  df-mapd 35289  df-hdmap1 35458
This theorem is referenced by:  hdmap1euOLDN  35491
  Copyright terms: Public domain W3C validator