Metamath Proof Explorer

Theorem hgmapmul

Description: Part 15 of Baer p. 50 line 16. The multiplication is reversed after converting to the dual space scalar to the vector space scalar. (Contributed by NM, 7-Jun-2015)

Ref Expression
Hypotheses hgmapmul.h 
|- H = ( LHyp ` K )
hgmapmul.u 
|- U = ( ( DVecH ` K ) ` W )
hgmapmul.r 
|- R = ( Scalar ` U )
hgmapmul.b 
|- B = ( Base ` R )
hgmapmul.t 
|- .x. = ( .r ` R )
hgmapmul.g 
|- G = ( ( HGMap ` K ) ` W )
hgmapmul.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hgmapmul.x 
|- ( ph -> X e. B )
hgmapmul.y 
|- ( ph -> Y e. B )
Assertion hgmapmul 
|- ( ph -> ( G ` ( X .x. Y ) ) = ( ( G ` Y ) .x. ( G ` X ) ) )

Proof

Step Hyp Ref Expression
1 hgmapmul.h 
 |-  H = ( LHyp ` K )
2 hgmapmul.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hgmapmul.r 
 |-  R = ( Scalar ` U )
4 hgmapmul.b 
 |-  B = ( Base ` R )
5 hgmapmul.t 
 |-  .x. = ( .r ` R )
6 hgmapmul.g 
 |-  G = ( ( HGMap ` K ) ` W )
7 hgmapmul.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 hgmapmul.x 
 |-  ( ph -> X e. B )
9 hgmapmul.y 
 |-  ( ph -> Y e. B )
10 eqid 
 |-  ( Base ` U ) = ( Base ` U )
11 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
12 1 2 10 11 7 dvh1dim 
 |-  ( ph -> E. t e. ( Base ` U ) t =/= ( 0g ` U ) )
13 eqid 
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
14 1 13 7 lcdlmod 
 |-  ( ph -> ( ( LCDual ` K ) ` W ) e. LMod )
15 14 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( LCDual ` K ) ` W ) e. LMod )
16 eqid 
 |-  ( Scalar ` ( ( LCDual ` K ) ` W ) ) = ( Scalar ` ( ( LCDual ` K ) ` W ) )
17 eqid 
 |-  ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) )
18 1 2 3 4 13 16 17 6 7 8 hgmapdcl 
 |-  ( ph -> ( G ` X ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
19 18 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( G ` X ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
20 1 2 3 4 13 16 17 6 7 9 hgmapdcl 
 |-  ( ph -> ( G ` Y ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
21 20 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( G ` Y ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
22 eqid 
 |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
23 eqid 
 |-  ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )
24 7 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
25 simp2 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> t e. ( Base ` U ) )
26 1 2 10 13 22 23 24 25 hdmapcl 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` t ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
27 eqid 
 |-  ( .s ` ( ( LCDual ` K ) ` W ) ) = ( .s ` ( ( LCDual ` K ) ` W ) )
28 eqid 
 |-  ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) )
29 22 16 27 17 28 lmodvsass 
 |-  ( ( ( ( LCDual ` K ) ` W ) e. LMod /\ ( ( G ` X ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) /\ ( G ` Y ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) /\ ( ( ( HDMap ` K ) ` W ) ` t ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) ) ) -> ( ( ( G ` X ) ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) = ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( G ` Y ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) ) )
30 15 19 21 26 29 syl13anc 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( G ` X ) ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) = ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( G ` Y ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) ) )
31 1 2 7 dvhlmod 
 |-  ( ph -> U e. LMod )
32 31 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> U e. LMod )
33 8 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> X e. B )
34 9 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> Y e. B )
35 eqid 
 |-  ( .s ` U ) = ( .s ` U )
36 10 3 35 4 5 lmodvsass 
 |-  ( ( U e. LMod /\ ( X e. B /\ Y e. B /\ t e. ( Base ` U ) ) ) -> ( ( X .x. Y ) ( .s ` U ) t ) = ( X ( .s ` U ) ( Y ( .s ` U ) t ) ) )
37 32 33 34 25 36 syl13anc 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( X .x. Y ) ( .s ` U ) t ) = ( X ( .s ` U ) ( Y ( .s ` U ) t ) ) )
38 37 fveq2d 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( ( X .x. Y ) ( .s ` U ) t ) ) = ( ( ( HDMap ` K ) ` W ) ` ( X ( .s ` U ) ( Y ( .s ` U ) t ) ) ) )
39 10 3 35 4 lmodvscl 
 |-  ( ( U e. LMod /\ Y e. B /\ t e. ( Base ` U ) ) -> ( Y ( .s ` U ) t ) e. ( Base ` U ) )
40 32 34 25 39 syl3anc 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( Y ( .s ` U ) t ) e. ( Base ` U ) )
41 1 2 10 35 3 4 13 27 23 6 24 40 33 hgmapvs 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( X ( .s ` U ) ( Y ( .s ` U ) t ) ) ) = ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` ( Y ( .s ` U ) t ) ) ) )
42 1 2 10 35 3 4 13 27 23 6 24 25 34 hgmapvs 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( Y ( .s ` U ) t ) ) = ( ( G ` Y ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) )
43 42 oveq2d 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` ( Y ( .s ` U ) t ) ) ) = ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( G ` Y ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) ) )
44 38 41 43 3eqtrd 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( ( X .x. Y ) ( .s ` U ) t ) ) = ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( G ` Y ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) ) )
45 3 4 5 lmodmcl 
 |-  ( ( U e. LMod /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
46 31 8 9 45 syl3anc 
 |-  ( ph -> ( X .x. Y ) e. B )
47 46 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( X .x. Y ) e. B )
48 1 2 10 35 3 4 13 27 23 6 24 25 47 hgmapvs 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( ( X .x. Y ) ( .s ` U ) t ) ) = ( ( G ` ( X .x. Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) )
49 30 44 48 3eqtr2rd 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( G ` ( X .x. Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) = ( ( ( G ` X ) ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) )
50 eqid 
 |-  ( 0g ` ( ( LCDual ` K ) ` W ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) )
51 1 13 7 lcdlvec 
 |-  ( ph -> ( ( LCDual ` K ) ` W ) e. LVec )
52 51 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( LCDual ` K ) ` W ) e. LVec )
53 1 2 3 4 13 16 17 6 7 46 hgmapdcl 
 |-  ( ph -> ( G ` ( X .x. Y ) ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
54 53 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( G ` ( X .x. Y ) ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
55 16 17 28 lmodmcl 
 |-  ( ( ( ( LCDual ` K ) ` W ) e. LMod /\ ( G ` X ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) /\ ( G ` Y ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) -> ( ( G ` X ) ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
56 14 18 20 55 syl3anc 
 |-  ( ph -> ( ( G ` X ) ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
57 56 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( G ` X ) ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
58 simp3 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> t =/= ( 0g ` U ) )
59 1 2 10 11 13 50 23 24 25 hdmapeq0 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( ( HDMap ` K ) ` W ) ` t ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> t = ( 0g ` U ) ) )
60 59 necon3bid 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( ( HDMap ` K ) ` W ) ` t ) =/= ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> t =/= ( 0g ` U ) ) )
61 58 60 mpbird 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` t ) =/= ( 0g ` ( ( LCDual ` K ) ` W ) ) )
62 22 27 16 17 50 52 54 57 26 61 lvecvscan2 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( G ` ( X .x. Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) = ( ( ( G ` X ) ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) <-> ( G ` ( X .x. Y ) ) = ( ( G ` X ) ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) ) )
63 49 62 mpbid 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( G ` ( X .x. Y ) ) = ( ( G ` X ) ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) )
64 63 rexlimdv3a 
 |-  ( ph -> ( E. t e. ( Base ` U ) t =/= ( 0g ` U ) -> ( G ` ( X .x. Y ) ) = ( ( G ` X ) ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) ) )
65 12 64 mpd 
 |-  ( ph -> ( G ` ( X .x. Y ) ) = ( ( G ` X ) ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) )
66 1 2 3 4 6 7 8 hgmapcl 
 |-  ( ph -> ( G ` X ) e. B )
67 1 2 3 4 6 7 9 hgmapcl 
 |-  ( ph -> ( G ` Y ) e. B )
68 1 2 3 4 5 13 16 28 7 66 67 lcdsmul 
 |-  ( ph -> ( ( G ` X ) ( .r ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) = ( ( G ` Y ) .x. ( G ` X ) ) )
69 65 68 eqtrd 
 |-  ( ph -> ( G ` ( X .x. Y ) ) = ( ( G ` Y ) .x. ( G ` X ) ) )