Metamath Proof Explorer

Theorem lcfrlem1

Description: Lemma for lcfr . Note that X is z in Mario's notes. (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 ) )
Assertion lcfrlem1 
|- ( ph -> ( H ` X ) = .0. )

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 15 fveq1i 
 |-  ( H ` X ) = ( ( E .- ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ` X )
17 eqid 
 |-  ( -g ` S ) = ( -g ` S )
18 lveclmod 
 |-  ( U e. LVec -> U e. LMod )
19 10 18 syl 
 |-  ( ph -> U e. LMod )
20 eqid 
 |-  ( Base ` S ) = ( Base ` S )
21 2 lvecdrng 
 |-  ( U e. LVec -> S e. DivRing )
22 10 21 syl 
 |-  ( ph -> S e. DivRing )
23 2 20 1 6 lflcl 
 |-  ( ( U e. LVec /\ G e. F /\ X e. V ) -> ( G ` X ) e. ( Base ` S ) )
24 10 12 13 23 syl3anc 
 |-  ( ph -> ( G ` X ) e. ( Base ` S ) )
25 20 4 5 drnginvrcl 
 |-  ( ( S e. DivRing /\ ( G ` X ) e. ( Base ` S ) /\ ( G ` X ) =/= .0. ) -> ( I ` ( G ` X ) ) e. ( Base ` S ) )
26 22 24 14 25 syl3anc 
 |-  ( ph -> ( I ` ( G ` X ) ) e. ( Base ` S ) )
27 2 20 1 6 lflcl 
 |-  ( ( U e. LVec /\ E e. F /\ X e. V ) -> ( E ` X ) e. ( Base ` S ) )
28 10 11 13 27 syl3anc 
 |-  ( ph -> ( E ` X ) e. ( Base ` S ) )
29 2 20 3 lmodmcl 
 |-  ( ( U e. LMod /\ ( I ` ( G ` X ) ) e. ( Base ` S ) /\ ( E ` X ) e. ( Base ` S ) ) -> ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) e. ( Base ` S ) )
30 19 26 28 29 syl3anc 
 |-  ( ph -> ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) e. ( Base ` S ) )
31 6 2 20 7 8 19 30 12 ldualvscl 
 |-  ( ph -> ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) e. F )
32 1 2 17 6 7 9 19 11 31 13 ldualvsubval 
 |-  ( ph -> ( ( E .- ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ` X ) = ( ( E ` X ) ( -g ` S ) ( ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ` X ) ) )
33 6 1 2 20 3 7 8 10 30 12 13 ldualvsval 
 |-  ( ph -> ( ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ` X ) = ( ( G ` X ) .X. ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) ) )
34 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
35 20 4 3 34 5 drnginvrr 
 |-  ( ( S e. DivRing /\ ( G ` X ) e. ( Base ` S ) /\ ( G ` X ) =/= .0. ) -> ( ( G ` X ) .X. ( I ` ( G ` X ) ) ) = ( 1r ` S ) )
36 22 24 14 35 syl3anc 
 |-  ( ph -> ( ( G ` X ) .X. ( I ` ( G ` X ) ) ) = ( 1r ` S ) )
37 36 oveq1d 
 |-  ( ph -> ( ( ( G ` X ) .X. ( I ` ( G ` X ) ) ) .X. ( E ` X ) ) = ( ( 1r ` S ) .X. ( E ` X ) ) )
38 2 lmodring 
 |-  ( U e. LMod -> S e. Ring )
39 19 38 syl 
 |-  ( ph -> S e. Ring )
40 20 3 ringass 
 |-  ( ( 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 ) ) ) )
41 39 24 26 28 40 syl13anc 
 |-  ( ph -> ( ( ( G ` X ) .X. ( I ` ( G ` X ) ) ) .X. ( E ` X ) ) = ( ( G ` X ) .X. ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) ) )
42 20 3 34 ringlidm 
 |-  ( ( S e. Ring /\ ( E ` X ) e. ( Base ` S ) ) -> ( ( 1r ` S ) .X. ( E ` X ) ) = ( E ` X ) )
43 39 28 42 syl2anc 
 |-  ( ph -> ( ( 1r ` S ) .X. ( E ` X ) ) = ( E ` X ) )
44 37 41 43 3eqtr3d 
 |-  ( ph -> ( ( G ` X ) .X. ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) ) = ( E ` X ) )
45 33 44 eqtrd 
 |-  ( ph -> ( ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ` X ) = ( E ` X ) )
46 45 oveq2d 
 |-  ( ph -> ( ( E ` X ) ( -g ` S ) ( ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ` X ) ) = ( ( E ` X ) ( -g ` S ) ( E ` X ) ) )
47 2 lmodfgrp 
 |-  ( U e. LMod -> S e. Grp )
48 19 47 syl 
 |-  ( ph -> S e. Grp )
49 20 4 17 grpsubid 
 |-  ( ( S e. Grp /\ ( E ` X ) e. ( Base ` S ) ) -> ( ( E ` X ) ( -g ` S ) ( E ` X ) ) = .0. )
50 48 28 49 syl2anc 
 |-  ( ph -> ( ( E ` X ) ( -g ` S ) ( E ` X ) ) = .0. )
51 32 46 50 3eqtrd 
 |-  ( ph -> ( ( E .- ( ( ( I ` ( G ` X ) ) .X. ( E ` X ) ) .x. G ) ) ` X ) = .0. )
52 16 51 syl5eq 
 |-  ( ph -> ( H ` X ) = .0. )