Metamath Proof Explorer


Theorem mapdpglem25

Description: Lemma for mapdpg . Baer p. 45 line 12: "Then we have Gy' = Gy'' and G(x'-y') = G(x'-y'')." (Contributed by NM, 21-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
Assertion mapdpglem25 φ J h = J i J G R h = J 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 18 simprd φ M N Y = J h M N X - ˙ Y = J G R h
21 20 simpld φ M N Y = J h
22 19 simprd φ M N Y = J i M N X - ˙ Y = J G R i
23 22 simpld φ M N Y = J i
24 21 23 eqtr3d φ J h = J i
25 20 simprd φ M N X - ˙ Y = J G R h
26 22 simprd φ M N X - ˙ Y = J G R i
27 25 26 eqtr3d φ J G R h = J G R i
28 24 27 jca φ J h = J i J G R h = J G R i