Metamath Proof Explorer


Theorem mapdpglem9

Description: Lemma for mapdpg . Baer p. 45, line 4: "...so that x would consequently belong to Fy." (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 mapdpglem9 φ 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 dvhlmod φ U LMod
31 eqid + U = + U
32 4 31 5 lmodvnpcan U LMod X V Y V X - ˙ Y + U Y = X
33 30 9 10 32 syl3anc φ X - ˙ Y + U Y = X
34 eqid LSubSp U = LSubSp U
35 4 34 6 lspsncl U LMod Y V N Y LSubSp U
36 30 10 35 syl2anc φ N Y LSubSp U
37 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 mapdpglem8 φ N X - ˙ Y N Y
38 4 5 lmodvsubcl U LMod X V Y V X - ˙ Y V
39 30 9 10 38 syl3anc φ X - ˙ Y V
40 4 6 lspsnid U LMod X - ˙ Y V X - ˙ Y N X - ˙ Y
41 30 39 40 syl2anc φ X - ˙ Y N X - ˙ Y
42 37 41 sseldd φ X - ˙ Y N Y
43 4 6 lspsnid U LMod Y V Y N Y
44 30 10 43 syl2anc φ Y N Y
45 31 34 lssvacl U LMod N Y LSubSp U X - ˙ Y N Y Y N Y X - ˙ Y + U Y N Y
46 30 36 42 44 45 syl22anc φ X - ˙ Y + U Y N Y
47 33 46 eqeltrrd φ X N Y