Metamath Proof Explorer


Theorem mapdpglem10

Description: Lemma for mapdpg . Baer p. 45, line 6: "Hence Fx=Fy, an impossibility." (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
mapdpglem4.g0 φ g = 0 ˙
Assertion mapdpglem10 φ N X = N Y

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 mapdpglem4.g0 φ g = 0 ˙
30 1 3 8 dvhlvec φ U LVec
31 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 mapdpglem9 φ X N Y
32 4 21 6 30 10 31 28 lspsneleq φ N X = N Y