Metamath Proof Explorer


Theorem mapdpglem27

Description: Lemma for mapdpg . Baer p. 45 line 16: "v(x'-y'') = x'-y'" (with equality swapped). (Contributed by NM, 22-Mar-2015)

Ref Expression
Hypotheses mapdpg.h H = LHyp K
mapdpg.m M = mapd K W
mapdpg.u U = DVecH K W
mapdpg.v V = Base U
mapdpg.s - ˙ = - U
mapdpg.z 0 ˙ = 0 U
mapdpg.n N = LSpan U
mapdpg.c C = LCDual K W
mapdpg.f F = Base C
mapdpg.r R = - C
mapdpg.j J = LSpan C
mapdpg.k φ K HL W H
mapdpg.x φ X V 0 ˙
mapdpg.y φ Y V 0 ˙
mapdpg.g φ G F
mapdpg.ne φ N X N Y
mapdpg.e φ M N X = J G
mapdpgem25.h1 φ h F M N Y = J h M N X - ˙ Y = J G R h
mapdpgem25.i1 φ i F M N Y = J i M N X - ˙ Y = J G R i
mapdpglem26.a A = Scalar U
mapdpglem26.b B = Base A
mapdpglem26.t · ˙ = C
mapdpglem26.o O = 0 A
Assertion mapdpglem27 φ v B O G R h = v · ˙ G R i

Proof

Step Hyp Ref Expression
1 mapdpg.h H = LHyp K
2 mapdpg.m M = mapd K W
3 mapdpg.u U = DVecH K W
4 mapdpg.v V = Base U
5 mapdpg.s - ˙ = - U
6 mapdpg.z 0 ˙ = 0 U
7 mapdpg.n N = LSpan U
8 mapdpg.c C = LCDual K W
9 mapdpg.f F = Base C
10 mapdpg.r R = - C
11 mapdpg.j J = LSpan C
12 mapdpg.k φ K HL W H
13 mapdpg.x φ X V 0 ˙
14 mapdpg.y φ Y V 0 ˙
15 mapdpg.g φ G F
16 mapdpg.ne φ N X N Y
17 mapdpg.e φ M N X = J G
18 mapdpgem25.h1 φ h F M N Y = J h M N X - ˙ Y = J G R h
19 mapdpgem25.i1 φ i F M N Y = J i M N X - ˙ Y = J G R i
20 mapdpglem26.a A = Scalar U
21 mapdpglem26.b B = Base A
22 mapdpglem26.t · ˙ = C
23 mapdpglem26.o O = 0 A
24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 mapdpglem25 φ J h = J i J G R h = J G R i
25 24 simprd φ J G R h = J G R i
26 eqid Scalar C = Scalar C
27 eqid Base Scalar C = Base Scalar C
28 eqid 0 Scalar C = 0 Scalar C
29 1 8 12 lcdlvec φ C LVec
30 1 8 12 lcdlmod φ C LMod
31 18 simpld φ h F
32 9 10 lmodvsubcl C LMod G F h F G R h F
33 30 15 31 32 syl3anc φ G R h F
34 19 simpld φ i F
35 9 10 lmodvsubcl C LMod G F i F G R i F
36 30 15 34 35 syl3anc φ G R i F
37 9 26 27 28 22 11 29 33 36 lspsneq φ J G R h = J G R i v Base Scalar C 0 Scalar C G R h = v · ˙ G R i
38 1 3 20 21 8 26 27 12 lcdsbase φ Base Scalar C = B
39 1 3 20 23 8 26 28 12 lcd0 φ 0 Scalar C = O
40 39 sneqd φ 0 Scalar C = O
41 38 40 difeq12d φ Base Scalar C 0 Scalar C = B O
42 41 rexeqdv φ v Base Scalar C 0 Scalar C G R h = v · ˙ G R i v B O G R h = v · ˙ G R i
43 37 42 bitrd φ J G R h = J G R i v B O G R h = v · ˙ G R i
44 25 43 mpbid φ v B O G R h = v · ˙ G R i