Metamath Proof Explorer

Theorem hdmapinvlem3

Description: Line 30 in Baer p. 110, f(sw + u, tw - v) = 0. (Contributed by NM, 12-Jun-2015)

Ref Expression
Hypotheses hdmapinvlem3.h 
|- H = ( LHyp ` K )
hdmapinvlem3.e 
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
hdmapinvlem3.o 
|- O = ( ( ocH ` K ) ` W )
hdmapinvlem3.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapinvlem3.v 
|- V = ( Base ` U )
hdmapinvlem3.p 
|- .+ = ( +g ` U )
hdmapinvlem3.m 
|- .- = ( -g ` U )
hdmapinvlem3.q 
|- .x. = ( .s ` U )
hdmapinvlem3.r 
|- R = ( Scalar ` U )
hdmapinvlem3.b 
|- B = ( Base ` R )
hdmapinvlem3.t 
|- .X. = ( .r ` R )
hdmapinvlem3.z 
|- .0. = ( 0g ` R )
hdmapinvlem3.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapinvlem3.g 
|- G = ( ( HGMap ` K ) ` W )
hdmapinvlem3.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapinvlem3.c 
|- ( ph -> C e. ( O ` { E } ) )
hdmapinvlem3.d 
|- ( ph -> D e. ( O ` { E } ) )
hdmapinvlem3.i 
|- ( ph -> I e. B )
hdmapinvlem3.j 
|- ( ph -> J e. B )
hdmapinvlem3.ij 
|- ( ph -> ( I .X. ( G ` J ) ) = ( ( S ` D ) ` C ) )
Assertion hdmapinvlem3 
|- ( ph -> ( ( S ` ( ( J .x. E ) .- D ) ) ` ( ( I .x. E ) .+ C ) ) = .0. )

Proof

Step Hyp Ref Expression
1 hdmapinvlem3.h 
 |-  H = ( LHyp ` K )
2 hdmapinvlem3.e 
 |-  E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
3 hdmapinvlem3.o 
 |-  O = ( ( ocH ` K ) ` W )
4 hdmapinvlem3.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 hdmapinvlem3.v 
 |-  V = ( Base ` U )
6 hdmapinvlem3.p 
 |-  .+ = ( +g ` U )
7 hdmapinvlem3.m 
 |-  .- = ( -g ` U )
8 hdmapinvlem3.q 
 |-  .x. = ( .s ` U )
9 hdmapinvlem3.r 
 |-  R = ( Scalar ` U )
10 hdmapinvlem3.b 
 |-  B = ( Base ` R )
11 hdmapinvlem3.t 
 |-  .X. = ( .r ` R )
12 hdmapinvlem3.z 
 |-  .0. = ( 0g ` R )
13 hdmapinvlem3.s 
 |-  S = ( ( HDMap ` K ) ` W )
14 hdmapinvlem3.g 
 |-  G = ( ( HGMap ` K ) ` W )
15 hdmapinvlem3.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
16 hdmapinvlem3.c 
 |-  ( ph -> C e. ( O ` { E } ) )
17 hdmapinvlem3.d 
 |-  ( ph -> D e. ( O ` { E } ) )
18 hdmapinvlem3.i 
 |-  ( ph -> I e. B )
19 hdmapinvlem3.j 
 |-  ( ph -> J e. B )
20 hdmapinvlem3.ij 
 |-  ( ph -> ( I .X. ( G ` J ) ) = ( ( S ` D ) ` C ) )
21 eqid 
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
22 eqid 
 |-  ( -g ` ( ( LCDual ` K ) ` W ) ) = ( -g ` ( ( LCDual ` K ) ` W ) )
23 1 4 15 dvhlmod 
 |-  ( ph -> U e. LMod )
24 eqid 
 |-  ( Base ` K ) = ( Base ` K )
25 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
26 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
27 1 24 25 4 5 26 2 15 dvheveccl 
 |-  ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
28 27 eldifad 
 |-  ( ph -> E e. V )
29 5 9 8 10 lmodvscl 
 |-  ( ( U e. LMod /\ J e. B /\ E e. V ) -> ( J .x. E ) e. V )
30 23 19 28 29 syl3anc 
 |-  ( ph -> ( J .x. E ) e. V )
31 28 snssd 
 |-  ( ph -> { E } C_ V )
32 1 4 5 3 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { E } C_ V ) -> ( O ` { E } ) C_ V )
33 15 31 32 syl2anc 
 |-  ( ph -> ( O ` { E } ) C_ V )
34 33 17 sseldd 
 |-  ( ph -> D e. V )
35 1 4 5 7 21 22 13 15 30 34 hdmapsub 
 |-  ( ph -> ( S ` ( ( J .x. E ) .- D ) ) = ( ( S ` ( J .x. E ) ) ( -g ` ( ( LCDual ` K ) ` W ) ) ( S ` D ) ) )
36 35 fveq1d 
 |-  ( ph -> ( ( S ` ( ( J .x. E ) .- D ) ) ` ( ( I .x. E ) .+ C ) ) = ( ( ( S ` ( J .x. E ) ) ( -g ` ( ( LCDual ` K ) ` W ) ) ( S ` D ) ) ` ( ( I .x. E ) .+ C ) ) )
37 eqid 
 |-  ( -g ` R ) = ( -g ` R )
38 eqid 
 |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
39 1 4 5 21 38 13 15 30 hdmapcl 
 |-  ( ph -> ( S ` ( J .x. E ) ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
40 1 4 5 21 38 13 15 34 hdmapcl 
 |-  ( ph -> ( S ` D ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
41 5 9 8 10 lmodvscl 
 |-  ( ( U e. LMod /\ I e. B /\ E e. V ) -> ( I .x. E ) e. V )
42 23 18 28 41 syl3anc 
 |-  ( ph -> ( I .x. E ) e. V )
43 33 16 sseldd 
 |-  ( ph -> C e. V )
44 5 6 lmodvacl 
 |-  ( ( U e. LMod /\ ( I .x. E ) e. V /\ C e. V ) -> ( ( I .x. E ) .+ C ) e. V )
45 23 42 43 44 syl3anc 
 |-  ( ph -> ( ( I .x. E ) .+ C ) e. V )
46 1 4 5 9 37 21 38 22 15 39 40 45 lcdvsubval 
 |-  ( ph -> ( ( ( S ` ( J .x. E ) ) ( -g ` ( ( LCDual ` K ) ` W ) ) ( S ` D ) ) ` ( ( I .x. E ) .+ C ) ) = ( ( ( S ` ( J .x. E ) ) ` ( ( I .x. E ) .+ C ) ) ( -g ` R ) ( ( S ` D ) ` ( ( I .x. E ) .+ C ) ) ) )
47 eqid 
 |-  ( +g ` R ) = ( +g ` R )
48 1 4 5 6 9 47 13 15 42 43 30 hdmaplna1 
 |-  ( ph -> ( ( S ` ( J .x. E ) ) ` ( ( I .x. E ) .+ C ) ) = ( ( ( S ` ( J .x. E ) ) ` ( I .x. E ) ) ( +g ` R ) ( ( S ` ( J .x. E ) ) ` C ) ) )
49 1 4 5 8 9 10 11 13 14 15 42 28 19 hdmapglnm2 
 |-  ( ph -> ( ( S ` ( J .x. E ) ) ` ( I .x. E ) ) = ( ( ( S ` E ) ` ( I .x. E ) ) .X. ( G ` J ) ) )
50 1 4 5 8 9 10 11 13 15 28 28 18 hdmaplnm1 
 |-  ( ph -> ( ( S ` E ) ` ( I .x. E ) ) = ( I .X. ( ( S ` E ) ` E ) ) )
51 eqid 
 |-  ( ( HVMap ` K ) ` W ) = ( ( HVMap ` K ) ` W )
52 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
53 1 2 51 13 15 4 9 52 hdmapevec2 
 |-  ( ph -> ( ( S ` E ) ` E ) = ( 1r ` R ) )
54 53 oveq2d 
 |-  ( ph -> ( I .X. ( ( S ` E ) ` E ) ) = ( I .X. ( 1r ` R ) ) )
55 9 lmodring 
 |-  ( U e. LMod -> R e. Ring )
56 23 55 syl 
 |-  ( ph -> R e. Ring )
57 10 11 52 ringridm 
 |-  ( ( R e. Ring /\ I e. B ) -> ( I .X. ( 1r ` R ) ) = I )
58 56 18 57 syl2anc 
 |-  ( ph -> ( I .X. ( 1r ` R ) ) = I )
59 50 54 58 3eqtrd 
 |-  ( ph -> ( ( S ` E ) ` ( I .x. E ) ) = I )
60 59 oveq1d 
 |-  ( ph -> ( ( ( S ` E ) ` ( I .x. E ) ) .X. ( G ` J ) ) = ( I .X. ( G ` J ) ) )
61 49 60 eqtrd 
 |-  ( ph -> ( ( S ` ( J .x. E ) ) ` ( I .x. E ) ) = ( I .X. ( G ` J ) ) )
62 1 4 5 8 9 10 11 13 14 15 43 28 19 hdmapglnm2 
 |-  ( ph -> ( ( S ` ( J .x. E ) ) ` C ) = ( ( ( S ` E ) ` C ) .X. ( G ` J ) ) )
63 1 2 3 4 5 9 10 11 12 13 15 16 hdmapinvlem1 
 |-  ( ph -> ( ( S ` E ) ` C ) = .0. )
64 63 oveq1d 
 |-  ( ph -> ( ( ( S ` E ) ` C ) .X. ( G ` J ) ) = ( .0. .X. ( G ` J ) ) )
65 1 4 9 10 14 15 19 hgmapcl 
 |-  ( ph -> ( G ` J ) e. B )
66 10 11 12 ringlz 
 |-  ( ( R e. Ring /\ ( G ` J ) e. B ) -> ( .0. .X. ( G ` J ) ) = .0. )
67 56 65 66 syl2anc 
 |-  ( ph -> ( .0. .X. ( G ` J ) ) = .0. )
68 62 64 67 3eqtrd 
 |-  ( ph -> ( ( S ` ( J .x. E ) ) ` C ) = .0. )
69 61 68 oveq12d 
 |-  ( ph -> ( ( ( S ` ( J .x. E ) ) ` ( I .x. E ) ) ( +g ` R ) ( ( S ` ( J .x. E ) ) ` C ) ) = ( ( I .X. ( G ` J ) ) ( +g ` R ) .0. ) )
70 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
71 56 70 syl 
 |-  ( ph -> R e. Grp )
72 9 10 11 lmodmcl 
 |-  ( ( U e. LMod /\ I e. B /\ ( G ` J ) e. B ) -> ( I .X. ( G ` J ) ) e. B )
73 23 18 65 72 syl3anc 
 |-  ( ph -> ( I .X. ( G ` J ) ) e. B )
74 10 47 12 grprid 
 |-  ( ( R e. Grp /\ ( I .X. ( G ` J ) ) e. B ) -> ( ( I .X. ( G ` J ) ) ( +g ` R ) .0. ) = ( I .X. ( G ` J ) ) )
75 71 73 74 syl2anc 
 |-  ( ph -> ( ( I .X. ( G ` J ) ) ( +g ` R ) .0. ) = ( I .X. ( G ` J ) ) )
76 48 69 75 3eqtrd 
 |-  ( ph -> ( ( S ` ( J .x. E ) ) ` ( ( I .x. E ) .+ C ) ) = ( I .X. ( G ` J ) ) )
77 1 4 5 6 9 47 13 15 42 43 34 hdmaplna1 
 |-  ( ph -> ( ( S ` D ) ` ( ( I .x. E ) .+ C ) ) = ( ( ( S ` D ) ` ( I .x. E ) ) ( +g ` R ) ( ( S ` D ) ` C ) ) )
78 1 4 5 8 9 10 11 13 15 28 34 18 hdmaplnm1 
 |-  ( ph -> ( ( S ` D ) ` ( I .x. E ) ) = ( I .X. ( ( S ` D ) ` E ) ) )
79 1 2 3 4 5 9 10 11 12 13 15 17 hdmapinvlem2 
 |-  ( ph -> ( ( S ` D ) ` E ) = .0. )
80 79 oveq2d 
 |-  ( ph -> ( I .X. ( ( S ` D ) ` E ) ) = ( I .X. .0. ) )
81 10 11 12 ringrz 
 |-  ( ( R e. Ring /\ I e. B ) -> ( I .X. .0. ) = .0. )
82 56 18 81 syl2anc 
 |-  ( ph -> ( I .X. .0. ) = .0. )
83 78 80 82 3eqtrrd 
 |-  ( ph -> .0. = ( ( S ` D ) ` ( I .x. E ) ) )
84 83 20 oveq12d 
 |-  ( ph -> ( .0. ( +g ` R ) ( I .X. ( G ` J ) ) ) = ( ( ( S ` D ) ` ( I .x. E ) ) ( +g ` R ) ( ( S ` D ) ` C ) ) )
85 10 47 12 grplid 
 |-  ( ( R e. Grp /\ ( I .X. ( G ` J ) ) e. B ) -> ( .0. ( +g ` R ) ( I .X. ( G ` J ) ) ) = ( I .X. ( G ` J ) ) )
86 71 73 85 syl2anc 
 |-  ( ph -> ( .0. ( +g ` R ) ( I .X. ( G ` J ) ) ) = ( I .X. ( G ` J ) ) )
87 77 84 86 3eqtr2d 
 |-  ( ph -> ( ( S ` D ) ` ( ( I .x. E ) .+ C ) ) = ( I .X. ( G ` J ) ) )
88 76 87 oveq12d 
 |-  ( ph -> ( ( ( S ` ( J .x. E ) ) ` ( ( I .x. E ) .+ C ) ) ( -g ` R ) ( ( S ` D ) ` ( ( I .x. E ) .+ C ) ) ) = ( ( I .X. ( G ` J ) ) ( -g ` R ) ( I .X. ( G ` J ) ) ) )
89 46 88 eqtrd 
 |-  ( ph -> ( ( ( S ` ( J .x. E ) ) ( -g ` ( ( LCDual ` K ) ` W ) ) ( S ` D ) ) ` ( ( I .x. E ) .+ C ) ) = ( ( I .X. ( G ` J ) ) ( -g ` R ) ( I .X. ( G ` J ) ) ) )
90 10 12 37 grpsubid 
 |-  ( ( R e. Grp /\ ( I .X. ( G ` J ) ) e. B ) -> ( ( I .X. ( G ` J ) ) ( -g ` R ) ( I .X. ( G ` J ) ) ) = .0. )
91 71 73 90 syl2anc 
 |-  ( ph -> ( ( I .X. ( G ` J ) ) ( -g ` R ) ( I .X. ( G ` J ) ) ) = .0. )
92 36 89 91 3eqtrd 
 |-  ( ph -> ( ( S ` ( ( J .x. E ) .- D ) ) ` ( ( I .x. E ) .+ C ) ) = .0. )