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. )