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

Theorem lcfrlem1 36740
Description: Lemma for lcfr 36783. Note that  X is z in Mario's notes. (Contributed by NM, 27-Feb-2015.)
Hypotheses
Ref Expression
lcfrlem1.v  |-  V  =  ( Base `  U
)
lcfrlem1.s  |-  S  =  (Scalar `  U )
lcfrlem1.q  |-  .X.  =  ( .r `  S )
lcfrlem1.z  |-  .0.  =  ( 0g `  S )
lcfrlem1.i  |-  I  =  ( invr `  S
)
lcfrlem1.f  |-  F  =  (LFnl `  U )
lcfrlem1.d  |-  D  =  (LDual `  U )
lcfrlem1.t  |-  .x.  =  ( .s `  D )
lcfrlem1.m  |-  .-  =  ( -g `  D )
lcfrlem1.u  |-  ( ph  ->  U  e.  LVec )
lcfrlem1.e  |-  ( ph  ->  E  e.  F )
lcfrlem1.g  |-  ( ph  ->  G  e.  F )
lcfrlem1.x  |-  ( ph  ->  X  e.  V )
lcfrlem1.n  |-  ( ph  ->  ( G `  X
)  =/=  .0.  )
lcfrlem1.h  |-  H  =  ( E  .-  (
( ( I `  ( G `  X ) )  .X.  ( E `  X ) )  .x.  G ) )
Assertion
Ref Expression
lcfrlem1  |-  ( ph  ->  ( H `  X
)  =  .0.  )

Proof of Theorem lcfrlem1
StepHypRef Expression
1 lcfrlem1.h . . 3  |-  H  =  ( E  .-  (
( ( I `  ( G `  X ) )  .X.  ( E `  X ) )  .x.  G ) )
21fveq1i 5873 . 2  |-  ( H `
 X )  =  ( ( E  .-  ( ( ( I `
 ( G `  X ) )  .X.  ( E `  X ) )  .x.  G ) ) `  X )
3 lcfrlem1.v . . . 4  |-  V  =  ( Base `  U
)
4 lcfrlem1.s . . . 4  |-  S  =  (Scalar `  U )
5 eqid 2467 . . . 4  |-  ( -g `  S )  =  (
-g `  S )
6 lcfrlem1.f . . . 4  |-  F  =  (LFnl `  U )
7 lcfrlem1.d . . . 4  |-  D  =  (LDual `  U )
8 lcfrlem1.m . . . 4  |-  .-  =  ( -g `  D )
9 lcfrlem1.u . . . . 5  |-  ( ph  ->  U  e.  LVec )
10 lveclmod 17623 . . . . 5  |-  ( U  e.  LVec  ->  U  e. 
LMod )
119, 10syl 16 . . . 4  |-  ( ph  ->  U  e.  LMod )
12 lcfrlem1.e . . . 4  |-  ( ph  ->  E  e.  F )
13 eqid 2467 . . . . 5  |-  ( Base `  S )  =  (
Base `  S )
14 lcfrlem1.t . . . . 5  |-  .x.  =  ( .s `  D )
154lvecdrng 17622 . . . . . . . 8  |-  ( U  e.  LVec  ->  S  e.  DivRing )
169, 15syl 16 . . . . . . 7  |-  ( ph  ->  S  e.  DivRing )
17 lcfrlem1.g . . . . . . . 8  |-  ( ph  ->  G  e.  F )
18 lcfrlem1.x . . . . . . . 8  |-  ( ph  ->  X  e.  V )
194, 13, 3, 6lflcl 34262 . . . . . . . 8  |-  ( ( U  e.  LVec  /\  G  e.  F  /\  X  e.  V )  ->  ( G `  X )  e.  ( Base `  S
) )
209, 17, 18, 19syl3anc 1228 . . . . . . 7  |-  ( ph  ->  ( G `  X
)  e.  ( Base `  S ) )
21 lcfrlem1.n . . . . . . 7  |-  ( ph  ->  ( G `  X
)  =/=  .0.  )
22 lcfrlem1.z . . . . . . . 8  |-  .0.  =  ( 0g `  S )
23 lcfrlem1.i . . . . . . . 8  |-  I  =  ( invr `  S
)
2413, 22, 23drnginvrcl 17284 . . . . . . 7  |-  ( ( S  e.  DivRing  /\  ( G `  X )  e.  ( Base `  S
)  /\  ( G `  X )  =/=  .0.  )  ->  ( I `  ( G `  X ) )  e.  ( Base `  S ) )
2516, 20, 21, 24syl3anc 1228 . . . . . 6  |-  ( ph  ->  ( I `  ( G `  X )
)  e.  ( Base `  S ) )
264, 13, 3, 6lflcl 34262 . . . . . . 7  |-  ( ( U  e.  LVec  /\  E  e.  F  /\  X  e.  V )  ->  ( E `  X )  e.  ( Base `  S
) )
279, 12, 18, 26syl3anc 1228 . . . . . 6  |-  ( ph  ->  ( E `  X
)  e.  ( Base `  S ) )
28 lcfrlem1.q . . . . . . 7  |-  .X.  =  ( .r `  S )
294, 13, 28lmodmcl 17395 . . . . . 6  |-  ( ( U  e.  LMod  /\  (
I `  ( G `  X ) )  e.  ( Base `  S
)  /\  ( E `  X )  e.  (
Base `  S )
)  ->  ( (
I `  ( G `  X ) )  .X.  ( E `  X ) )  e.  ( Base `  S ) )
3011, 25, 27, 29syl3anc 1228 . . . . 5  |-  ( ph  ->  ( ( I `  ( G `  X ) )  .X.  ( E `  X ) )  e.  ( Base `  S
) )
316, 4, 13, 7, 14, 11, 30, 17ldualvscl 34337 . . . 4  |-  ( ph  ->  ( ( ( I `
 ( G `  X ) )  .X.  ( E `  X ) )  .x.  G )  e.  F )
323, 4, 5, 6, 7, 8, 11, 12, 31, 18ldualvsubval 34355 . . 3  |-  ( ph  ->  ( ( E  .-  ( ( ( I `
 ( G `  X ) )  .X.  ( E `  X ) )  .x.  G ) ) `  X )  =  ( ( E `
 X ) (
-g `  S )
( ( ( ( I `  ( G `
 X ) ) 
.X.  ( E `  X ) )  .x.  G ) `  X
) ) )
336, 3, 4, 13, 28, 7, 14, 9, 30, 17, 18ldualvsval 34336 . . . . 5  |-  ( ph  ->  ( ( ( ( I `  ( G `
 X ) ) 
.X.  ( E `  X ) )  .x.  G ) `  X
)  =  ( ( G `  X ) 
.X.  ( ( I `
 ( G `  X ) )  .X.  ( E `  X ) ) ) )
34 eqid 2467 . . . . . . . . 9  |-  ( 1r
`  S )  =  ( 1r `  S
)
3513, 22, 28, 34, 23drnginvrr 17287 . . . . . . . 8  |-  ( ( S  e.  DivRing  /\  ( G `  X )  e.  ( Base `  S
)  /\  ( G `  X )  =/=  .0.  )  ->  ( ( G `
 X )  .X.  ( I `  ( G `  X )
) )  =  ( 1r `  S ) )
3616, 20, 21, 35syl3anc 1228 . . . . . . 7  |-  ( ph  ->  ( ( G `  X )  .X.  (
I `  ( G `  X ) ) )  =  ( 1r `  S ) )
3736oveq1d 6310 . . . . . 6  |-  ( ph  ->  ( ( ( G `
 X )  .X.  ( I `  ( G `  X )
) )  .X.  ( E `  X )
)  =  ( ( 1r `  S ) 
.X.  ( E `  X ) ) )
384lmodring 17391 . . . . . . . 8  |-  ( U  e.  LMod  ->  S  e. 
Ring )
3911, 38syl 16 . . . . . . 7  |-  ( ph  ->  S  e.  Ring )
4013, 28ringass 17087 . . . . . . 7  |-  ( ( S  e.  Ring  /\  (
( G `  X
)  e.  ( Base `  S )  /\  (
I `  ( G `  X ) )  e.  ( Base `  S
)  /\  ( E `  X )  e.  (
Base `  S )
) )  ->  (
( ( G `  X )  .X.  (
I `  ( G `  X ) ) ) 
.X.  ( E `  X ) )  =  ( ( G `  X )  .X.  (
( I `  ( G `  X )
)  .X.  ( E `  X ) ) ) )
4139, 20, 25, 27, 40syl13anc 1230 . . . . . 6  |-  ( ph  ->  ( ( ( G `
 X )  .X.  ( I `  ( G `  X )
) )  .X.  ( E `  X )
)  =  ( ( G `  X ) 
.X.  ( ( I `
 ( G `  X ) )  .X.  ( E `  X ) ) ) )
4213, 28, 34ringlidm 17094 . . . . . . 7  |-  ( ( S  e.  Ring  /\  ( E `  X )  e.  ( Base `  S
) )  ->  (
( 1r `  S
)  .X.  ( E `  X ) )  =  ( E `  X
) )
4339, 27, 42syl2anc 661 . . . . . 6  |-  ( ph  ->  ( ( 1r `  S )  .X.  ( E `  X )
)  =  ( E `
 X ) )
4437, 41, 433eqtr3d 2516 . . . . 5  |-  ( ph  ->  ( ( G `  X )  .X.  (
( I `  ( G `  X )
)  .X.  ( E `  X ) ) )  =  ( E `  X ) )
4533, 44eqtrd 2508 . . . 4  |-  ( ph  ->  ( ( ( ( I `  ( G `
 X ) ) 
.X.  ( E `  X ) )  .x.  G ) `  X
)  =  ( E `
 X ) )
4645oveq2d 6311 . . 3  |-  ( ph  ->  ( ( E `  X ) ( -g `  S ) ( ( ( ( I `  ( G `  X ) )  .X.  ( E `  X ) )  .x.  G ) `  X
) )  =  ( ( E `  X
) ( -g `  S
) ( E `  X ) ) )
474lmodfgrp 17392 . . . . 5  |-  ( U  e.  LMod  ->  S  e. 
Grp )
4811, 47syl 16 . . . 4  |-  ( ph  ->  S  e.  Grp )
4913, 22, 5grpsubid 15994 . . . 4  |-  ( ( S  e.  Grp  /\  ( E `  X )  e.  ( Base `  S
) )  ->  (
( E `  X
) ( -g `  S
) ( E `  X ) )  =  .0.  )
5048, 27, 49syl2anc 661 . . 3  |-  ( ph  ->  ( ( E `  X ) ( -g `  S ) ( E `
 X ) )  =  .0.  )
5132, 46, 503eqtrd 2512 . 2  |-  ( ph  ->  ( ( E  .-  ( ( ( I `
 ( G `  X ) )  .X.  ( E `  X ) )  .x.  G ) ) `  X )  =  .0.  )
522, 51syl5eq 2520 1  |-  ( ph  ->  ( H `  X
)  =  .0.  )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767    =/= wne 2662   ` cfv 5594  (class class class)co 6295   Basecbs 14507   .rcmulr 14573  Scalarcsca 14575   .scvsca 14576   0gc0g 14712   Grpcgrp 15925   -gcsg 15927   1rcur 17025   Ringcrg 17070   invrcinvr 17192   DivRingcdr 17267   LModclmod 17383   LVecclvec 17619  LFnlclfn 34255  LDualcld 34321
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-of 6535  df-om 6696  df-1st 6795  df-2nd 6796  df-tpos 6967  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-map 7434  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  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-4 10608  df-5 10609  df-6 10610  df-n0 10808  df-z 10877  df-uz 11095  df-fz 11685  df-struct 14509  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-ress 14514  df-plusg 14585  df-mulr 14586  df-sca 14588  df-vsca 14589  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-lvec 17620  df-lfl 34256  df-ldual 34322
This theorem is referenced by:  lcfrlem3  36742
  Copyright terms: Public domain W3C validator