Metamath Proof Explorer


Theorem mapdpglem20

Description: Lemma for mapdpg . Baer p. 45, line 8: "...so that (Fy)*=Gy'." (Contributed by NM, 20-Mar-2015)

Ref Expression
Hypotheses mapdpglem.h H = LHyp K
mapdpglem.m M = mapd K W
mapdpglem.u U = DVecH K W
mapdpglem.v V = Base U
mapdpglem.s - ˙ = - U
mapdpglem.n N = LSpan U
mapdpglem.c C = LCDual K W
mapdpglem.k φ K HL W H
mapdpglem.x φ X V
mapdpglem.y φ Y V
mapdpglem1.p ˙ = LSSum C
mapdpglem2.j J = LSpan C
mapdpglem3.f F = Base C
mapdpglem3.te φ t M N X ˙ M N Y
mapdpglem3.a A = Scalar U
mapdpglem3.b B = Base A
mapdpglem3.t · ˙ = C
mapdpglem3.r R = - C
mapdpglem3.g φ G F
mapdpglem3.e φ M N X = J G
mapdpglem4.q Q = 0 U
mapdpglem.ne φ N X N Y
mapdpglem4.jt φ M N X - ˙ Y = J t
mapdpglem4.z 0 ˙ = 0 A
mapdpglem4.g4 φ g B
mapdpglem4.z4 φ z M N Y
mapdpglem4.t4 φ t = g · ˙ G R z
mapdpglem4.xn φ X Q
mapdpglem12.yn φ Y Q
mapdpglem17.ep E = inv r A g · ˙ z
Assertion mapdpglem20 φ M N Y = J E

Proof

Step Hyp Ref Expression
1 mapdpglem.h H = LHyp K
2 mapdpglem.m M = mapd K W
3 mapdpglem.u U = DVecH K W
4 mapdpglem.v V = Base U
5 mapdpglem.s - ˙ = - U
6 mapdpglem.n N = LSpan U
7 mapdpglem.c C = LCDual K W
8 mapdpglem.k φ K HL W H
9 mapdpglem.x φ X V
10 mapdpglem.y φ Y V
11 mapdpglem1.p ˙ = LSSum C
12 mapdpglem2.j J = LSpan C
13 mapdpglem3.f F = Base C
14 mapdpglem3.te φ t M N X ˙ M N Y
15 mapdpglem3.a A = Scalar U
16 mapdpglem3.b B = Base A
17 mapdpglem3.t · ˙ = C
18 mapdpglem3.r R = - C
19 mapdpglem3.g φ G F
20 mapdpglem3.e φ M N X = J G
21 mapdpglem4.q Q = 0 U
22 mapdpglem.ne φ N X N Y
23 mapdpglem4.jt φ M N X - ˙ Y = J t
24 mapdpglem4.z 0 ˙ = 0 A
25 mapdpglem4.g4 φ g B
26 mapdpglem4.z4 φ z M N Y
27 mapdpglem4.t4 φ t = g · ˙ G R z
28 mapdpglem4.xn φ X Q
29 mapdpglem12.yn φ Y Q
30 mapdpglem17.ep E = inv r A g · ˙ z
31 eqid 0 C = 0 C
32 eqid LSAtoms C = LSAtoms C
33 1 7 8 lcdlvec φ C LVec
34 eqid LSAtoms U = LSAtoms U
35 1 3 8 dvhlmod φ U LMod
36 eldifsn Y V Q Y V Y Q
37 10 29 36 sylanbrc φ Y V Q
38 4 6 21 34 35 37 lsatlspsn φ N Y LSAtoms U
39 1 2 3 34 7 32 8 38 mapdat φ M N Y LSAtoms C
40 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 mapdpglem19 φ E M N Y
41 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 mapdpglem18 φ E 0 C
42 31 12 32 33 39 40 41 lsatel φ M N Y = J E