Metamath Proof Explorer

Theorem hdmapinvlem4

Description: Part 1.1 of Proposition 1 of Baer p. 110. We use C , D , I , and J for Baer's u, v, s, and t. Our unit vector E has the required properties for his w by hdmapevec2 . Our ( ( SD )C ) means his f(u,v) (note argument reversal). (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 hdmapinvlem4 
|- ( ph -> ( J .X. ( G ` I ) ) = ( ( S ` C ) ` D ) )

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 
 |-  ( -g ` R ) = ( -g ` R )
22 1 4 15 dvhlmod 
 |-  ( ph -> U e. LMod )
23 eqid 
 |-  ( Base ` K ) = ( Base ` K )
24 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
25 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
26 1 23 24 4 5 25 2 15 dvheveccl 
 |-  ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
27 26 eldifad 
 |-  ( ph -> E e. V )
28 5 9 8 10 lmodvscl 
 |-  ( ( U e. LMod /\ J e. B /\ E e. V ) -> ( J .x. E ) e. V )
29 22 19 27 28 syl3anc 
 |-  ( ph -> ( J .x. E ) e. V )
30 27 snssd 
 |-  ( ph -> { E } C_ V )
31 1 4 5 3 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { E } C_ V ) -> ( O ` { E } ) C_ V )
32 15 30 31 syl2anc 
 |-  ( ph -> ( O ` { E } ) C_ V )
33 32 17 sseldd 
 |-  ( ph -> D e. V )
34 5 9 8 10 lmodvscl 
 |-  ( ( U e. LMod /\ I e. B /\ E e. V ) -> ( I .x. E ) e. V )
35 22 18 27 34 syl3anc 
 |-  ( ph -> ( I .x. E ) e. V )
36 32 16 sseldd 
 |-  ( ph -> C e. V )
37 5 6 lmodvacl 
 |-  ( ( U e. LMod /\ ( I .x. E ) e. V /\ C e. V ) -> ( ( I .x. E ) .+ C ) e. V )
38 22 35 36 37 syl3anc 
 |-  ( ph -> ( ( I .x. E ) .+ C ) e. V )
39 1 4 5 7 9 21 13 15 29 33 38 hdmaplns1 
 |-  ( ph -> ( ( S ` ( ( I .x. E ) .+ C ) ) ` ( ( J .x. E ) .- D ) ) = ( ( ( S ` ( ( I .x. E ) .+ C ) ) ` ( J .x. E ) ) ( -g ` R ) ( ( S ` ( ( I .x. E ) .+ C ) ) ` D ) ) )
40 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 hdmapinvlem3 
 |-  ( ph -> ( ( S ` ( ( J .x. E ) .- D ) ) ` ( ( I .x. E ) .+ C ) ) = .0. )
41 5 7 lmodvsubcl 
 |-  ( ( U e. LMod /\ ( J .x. E ) e. V /\ D e. V ) -> ( ( J .x. E ) .- D ) e. V )
42 22 29 33 41 syl3anc 
 |-  ( ph -> ( ( J .x. E ) .- D ) e. V )
43 1 4 5 9 12 13 15 42 38 hdmapip0com 
 |-  ( ph -> ( ( ( S ` ( ( J .x. E ) .- D ) ) ` ( ( I .x. E ) .+ C ) ) = .0. <-> ( ( S ` ( ( I .x. E ) .+ C ) ) ` ( ( J .x. E ) .- D ) ) = .0. ) )
44 40 43 mpbid 
 |-  ( ph -> ( ( S ` ( ( I .x. E ) .+ C ) ) ` ( ( J .x. E ) .- D ) ) = .0. )
45 1 4 5 8 9 10 11 13 15 27 38 19 hdmaplnm1 
 |-  ( ph -> ( ( S ` ( ( I .x. E ) .+ C ) ) ` ( J .x. E ) ) = ( J .X. ( ( S ` ( ( I .x. E ) .+ C ) ) ` E ) ) )
46 eqid 
 |-  ( +g ` R ) = ( +g ` R )
47 1 4 5 6 9 46 13 15 27 35 36 hdmaplna2 
 |-  ( ph -> ( ( S ` ( ( I .x. E ) .+ C ) ) ` E ) = ( ( ( S ` ( I .x. E ) ) ` E ) ( +g ` R ) ( ( S ` C ) ` E ) ) )
48 1 2 3 4 5 9 10 11 12 13 15 16 hdmapinvlem2 
 |-  ( ph -> ( ( S ` C ) ` E ) = .0. )
49 48 oveq2d 
 |-  ( ph -> ( ( ( S ` ( I .x. E ) ) ` E ) ( +g ` R ) ( ( S ` C ) ` E ) ) = ( ( ( S ` ( I .x. E ) ) ` E ) ( +g ` R ) .0. ) )
50 9 lmodring 
 |-  ( U e. LMod -> R e. Ring )
51 22 50 syl 
 |-  ( ph -> R e. Ring )
52 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
53 51 52 syl 
 |-  ( ph -> R e. Grp )
54 1 4 5 9 10 13 15 27 35 hdmapipcl 
 |-  ( ph -> ( ( S ` ( I .x. E ) ) ` E ) e. B )
55 10 46 12 grprid 
 |-  ( ( R e. Grp /\ ( ( S ` ( I .x. E ) ) ` E ) e. B ) -> ( ( ( S ` ( I .x. E ) ) ` E ) ( +g ` R ) .0. ) = ( ( S ` ( I .x. E ) ) ` E ) )
56 53 54 55 syl2anc 
 |-  ( ph -> ( ( ( S ` ( I .x. E ) ) ` E ) ( +g ` R ) .0. ) = ( ( S ` ( I .x. E ) ) ` E ) )
57 1 4 5 8 9 10 11 13 14 15 27 27 18 hdmapglnm2 
 |-  ( ph -> ( ( S ` ( I .x. E ) ) ` E ) = ( ( ( S ` E ) ` E ) .X. ( G ` I ) ) )
58 eqid 
 |-  ( ( HVMap ` K ) ` W ) = ( ( HVMap ` K ) ` W )
59 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
60 1 2 58 13 15 4 9 59 hdmapevec2 
 |-  ( ph -> ( ( S ` E ) ` E ) = ( 1r ` R ) )
61 60 oveq1d 
 |-  ( ph -> ( ( ( S ` E ) ` E ) .X. ( G ` I ) ) = ( ( 1r ` R ) .X. ( G ` I ) ) )
62 1 4 9 10 14 15 18 hgmapcl 
 |-  ( ph -> ( G ` I ) e. B )
63 10 11 59 ringlidm 
 |-  ( ( R e. Ring /\ ( G ` I ) e. B ) -> ( ( 1r ` R ) .X. ( G ` I ) ) = ( G ` I ) )
64 51 62 63 syl2anc 
 |-  ( ph -> ( ( 1r ` R ) .X. ( G ` I ) ) = ( G ` I ) )
65 61 64 eqtrd 
 |-  ( ph -> ( ( ( S ` E ) ` E ) .X. ( G ` I ) ) = ( G ` I ) )
66 56 57 65 3eqtrd 
 |-  ( ph -> ( ( ( S ` ( I .x. E ) ) ` E ) ( +g ` R ) .0. ) = ( G ` I ) )
67 47 49 66 3eqtrd 
 |-  ( ph -> ( ( S ` ( ( I .x. E ) .+ C ) ) ` E ) = ( G ` I ) )
68 67 oveq2d 
 |-  ( ph -> ( J .X. ( ( S ` ( ( I .x. E ) .+ C ) ) ` E ) ) = ( J .X. ( G ` I ) ) )
69 45 68 eqtrd 
 |-  ( ph -> ( ( S ` ( ( I .x. E ) .+ C ) ) ` ( J .x. E ) ) = ( J .X. ( G ` I ) ) )
70 1 4 5 6 9 46 13 15 33 35 36 hdmaplna2 
 |-  ( ph -> ( ( S ` ( ( I .x. E ) .+ C ) ) ` D ) = ( ( ( S ` ( I .x. E ) ) ` D ) ( +g ` R ) ( ( S ` C ) ` D ) ) )
71 1 4 5 8 9 10 11 13 14 15 33 27 18 hdmapglnm2 
 |-  ( ph -> ( ( S ` ( I .x. E ) ) ` D ) = ( ( ( S ` E ) ` D ) .X. ( G ` I ) ) )
72 1 2 3 4 5 9 10 11 12 13 15 17 hdmapinvlem1 
 |-  ( ph -> ( ( S ` E ) ` D ) = .0. )
73 72 oveq1d 
 |-  ( ph -> ( ( ( S ` E ) ` D ) .X. ( G ` I ) ) = ( .0. .X. ( G ` I ) ) )
74 10 11 12 ringlz 
 |-  ( ( R e. Ring /\ ( G ` I ) e. B ) -> ( .0. .X. ( G ` I ) ) = .0. )
75 51 62 74 syl2anc 
 |-  ( ph -> ( .0. .X. ( G ` I ) ) = .0. )
76 71 73 75 3eqtrd 
 |-  ( ph -> ( ( S ` ( I .x. E ) ) ` D ) = .0. )
77 76 oveq1d 
 |-  ( ph -> ( ( ( S ` ( I .x. E ) ) ` D ) ( +g ` R ) ( ( S ` C ) ` D ) ) = ( .0. ( +g ` R ) ( ( S ` C ) ` D ) ) )
78 1 4 5 9 10 13 15 33 36 hdmapipcl 
 |-  ( ph -> ( ( S ` C ) ` D ) e. B )
79 10 46 12 grplid 
 |-  ( ( R e. Grp /\ ( ( S ` C ) ` D ) e. B ) -> ( .0. ( +g ` R ) ( ( S ` C ) ` D ) ) = ( ( S ` C ) ` D ) )
80 53 78 79 syl2anc 
 |-  ( ph -> ( .0. ( +g ` R ) ( ( S ` C ) ` D ) ) = ( ( S ` C ) ` D ) )
81 70 77 80 3eqtrd 
 |-  ( ph -> ( ( S ` ( ( I .x. E ) .+ C ) ) ` D ) = ( ( S ` C ) ` D ) )
82 69 81 oveq12d 
 |-  ( ph -> ( ( ( S ` ( ( I .x. E ) .+ C ) ) ` ( J .x. E ) ) ( -g ` R ) ( ( S ` ( ( I .x. E ) .+ C ) ) ` D ) ) = ( ( J .X. ( G ` I ) ) ( -g ` R ) ( ( S ` C ) ` D ) ) )
83 39 44 82 3eqtr3rd 
 |-  ( ph -> ( ( J .X. ( G ` I ) ) ( -g ` R ) ( ( S ` C ) ` D ) ) = .0. )
84 9 10 11 lmodmcl 
 |-  ( ( U e. LMod /\ J e. B /\ ( G ` I ) e. B ) -> ( J .X. ( G ` I ) ) e. B )
85 22 19 62 84 syl3anc 
 |-  ( ph -> ( J .X. ( G ` I ) ) e. B )
86 10 12 21 grpsubeq0 
 |-  ( ( R e. Grp /\ ( J .X. ( G ` I ) ) e. B /\ ( ( S ` C ) ` D ) e. B ) -> ( ( ( J .X. ( G ` I ) ) ( -g ` R ) ( ( S ` C ) ` D ) ) = .0. <-> ( J .X. ( G ` I ) ) = ( ( S ` C ) ` D ) ) )
87 53 85 78 86 syl3anc 
 |-  ( ph -> ( ( ( J .X. ( G ` I ) ) ( -g ` R ) ( ( S ` C ) ` D ) ) = .0. <-> ( J .X. ( G ` I ) ) = ( ( S ` C ) ` D ) ) )
88 83 87 mpbid 
 |-  ( ph -> ( J .X. ( G ` I ) ) = ( ( S ` C ) ` D ) )