Metamath Proof Explorer

Theorem lclkrlem2m

Description: Lemma for lclkr . Construct a vector B that makes the sum of functionals zero. Combine with B e. V to shorten overall proof. (Contributed by NM, 17-Jan-2015)

Ref Expression
Hypotheses lclkrlem2m.v 
|- V = ( Base ` U )
lclkrlem2m.t 
|- .x. = ( .s ` U )
lclkrlem2m.s 
|- S = ( Scalar ` U )
lclkrlem2m.q 
|- .X. = ( .r ` S )
lclkrlem2m.z 
|- .0. = ( 0g ` S )
lclkrlem2m.i 
|- I = ( invr ` S )
lclkrlem2m.m 
|- .- = ( -g ` U )
lclkrlem2m.f 
|- F = ( LFnl ` U )
lclkrlem2m.d 
|- D = ( LDual ` U )
lclkrlem2m.p 
|- .+ = ( +g ` D )
lclkrlem2m.x 
|- ( ph -> X e. V )
lclkrlem2m.y 
|- ( ph -> Y e. V )
lclkrlem2m.e 
|- ( ph -> E e. F )
lclkrlem2m.g 
|- ( ph -> G e. F )
lclkrlem2m.w 
|- ( ph -> U e. LVec )
lclkrlem2m.b 
|- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )
lclkrlem2m.n 
|- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )
Assertion lclkrlem2m 
|- ( ph -> ( B e. V /\ ( ( E .+ G ) ` B ) = .0. ) )

Proof

Step Hyp Ref Expression
1 lclkrlem2m.v 
 |-  V = ( Base ` U )
2 lclkrlem2m.t 
 |-  .x. = ( .s ` U )
3 lclkrlem2m.s 
 |-  S = ( Scalar ` U )
4 lclkrlem2m.q 
 |-  .X. = ( .r ` S )
5 lclkrlem2m.z 
 |-  .0. = ( 0g ` S )
6 lclkrlem2m.i 
 |-  I = ( invr ` S )
7 lclkrlem2m.m 
 |-  .- = ( -g ` U )
8 lclkrlem2m.f 
 |-  F = ( LFnl ` U )
9 lclkrlem2m.d 
 |-  D = ( LDual ` U )
10 lclkrlem2m.p 
 |-  .+ = ( +g ` D )
11 lclkrlem2m.x 
 |-  ( ph -> X e. V )
12 lclkrlem2m.y 
 |-  ( ph -> Y e. V )
13 lclkrlem2m.e 
 |-  ( ph -> E e. F )
14 lclkrlem2m.g 
 |-  ( ph -> G e. F )
15 lclkrlem2m.w 
 |-  ( ph -> U e. LVec )
16 lclkrlem2m.b 
 |-  B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )
17 lclkrlem2m.n 
 |-  ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )
18 lveclmod 
 |-  ( U e. LVec -> U e. LMod )
19 15 18 syl 
 |-  ( ph -> U e. LMod )
20 lmodgrp 
 |-  ( U e. LMod -> U e. Grp )
21 19 20 syl 
 |-  ( ph -> U e. Grp )
22 3 lmodring 
 |-  ( U e. LMod -> S e. Ring )
23 19 22 syl 
 |-  ( ph -> S e. Ring )
24 8 9 10 19 13 14 ldualvaddcl 
 |-  ( ph -> ( E .+ G ) e. F )
25 eqid 
 |-  ( Base ` S ) = ( Base ` S )
26 3 25 1 8 lflcl 
 |-  ( ( U e. LVec /\ ( E .+ G ) e. F /\ X e. V ) -> ( ( E .+ G ) ` X ) e. ( Base ` S ) )
27 15 24 11 26 syl3anc 
 |-  ( ph -> ( ( E .+ G ) ` X ) e. ( Base ` S ) )
28 3 lvecdrng 
 |-  ( U e. LVec -> S e. DivRing )
29 15 28 syl 
 |-  ( ph -> S e. DivRing )
30 3 25 1 8 lflcl 
 |-  ( ( U e. LVec /\ ( E .+ G ) e. F /\ Y e. V ) -> ( ( E .+ G ) ` Y ) e. ( Base ` S ) )
31 15 24 12 30 syl3anc 
 |-  ( ph -> ( ( E .+ G ) ` Y ) e. ( Base ` S ) )
32 25 5 6 drnginvrcl 
 |-  ( ( S e. DivRing /\ ( ( E .+ G ) ` Y ) e. ( Base ` S ) /\ ( ( E .+ G ) ` Y ) =/= .0. ) -> ( I ` ( ( E .+ G ) ` Y ) ) e. ( Base ` S ) )
33 29 31 17 32 syl3anc 
 |-  ( ph -> ( I ` ( ( E .+ G ) ` Y ) ) e. ( Base ` S ) )
34 25 4 ringcl 
 |-  ( ( S e. Ring /\ ( ( E .+ G ) ` X ) e. ( Base ` S ) /\ ( I ` ( ( E .+ G ) ` Y ) ) e. ( Base ` S ) ) -> ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) e. ( Base ` S ) )
35 23 27 33 34 syl3anc 
 |-  ( ph -> ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) e. ( Base ` S ) )
36 1 3 2 25 lmodvscl 
 |-  ( ( U e. LMod /\ ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) e. ( Base ` S ) /\ Y e. V ) -> ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) e. V )
37 19 35 12 36 syl3anc 
 |-  ( ph -> ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) e. V )
38 1 7 grpsubcl 
 |-  ( ( U e. Grp /\ X e. V /\ ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) e. V ) -> ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) e. V )
39 21 11 37 38 syl3anc 
 |-  ( ph -> ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) e. V )
40 16 39 eqeltrid 
 |-  ( ph -> B e. V )
41 16 fveq2i 
 |-  ( ( E .+ G ) ` B ) = ( ( E .+ G ) ` ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) )
42 eqid 
 |-  ( -g ` S ) = ( -g ` S )
43 3 42 1 7 8 lflsub 
 |-  ( ( U e. LMod /\ ( E .+ G ) e. F /\ ( X e. V /\ ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) e. V ) ) -> ( ( E .+ G ) ` ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) ) = ( ( ( E .+ G ) ` X ) ( -g ` S ) ( ( E .+ G ) ` ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) ) )
44 19 24 11 37 43 syl112anc 
 |-  ( ph -> ( ( E .+ G ) ` ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) ) = ( ( ( E .+ G ) ` X ) ( -g ` S ) ( ( E .+ G ) ` ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) ) )
45 3 25 4 1 2 8 lflmul 
 |-  ( ( U e. LMod /\ ( E .+ G ) e. F /\ ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) e. ( Base ` S ) /\ Y e. V ) ) -> ( ( E .+ G ) ` ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) = ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .X. ( ( E .+ G ) ` Y ) ) )
46 19 24 35 12 45 syl112anc 
 |-  ( ph -> ( ( E .+ G ) ` ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) = ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .X. ( ( E .+ G ) ` Y ) ) )
47 25 4 ringass 
 |-  ( ( S e. Ring /\ ( ( ( E .+ G ) ` X ) e. ( Base ` S ) /\ ( I ` ( ( E .+ G ) ` Y ) ) e. ( Base ` S ) /\ ( ( E .+ G ) ` Y ) e. ( Base ` S ) ) ) -> ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .X. ( ( E .+ G ) ` Y ) ) = ( ( ( E .+ G ) ` X ) .X. ( ( I ` ( ( E .+ G ) ` Y ) ) .X. ( ( E .+ G ) ` Y ) ) ) )
48 23 27 33 31 47 syl13anc 
 |-  ( ph -> ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .X. ( ( E .+ G ) ` Y ) ) = ( ( ( E .+ G ) ` X ) .X. ( ( I ` ( ( E .+ G ) ` Y ) ) .X. ( ( E .+ G ) ` Y ) ) ) )
49 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
50 25 5 4 49 6 drnginvrl 
 |-  ( ( S e. DivRing /\ ( ( E .+ G ) ` Y ) e. ( Base ` S ) /\ ( ( E .+ G ) ` Y ) =/= .0. ) -> ( ( I ` ( ( E .+ G ) ` Y ) ) .X. ( ( E .+ G ) ` Y ) ) = ( 1r ` S ) )
51 29 31 17 50 syl3anc 
 |-  ( ph -> ( ( I ` ( ( E .+ G ) ` Y ) ) .X. ( ( E .+ G ) ` Y ) ) = ( 1r ` S ) )
52 51 oveq2d 
 |-  ( ph -> ( ( ( E .+ G ) ` X ) .X. ( ( I ` ( ( E .+ G ) ` Y ) ) .X. ( ( E .+ G ) ` Y ) ) ) = ( ( ( E .+ G ) ` X ) .X. ( 1r ` S ) ) )
53 48 52 eqtrd 
 |-  ( ph -> ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .X. ( ( E .+ G ) ` Y ) ) = ( ( ( E .+ G ) ` X ) .X. ( 1r ` S ) ) )
54 25 4 49 ringridm 
 |-  ( ( S e. Ring /\ ( ( E .+ G ) ` X ) e. ( Base ` S ) ) -> ( ( ( E .+ G ) ` X ) .X. ( 1r ` S ) ) = ( ( E .+ G ) ` X ) )
55 23 27 54 syl2anc 
 |-  ( ph -> ( ( ( E .+ G ) ` X ) .X. ( 1r ` S ) ) = ( ( E .+ G ) ` X ) )
56 46 53 55 3eqtrd 
 |-  ( ph -> ( ( E .+ G ) ` ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) = ( ( E .+ G ) ` X ) )
57 56 oveq2d 
 |-  ( ph -> ( ( ( E .+ G ) ` X ) ( -g ` S ) ( ( E .+ G ) ` ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) ) = ( ( ( E .+ G ) ` X ) ( -g ` S ) ( ( E .+ G ) ` X ) ) )
58 ringgrp 
 |-  ( S e. Ring -> S e. Grp )
59 23 58 syl 
 |-  ( ph -> S e. Grp )
60 25 5 42 grpsubid 
 |-  ( ( S e. Grp /\ ( ( E .+ G ) ` X ) e. ( Base ` S ) ) -> ( ( ( E .+ G ) ` X ) ( -g ` S ) ( ( E .+ G ) ` X ) ) = .0. )
61 59 27 60 syl2anc 
 |-  ( ph -> ( ( ( E .+ G ) ` X ) ( -g ` S ) ( ( E .+ G ) ` X ) ) = .0. )
62 44 57 61 3eqtrd 
 |-  ( ph -> ( ( E .+ G ) ` ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) ) = .0. )
63 41 62 eqtrid 
 |-  ( ph -> ( ( E .+ G ) ` B ) = .0. )
64 40 63 jca 
 |-  ( ph -> ( B e. V /\ ( ( E .+ G ) ` B ) = .0. ) )