Metamath Proof Explorer

Theorem lcfrlem2

Description: Lemma for lcfr . (Contributed by NM, 27-Feb-2015)

Ref Expression
Hypotheses 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 ) )
lcfrlem2.l 
|- L = ( LKer ` U )
Assertion lcfrlem2 
|- ( ph -> ( ( L ` E ) i^i ( L ` G ) ) C_ ( L ` H ) )

Proof

Step Hyp Ref Expression
1 lcfrlem1.v 
 |-  V = ( Base ` U )
2 lcfrlem1.s 
 |-  S = ( Scalar ` U )
3 lcfrlem1.q 
 |-  .X. = ( .r ` S )
4 lcfrlem1.z 
 |-  .0. = ( 0g ` S )
5 lcfrlem1.i 
 |-  I = ( invr ` S )
6 lcfrlem1.f 
 |-  F = ( LFnl ` U )
7 lcfrlem1.d 
 |-  D = ( LDual ` U )
8 lcfrlem1.t 
 |-  .x. = ( .s ` D )
9 lcfrlem1.m 
 |-  .- = ( -g ` D )
10 lcfrlem1.u 
 |-  ( ph -> U e. LVec )
11 lcfrlem1.e 
 |-  ( ph -> E e. F )
12 lcfrlem1.g 
 |-  ( ph -> G e. F )
13 lcfrlem1.x 
 |-  ( ph -> X e. V )
14 lcfrlem1.n 
 |-  ( ph -> ( G ` X ) =/= .0. )
15 lcfrlem1.h 
 |-  H = ( E .- ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) )
16 lcfrlem2.l 
 |-  L = ( LKer ` U )
17 eqid 
 |-  ( Base ` S ) = ( Base ` S )
18 lveclmod 
 |-  ( U e. LVec -> U e. LMod )
19 10 18 syl 
 |-  ( ph -> U e. LMod )
20 2 lmodring 
 |-  ( U e. LMod -> S e. Ring )
21 19 20 syl 
 |-  ( ph -> S e. Ring )
22 2 lvecdrng 
 |-  ( U e. LVec -> S e. DivRing )
23 10 22 syl 
 |-  ( ph -> S e. DivRing )
24 2 17 1 6 lflcl 
 |-  ( ( U e. LVec /\ G e. F /\ X e. V ) -> ( G ` X ) e. ( Base ` S ) )
25 10 12 13 24 syl3anc 
 |-  ( ph -> ( G ` X ) e. ( Base ` S ) )
26 17 4 5 drnginvrcl 
 |-  ( ( S e. DivRing /\ ( G ` X ) e. ( Base ` S ) /\ ( G ` X ) =/= .0. ) -> ( I ` ( G ` X ) ) e. ( Base ` S ) )
27 23 25 14 26 syl3anc 
 |-  ( ph -> ( I ` ( G ` X ) ) e. ( Base ` S ) )
28 2 17 1 6 lflcl 
 |-  ( ( U e. LVec /\ E e. F /\ X e. V ) -> ( E ` X ) e. ( Base ` S ) )
29 10 11 13 28 syl3anc 
 |-  ( ph -> ( E ` X ) e. ( Base ` S ) )
30 17 3 ringcl 
 |-  ( ( S e. Ring /\ ( I ` ( G ` X ) ) e. ( Base ` S ) /\ ( E ` X ) e. ( Base ` S ) ) -> ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) e. ( Base ` S ) )
31 21 27 29 30 syl3anc 
 |-  ( ph -> ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) e. ( Base ` S ) )
32 2 17 6 16 7 8 10 12 31 lkrss 
 |-  ( ph -> ( L ` G ) C_ ( L ` ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) )
33 6 2 17 7 8 19 31 12 ldualvscl 
 |-  ( ph -> ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) e. F )
34 ringgrp 
 |-  ( S e. Ring -> S e. Grp )
35 21 34 syl 
 |-  ( ph -> S e. Grp )
36 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
37 17 36 ringidcl 
 |-  ( S e. Ring -> ( 1r ` S ) e. ( Base ` S ) )
38 21 37 syl 
 |-  ( ph -> ( 1r ` S ) e. ( Base ` S ) )
39 eqid 
 |-  ( invg ` S ) = ( invg ` S )
40 17 39 grpinvcl 
 |-  ( ( S e. Grp /\ ( 1r ` S ) e. ( Base ` S ) ) -> ( ( invg ` S ) ` ( 1r ` S ) ) e. ( Base ` S ) )
41 35 38 40 syl2anc 
 |-  ( ph -> ( ( invg ` S ) ` ( 1r ` S ) ) e. ( Base ` S ) )
42 2 17 6 16 7 8 10 33 41 lkrss 
 |-  ( ph -> ( L ` ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) C_ ( L ` ( ( ( invg ` S ) ` ( 1r ` S ) ) .x. ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ) )
43 32 42 sstrd 
 |-  ( ph -> ( L ` G ) C_ ( L ` ( ( ( invg ` S ) ` ( 1r ` S ) ) .x. ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ) )
44 sslin 
 |-  ( ( L ` G ) C_ ( L ` ( ( ( invg ` S ) ` ( 1r ` S ) ) .x. ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ) -> ( ( L ` E ) i^i ( L ` G ) ) C_ ( ( L ` E ) i^i ( L ` ( ( ( invg ` S ) ` ( 1r ` S ) ) .x. ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ) ) )
45 43 44 syl 
 |-  ( ph -> ( ( L ` E ) i^i ( L ` G ) ) C_ ( ( L ` E ) i^i ( L ` ( ( ( invg ` S ) ` ( 1r ` S ) ) .x. ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ) ) )
46 eqid 
 |-  ( +g ` D ) = ( +g ` D )
47 6 2 17 7 8 19 41 33 ldualvscl 
 |-  ( ph -> ( ( ( invg ` S ) ` ( 1r ` S ) ) .x. ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) e. F )
48 6 16 7 46 19 11 47 lkrin 
 |-  ( ph -> ( ( L ` E ) i^i ( L ` ( ( ( invg ` S ) ` ( 1r ` S ) ) .x. ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ) ) C_ ( L ` ( E ( +g ` D ) ( ( ( invg ` S ) ` ( 1r ` S ) ) .x. ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ) ) )
49 45 48 sstrd 
 |-  ( ph -> ( ( L ` E ) i^i ( L ` G ) ) C_ ( L ` ( E ( +g ` D ) ( ( ( invg ` S ) ` ( 1r ` S ) ) .x. ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ) ) )
50 15 fveq2i 
 |-  ( L ` H ) = ( L ` ( E .- ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) )
51 2 39 36 6 7 46 8 9 19 11 33 ldualvsub 
 |-  ( ph -> ( E .- ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) = ( E ( +g ` D ) ( ( ( invg ` S ) ` ( 1r ` S ) ) .x. ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ) )
52 51 fveq2d 
 |-  ( ph -> ( L ` ( E .- ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ) = ( L ` ( E ( +g ` D ) ( ( ( invg ` S ) ` ( 1r ` S ) ) .x. ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ) ) )
53 50 52 syl5req 
 |-  ( ph -> ( L ` ( E ( +g ` D ) ( ( ( invg ` S ) ` ( 1r ` S ) ) .x. ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ) ) = ( L ` H ) )
54 49 53 sseqtrd 
 |-  ( ph -> ( ( L ` E ) i^i ( L ` G ) ) C_ ( L ` H ) )