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

Theorem lcfrlem26 37747
Description: Lemma for lcfr 37764. Special case of lcfrlem36 37757 when  ( ( J `
 Y ) `  I ) is zero. (Contributed by NM, 11-Mar-2015.)
Hypotheses
Ref Expression
lcfrlem17.h  |-  H  =  ( LHyp `  K
)
lcfrlem17.o  |-  ._|_  =  ( ( ocH `  K
) `  W )
lcfrlem17.u  |-  U  =  ( ( DVecH `  K
) `  W )
lcfrlem17.v  |-  V  =  ( Base `  U
)
lcfrlem17.p  |-  .+  =  ( +g  `  U )
lcfrlem17.z  |-  .0.  =  ( 0g `  U )
lcfrlem17.n  |-  N  =  ( LSpan `  U )
lcfrlem17.a  |-  A  =  (LSAtoms `  U )
lcfrlem17.k  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
lcfrlem17.x  |-  ( ph  ->  X  e.  ( V 
\  {  .0.  }
) )
lcfrlem17.y  |-  ( ph  ->  Y  e.  ( V 
\  {  .0.  }
) )
lcfrlem17.ne  |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )
lcfrlem22.b  |-  B  =  ( ( N `  { X ,  Y }
)  i^i  (  ._|_  `  { ( X  .+  Y ) } ) )
lcfrlem24.t  |-  .x.  =  ( .s `  U )
lcfrlem24.s  |-  S  =  (Scalar `  U )
lcfrlem24.q  |-  Q  =  ( 0g `  S
)
lcfrlem24.r  |-  R  =  ( Base `  S
)
lcfrlem24.j  |-  J  =  ( x  e.  ( V  \  {  .0.  } )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
k  .x.  x )
) ) ) )
lcfrlem24.ib  |-  ( ph  ->  I  e.  B )
lcfrlem24.l  |-  L  =  (LKer `  U )
lcfrlem25.d  |-  D  =  (LDual `  U )
lcfrlem25.jz  |-  ( ph  ->  ( ( J `  Y ) `  I
)  =  Q )
lcfrlem25.in  |-  ( ph  ->  I  =/=  .0.  )
Assertion
Ref Expression
lcfrlem26  |-  ( ph  ->  ( X  .+  Y
)  e.  (  ._|_  `  ( L `  ( J `  Y )
) ) )
Distinct variable groups:    v, k, w, x,  ._|_    .+ , k, v, w, x    R, k, v, x    S, k    .x. , k, v, w, x   
v, V, x    k, X, v, w, x    k, Y, v, w, x    x,  .0.
Allowed substitution hints:    ph( x, w, v, k)    A( x, w, v, k)    B( x, w, v, k)    D( x, w, v, k)    Q( x, w, v, k)    R( w)    S( x, w, v)    U( x, w, v, k)    H( x, w, v, k)    I( x, w, v, k)    J( x, w, v, k)    K( x, w, v, k)    L( x, w, v, k)    N( x, w, v, k)    V( w, k)    W( x, w, v, k)    .0. ( w, v, k)

Proof of Theorem lcfrlem26
Dummy variable  f is distinct from all other variables.
StepHypRef Expression
1 lcfrlem17.h . . . . 5  |-  H  =  ( LHyp `  K
)
2 lcfrlem17.u . . . . 5  |-  U  =  ( ( DVecH `  K
) `  W )
3 lcfrlem17.o . . . . 5  |-  ._|_  =  ( ( ocH `  K
) `  W )
4 lcfrlem17.v . . . . 5  |-  V  =  ( Base `  U
)
5 lcfrlem17.n . . . . 5  |-  N  =  ( LSpan `  U )
6 lcfrlem17.k . . . . 5  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
7 lcfrlem17.p . . . . . . 7  |-  .+  =  ( +g  `  U )
8 lcfrlem17.z . . . . . . 7  |-  .0.  =  ( 0g `  U )
9 lcfrlem17.a . . . . . . 7  |-  A  =  (LSAtoms `  U )
10 lcfrlem17.x . . . . . . 7  |-  ( ph  ->  X  e.  ( V 
\  {  .0.  }
) )
11 lcfrlem17.y . . . . . . 7  |-  ( ph  ->  Y  e.  ( V 
\  {  .0.  }
) )
12 lcfrlem17.ne . . . . . . 7  |-  ( ph  ->  ( N `  { X } )  =/=  ( N `  { Y } ) )
131, 3, 2, 4, 7, 8, 5, 9, 6, 10, 11, 12lcfrlem17 37738 . . . . . 6  |-  ( ph  ->  ( X  .+  Y
)  e.  ( V 
\  {  .0.  }
) )
1413eldifad 3418 . . . . 5  |-  ( ph  ->  ( X  .+  Y
)  e.  V )
151, 2, 3, 4, 5, 6, 14dochocsn 37560 . . . 4  |-  ( ph  ->  (  ._|_  `  (  ._|_  `  { ( X  .+  Y ) } ) )  =  ( N `
 { ( X 
.+  Y ) } ) )
16 lcfrlem22.b . . . . . 6  |-  B  =  ( ( N `  { X ,  Y }
)  i^i  (  ._|_  `  { ( X  .+  Y ) } ) )
17 lcfrlem24.t . . . . . 6  |-  .x.  =  ( .s `  U )
18 lcfrlem24.s . . . . . 6  |-  S  =  (Scalar `  U )
19 lcfrlem24.q . . . . . 6  |-  Q  =  ( 0g `  S
)
20 lcfrlem24.r . . . . . 6  |-  R  =  ( Base `  S
)
21 lcfrlem24.j . . . . . 6  |-  J  =  ( x  e.  ( V  \  {  .0.  } )  |->  ( v  e.  V  |->  ( iota_ k  e.  R  E. w  e.  (  ._|_  `  { x } ) v  =  ( w  .+  (
k  .x.  x )
) ) ) )
22 lcfrlem24.ib . . . . . 6  |-  ( ph  ->  I  e.  B )
23 lcfrlem24.l . . . . . 6  |-  L  =  (LKer `  U )
24 lcfrlem25.d . . . . . 6  |-  D  =  (LDual `  U )
25 lcfrlem25.jz . . . . . 6  |-  ( ph  ->  ( ( J `  Y ) `  I
)  =  Q )
26 lcfrlem25.in . . . . . 6  |-  ( ph  ->  I  =/=  .0.  )
271, 3, 2, 4, 7, 8, 5, 9, 6, 10, 11, 12, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26lcfrlem25 37746 . . . . 5  |-  ( ph  ->  (  ._|_  `  { ( X  .+  Y ) } )  =  ( L `  ( J `
 Y ) ) )
2827fveq2d 5795 . . . 4  |-  ( ph  ->  (  ._|_  `  (  ._|_  `  { ( X  .+  Y ) } ) )  =  (  ._|_  `  ( L `  ( J `  Y )
) ) )
2915, 28eqtr3d 2439 . . 3  |-  ( ph  ->  ( N `  {
( X  .+  Y
) } )  =  (  ._|_  `  ( L `
 ( J `  Y ) ) ) )
30 eqimss 3486 . . 3  |-  ( ( N `  { ( X  .+  Y ) } )  =  ( 
._|_  `  ( L `  ( J `  Y ) ) )  ->  ( N `  { ( X  .+  Y ) } )  C_  (  ._|_  `  ( L `  ( J `  Y )
) ) )
3129, 30syl 16 . 2  |-  ( ph  ->  ( N `  {
( X  .+  Y
) } )  C_  (  ._|_  `  ( L `  ( J `  Y
) ) ) )
32 eqid 2396 . . 3  |-  ( LSubSp `  U )  =  (
LSubSp `  U )
331, 2, 6dvhlmod 37289 . . 3  |-  ( ph  ->  U  e.  LMod )
34 eqid 2396 . . . . 5  |-  (LFnl `  U )  =  (LFnl `  U )
35 eqid 2396 . . . . . 6  |-  ( 0g
`  D )  =  ( 0g `  D
)
36 eqid 2396 . . . . . 6  |-  { f  e.  (LFnl `  U
)  |  (  ._|_  `  (  ._|_  `  ( L `
 f ) ) )  =  ( L `
 f ) }  =  { f  e.  (LFnl `  U )  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }
371, 3, 2, 4, 7, 17, 18, 20, 8, 34, 23, 24, 35, 36, 21, 6, 11lcfrlem10 37731 . . . . 5  |-  ( ph  ->  ( J `  Y
)  e.  (LFnl `  U ) )
384, 34, 23, 33, 37lkrssv 35273 . . . 4  |-  ( ph  ->  ( L `  ( J `  Y )
)  C_  V )
391, 2, 4, 32, 3dochlss 37533 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( L `  ( J `  Y ) )  C_  V )  ->  (  ._|_  `  ( L `
 ( J `  Y ) ) )  e.  ( LSubSp `  U
) )
406, 38, 39syl2anc 659 . . 3  |-  ( ph  ->  (  ._|_  `  ( L `
 ( J `  Y ) ) )  e.  ( LSubSp `  U
) )
414, 32, 5, 33, 40, 14lspsnel5 17777 . 2  |-  ( ph  ->  ( ( X  .+  Y )  e.  ( 
._|_  `  ( L `  ( J `  Y ) ) )  <->  ( N `  { ( X  .+  Y ) } ) 
C_  (  ._|_  `  ( L `  ( J `  Y ) ) ) ) )
4231, 41mpbird 232 1  |-  ( ph  ->  ( X  .+  Y
)  e.  (  ._|_  `  ( L `  ( J `  Y )
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1399    e. wcel 1836    =/= wne 2591   E.wrex 2747   {crab 2750    \ cdif 3403    i^i cin 3405    C_ wss 3406   {csn 3961   {cpr 3963    |-> cmpt 4442   ` cfv 5513   iota_crio 6179  (class class class)co 6218   Basecbs 14657   +g cplusg 14725  Scalarcsca 14728   .scvsca 14729   0gc0g 14870   LSubSpclss 17714   LSpanclspn 17753  LSAtomsclsa 35151  LFnlclfn 35234  LKerclk 35262  LDualcld 35300   HLchlt 35527   LHypclh 36160   DVecHcdvh 37257   ocHcoch 37526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-rep 4495  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-cnex 9481  ax-resscn 9482  ax-1cn 9483  ax-icn 9484  ax-addcl 9485  ax-addrcl 9486  ax-mulcl 9487  ax-mulrcl 9488  ax-mulcom 9489  ax-addass 9490  ax-mulass 9491  ax-distr 9492  ax-i2m1 9493  ax-1ne0 9494  ax-1rid 9495  ax-rnegex 9496  ax-rrecex 9497  ax-cnre 9498  ax-pre-lttri 9499  ax-pre-lttrn 9500  ax-pre-ltadd 9501  ax-pre-mulgt0 9502  ax-riotaBAD 35136
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-fal 1405  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-nel 2594  df-ral 2751  df-rex 2752  df-reu 2753  df-rmo 2754  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4181  df-int 4217  df-iun 4262  df-iin 4263  df-br 4385  df-opab 4443  df-mpt 4444  df-tr 4478  df-eprel 4722  df-id 4726  df-po 4731  df-so 4732  df-fr 4769  df-we 4771  df-ord 4812  df-on 4813  df-lim 4814  df-suc 4815  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-riota 6180  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-of 6461  df-om 6622  df-1st 6721  df-2nd 6722  df-tpos 6895  df-undef 6942  df-recs 6982  df-rdg 7016  df-1o 7070  df-oadd 7074  df-er 7251  df-map 7362  df-en 7458  df-dom 7459  df-sdom 7460  df-fin 7461  df-pnf 9563  df-mnf 9564  df-xr 9565  df-ltxr 9566  df-le 9567  df-sub 9742  df-neg 9743  df-nn 10475  df-2 10533  df-3 10534  df-4 10535  df-5 10536  df-6 10537  df-n0 10735  df-z 10804  df-uz 11024  df-fz 11616  df-struct 14659  df-ndx 14660  df-slot 14661  df-base 14662  df-sets 14663  df-ress 14664  df-plusg 14738  df-mulr 14739  df-sca 14741  df-vsca 14742  df-0g 14872  df-mre 15016  df-mrc 15017  df-acs 15019  df-preset 15697  df-poset 15715  df-plt 15728  df-lub 15744  df-glb 15745  df-join 15746  df-meet 15747  df-p0 15809  df-p1 15810  df-lat 15816  df-clat 15878  df-mgm 16012  df-sgrp 16051  df-mnd 16061  df-submnd 16107  df-grp 16197  df-minusg 16198  df-sbg 16199  df-subg 16338  df-cntz 16495  df-oppg 16521  df-lsm 16796  df-cmn 16940  df-abl 16941  df-mgp 17278  df-ur 17290  df-ring 17336  df-oppr 17408  df-dvdsr 17426  df-unit 17427  df-invr 17457  df-dvr 17468  df-drng 17534  df-lmod 17650  df-lss 17715  df-lsp 17754  df-lvec 17885  df-lsatoms 35153  df-lshyp 35154  df-lcv 35196  df-lfl 35235  df-lkr 35263  df-ldual 35301  df-oposet 35353  df-ol 35355  df-oml 35356  df-covers 35443  df-ats 35444  df-atl 35475  df-cvlat 35499  df-hlat 35528  df-llines 35674  df-lplanes 35675  df-lvols 35676  df-lines 35677  df-psubsp 35679  df-pmap 35680  df-padd 35972  df-lhyp 36164  df-laut 36165  df-ldil 36280  df-ltrn 36281  df-trl 36336  df-tgrp 36921  df-tendo 36933  df-edring 36935  df-dveca 37181  df-disoa 37208  df-dvech 37258  df-dib 37318  df-dic 37352  df-dih 37408  df-doch 37527  df-djh 37574
This theorem is referenced by:  lcfrlem27  37748
  Copyright terms: Public domain W3C validator