Metamath Proof Explorer

Theorem lcfrlem3

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 lcfrlem3 
|- ( ph -> X e. ( 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 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 lcfrlem1 
 |-  ( ph -> ( H ` X ) = .0. )
18 lveclmod 
 |-  ( U e. LVec -> U e. LMod )
19 10 18 syl 
 |-  ( ph -> U e. LMod )
20 eqid 
 |-  ( Base ` S ) = ( Base ` S )
21 2 lmodring 
 |-  ( U e. LMod -> S e. Ring )
22 19 21 syl 
 |-  ( ph -> S e. Ring )
23 2 lvecdrng 
 |-  ( U e. LVec -> S e. DivRing )
24 10 23 syl 
 |-  ( ph -> S e. DivRing )
25 2 20 1 6 lflcl 
 |-  ( ( U e. LVec /\ G e. F /\ X e. V ) -> ( G ` X ) e. ( Base ` S ) )
26 10 12 13 25 syl3anc 
 |-  ( ph -> ( G ` X ) e. ( Base ` S ) )
27 20 4 5 drnginvrcl 
 |-  ( ( S e. DivRing /\ ( G ` X ) e. ( Base ` S ) /\ ( G ` X ) =/= .0. ) -> ( I ` ( G ` X ) ) e. ( Base ` S ) )
28 24 26 14 27 syl3anc 
 |-  ( ph -> ( I ` ( G ` X ) ) e. ( Base ` S ) )
29 2 20 1 6 lflcl 
 |-  ( ( U e. LVec /\ E e. F /\ X e. V ) -> ( E ` X ) e. ( Base ` S ) )
30 10 11 13 29 syl3anc 
 |-  ( ph -> ( E ` X ) e. ( Base ` S ) )
31 20 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 ) )
32 22 28 30 31 syl3anc 
 |-  ( ph -> ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) e. ( Base ` S ) )
33 6 2 20 7 8 19 32 12 ldualvscl 
 |-  ( ph -> ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) e. F )
34 6 7 9 19 11 33 ldualvsubcl 
 |-  ( ph -> ( E .- ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) e. F )
35 15 34 eqeltrid 
 |-  ( ph -> H e. F )
36 1 2 4 6 16 10 35 13 ellkr2 
 |-  ( ph -> ( X e. ( L ` H ) <-> ( H ` X ) = .0. ) )
37 17 36 mpbird 
 |-  ( ph -> X e. ( L ` H ) )